I'm trying to create a simple parser for the GADT evaluator from the wobbly types paper, and I need a little help. Here's the GADT and the evaluator...
data Term a where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Pair :: Term a -> Term b -> Term (a,b) Fst :: Term (a,b) -> Term a Snd :: Term (a,b) -> Term b
eval :: Term a -> a eval (Lit i) = i eval (Inc t) = eval t + 1 eval (IsZ t) = eval t == 0 eval (If b t e) = if eval b then eval t else eval e eval (Pair a b) = (eval a, eval b) eval (Fst t) = fst (eval t) eval (Snd t) = snd (eval t)
...and instead of writing my own read instance, I thought I'd take a shortcut and just try converting a regular data type to our generalized one...
data Expr = ELit Int | EInc Expr | EIsZ Expr | EPair Expr Expr | EIf Expr Expr Expr | EFst Expr | ESnd Expr deriving (Read,Show)
my_read' :: Expr -> Term a my_read' (ELit a) = Lit a my_read' (EInc a) = Inc (my_read' a) my_read' (EIsZ a) = IsZ (my_read' a) my_read' (EPair a b) = Pair (my_read' a) (my_read' b) my_read' (EIf p t e) = If (my_read' p) (my_read' t) (my_read' e) my_read' (EFst a) = Fst (my_read' a) my_read' (ESnd a) = Snd (my_read' a)
...That looks nice and simple, but it doesn't type check. GHCi-6.6 complains... Couldn't match expected type `a' (a rigid variable) against inferred type `Int' `a' is bound by the type signature for `my_read' at eval_gadt_wobbly.hs:45:24 Expected type: Term a Inferred type: Term Int In the expression: Lit a In the definition of `my_read': my_read (ELit a) = Lit a ...No surprise there, since there is no way to fail in the event of a maltyped "Expr". The next thing to try is a type class solution...
class MyRead a where my_read :: Expr -> Term a
instance MyRead Int where my_read (ELit a) = Lit a my_read (EInc a) = Inc (my_read a) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) my_read (EFst a) = Fst (my_read a :: MyRead b => Term (Int,b)) -- my_read (ESnd a) = Snd (my_read a) instance MyRead Bool where my_read (EIsZ a) = IsZ (my_read a) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) -- my_read (EFst a) = Fst (my_read a) -- my_read (ESnd a) = Snd (my_read a) instance (MyRead a, MyRead b) => MyRead (a,b) where my_read (EPair a b) = Pair (my_read a) (my_read b) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) -- my_read (EFst a) = Fst (my_read a) -- my_read (ESnd a) = Snd (my_read a)
This just about works, except for the definitions for the "Fst" and "Snd" constructors. The compiler complains... Ambiguous type variable `b' in the constraint: `MyRead b' arising from use of `my_read' at eval_gadt_wobbly.hs:65:28-36 Probable fix: add a type signature that fixes these type variable(s) ...Of course, that makes perfect sense, since, if we're applying "Fst" to a term, then we don't care about the other branch of the "Pair". You can get it accepted by the type checker by making the types more concrete... my_read (EFst a) = Fst (my_read a :: Term (Int,Int)) ...or... my_read (EFst a) = Fst (my_read a :: Term (Int,Bool)) ...but how does a person fix this to work in the more general case? Or is this even the right way to build a parser for the GADT evaluator example? Notice the repetition needed: the "If", "Fst", and "Snd" defintions have to be copied to all three instances. Also, feel free to comment on this example, and the fact that it will evaluate with no problems.
static_vs_laziness = eval (my_read (EIf (EIsZ (ELit 0)) (ELit 9) (EIsZ (ELit 42)))::Term Int)
Thanks, Greg Buchholz
I don't have an answer, but would be extremely interested in knowing one! one of my first attempts to use GADTs was to do something similar, implemening the simple polymorphic lambda calculus in a way that transformations could be guarenteed typesafe statically, but then when I went and tried to write an interpreter, I couldn't figure out how to read in programs to interpret. it seems you would want something like first class existentials 'Exp (exists a . a)' or something like that. John -- John Meacham - ⑆repetae.net⑆john⑈
Just noticed Joost Visser's message but since I had (essentially a very similar) response I thought I might send it off as well ... It includes the conditional cases. Regards, -d {-# OPTIONS_GHC -fglasgow-exts #-} module Main where data Term a where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Pair :: Term a -> Term b -> Term (a,b) Fst :: Term (a,b) -> Term a Snd :: Term (a,b) -> Term b data Expr = ELit Int | EInc Expr | EIsZ Expr | EPair Expr Expr | EIf Expr Expr Expr | EFst Expr | ESnd Expr deriving (Read,Show) -- Give a GADT for representation types data R a where Rint :: R Int Rbool :: R Bool Rpair :: R a -> R b -> R (a,b) -- Give an existential type with a type representation data TermEx where MkTerm :: R a -> Term a -> TermEx -- we use Weirich's higher-order type-safe cast to avoid deep traversals -- one can replace the type_cast with a more simple traversal-based -- version. data CL c a d = CL (c (d,a)) data CR c a d = CR (c (a,d)) type_cast :: forall a b c. R a -> R b -> c a -> c b type_cast Rint Rint x = x type_cast Rbool Rbool x = x type_cast (Rpair (ra::(R a0)) (rb::(R b0))) (Rpair (ra'::(R a0')) (rb'::(R b0'))) x = let g = (type_cast ra ra' :: ( (CL c b0) a0 -> (CL c b0) a0' )) h = (type_cast rb rb' :: ( (CR c a0') b0 -> (CR c a0') b0')) in case (g (CL x)) of CL x' -> case (h (CR x')) of CR y' -> y' type_cast _ _ _ = error "cannot cast!" -- give only the cases for Eif and Elit, the others are similar my_read :: Expr -> TermEx my_read (ELit i) = MkTerm Rint (Lit i); my_read (EIf p t e) = case (my_read p) of MkTerm rb b -> case rb of Rbool -> case (my_read t) of MkTerm r1 t1 -> case (my_read e) of MkTerm r2 t2 -> MkTerm r2 (If b (type_cast r1 r2 t1) t2) _ -> error "conditional not boolean!"
On Oct 31, 2006, at 2:19 AM, Dimitrios Vytiniotis wrote:
-- Give a GADT for representation types data R a where Rint :: R Int Rbool :: R Bool Rpair :: R a -> R b -> R (a,b)
-- Give an existential type with a type representation data TermEx where MkTerm :: R a -> Term a -> TermEx
-- we use Weirich's higher-order type-safe cast to avoid deep traversals -- one can replace the type_cast with a more simple traversal-based -- version.
...complicated higher order stuff... For instance:
data a :==: b where Refl :: a :==: a
(===) :: Monad m => R a -> R b -> m (a :==: b) Rint === Rint = return Refl Rbool === Rbool = return Refl Rpair a b === Rpair c d = do Refl <- a === c Refl <- b === d return Refl a === b = fail $ show a ++ " =/= " ++ show b
cast :: a :==: b -> c a -> c b cast Refl x = x
In particular one wants to extract the Term part of a TermEx:
getTerm :: Monad m => TermEx -> R a -> m (Term a) getTerm (MkTerm r' t) r = do Refl <- r === r' return t
/ Ulf
Hi Greg, We've built some GADT parsers recently to fit our two-level transformation library with front-ends for for XML Schema and SQL. See "Coupled Schema Transformation and Data Conversion For XML and SQL" (PADL 2007) if you're interested. The trick is to use a constructor in which the "a" variable of "Term a" is existentially quantified. For example:
data DynTerm where DynTerm :: Type a -> Term a -> DynTerm
(I'm using GADT notation here, but normal ADT syntax would do just fine as well.) The first argument is the folklore GADT for representing types:
data Type a where Int :: Type Int Bool :: Type Bool Prod :: Type a -> Type b -> Type (a,b)
Then you can write your parser function with the following type:
my_read' :: Expr -> DynTerm
Or, more likely:
my_read' :: Expr -> Maybe DynTerm
with:
my_read' (ELit a) = return $ DynTerm Int (Lit a) my_read' (EInc a) = do DynTerm Int a' <- my_read' a return (DynTerm Int (Inc a'))
Then you call eval something like:
test :: Expr -> Maybe Dynamic test expr = do DynTerm t a <- my_read' expr return (Dyn t (eval a))
The Dynamic is defined as:
data Dynamic where Dyn :: Type a -> a -> Dynamic
The dynamic typing trick here is due to Swierstra and Baars. For further processing of the Dynamic result, you'll need to write functions with a type like:
f :: Type a -> a -> X
A typical example:
gshow :: Type a -> a -> String gshow Int i = show i gshow Bool b = show b gshow (Prod a b) (x,y) = "("++gshow a x++","++gshow b y++")"
Hope this helps. Source code is attached. Best, Joost On Oct 30, 2006, at 5:00 PM, Greg Buchholz wrote:
I'm trying to create a simple parser for the GADT evaluator from the wobbly types paper, and I need a little help. Here's the GADT and the evaluator...
data Term a where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Pair :: Term a -> Term b -> Term (a,b) Fst :: Term (a,b) -> Term a Snd :: Term (a,b) -> Term b
eval :: Term a -> a eval (Lit i) = i eval (Inc t) = eval t + 1 eval (IsZ t) = eval t == 0 eval (If b t e) = if eval b then eval t else eval e eval (Pair a b) = (eval a, eval b) eval (Fst t) = fst (eval t) eval (Snd t) = snd (eval t)
...and instead of writing my own read instance, I thought I'd take a shortcut and just try converting a regular data type to our generalized one...
data Expr = ELit Int | EInc Expr | EIsZ Expr | EPair Expr Expr | EIf Expr Expr Expr | EFst Expr | ESnd Expr deriving (Read,Show)
my_read' :: Expr -> Term a my_read' (ELit a) = Lit a my_read' (EInc a) = Inc (my_read' a) my_read' (EIsZ a) = IsZ (my_read' a) my_read' (EPair a b) = Pair (my_read' a) (my_read' b) my_read' (EIf p t e) = If (my_read' p) (my_read' t) (my_read' e) my_read' (EFst a) = Fst (my_read' a) my_read' (ESnd a) = Snd (my_read' a)
...That looks nice and simple, but it doesn't type check. GHCi-6.6 complains...
Couldn't match expected type `a' (a rigid variable) against inferred type `Int' `a' is bound by the type signature for `my_read' at eval_gadt_wobbly.hs:45:24 Expected type: Term a Inferred type: Term Int In the expression: Lit a In the definition of `my_read': my_read (ELit a) = Lit a
...No surprise there, since there is no way to fail in the event of a maltyped "Expr". The next thing to try is a type class solution...
class MyRead a where my_read :: Expr -> Term a
instance MyRead Int where my_read (ELit a) = Lit a my_read (EInc a) = Inc (my_read a) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) my_read (EFst a) = Fst (my_read a :: MyRead b => Term (Int,b)) -- my_read (ESnd a) = Snd (my_read a)instance MyRead Bool where my_read (EIsZ a) = IsZ (my_read a) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) -- my_read (EFst a) = Fst (my_read a) -- my_read (ESnd a) = Snd (my_read a) instance (MyRead a, MyRead b) => MyRead (a,b) where my_read (EPair a b) = Pair (my_read a) (my_read b) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) -- my_read (EFst a) = Fst (my_read a) -- my_read (ESnd a) = Snd (my_read a)
This just about works, except for the definitions for the "Fst" and "Snd" constructors. The compiler complains...
Ambiguous type variable `b' in the constraint: `MyRead b' arising from use of `my_read' at eval_gadt_wobbly.hs:65:28-36 Probable fix: add a type signature that fixes these type variable(s)
...Of course, that makes perfect sense, since, if we're applying "Fst" to a term, then we don't care about the other branch of the "Pair". You can get it accepted by the type checker by making the types more concrete...
my_read (EFst a) = Fst (my_read a :: Term (Int,Int)) ...or... my_read (EFst a) = Fst (my_read a :: Term (Int,Bool))
...but how does a person fix this to work in the more general case? Or is this even the right way to build a parser for the GADT evaluator example? Notice the repetition needed: the "If", "Fst", and "Snd" defintions have to be copied to all three instances. Also, feel free to comment on this example, and the fact that it will evaluate with no problems.
static_vs_laziness = eval (my_read (EIf (EIsZ (ELit 0)) (ELit 9) (EIsZ (ELit 42)))::Term Int)
Thanks,
Greg Buchholz
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Dr. ir. Joost Visser | Departamento de Informática phone +351-253-604461 | Universidade do Minho fax +351-253-604471 | mailto:Joost.Visser@di.uminho.pt mobile +351-91-6253618 | http://www.di.uminho.pt/~joost.visser
...No surprise there, since there is no way to fail in the event of a maltyped "Expr". The next thing to try is a type class solution...
Think about it: you need to do type checking. For our little language we used Template Haskell to do your "Expr -> Term a" translation, thus the type-checking of our input programs is actually done by Haskell's type checker ;-) See our PLPV paper http://www.iro.umontreal.ca/~monnier/tct.pdf Stefan
Thanks to everyone who replied (especially Dimitrios Vytiniotis and Joost Visser). I now know the standard way to write the GADT parser. But I'm still curious if anyone has comments pertaining to the version using type classes. It seems so close to doing what we want, and it is pretty straightforward to implement. The best way I can think to describe it would be to say it uses the type system to find what it should parse next, and dies of a pattern match failure if something unexpected shows up, instead of checking to see if we can assemble a type safe tree from pre-parsed parts (does that make any sense?). I'm curious if there could be a small change to the type system to make the fully general "my_read" possible, or if it suffers from an incurable defect. Thanks, Greg Buchholz
{-# OPTIONS -fglasgow-exts #-}
main = print test
test :: Int test = eval.my_read.read $ "(EIf (EIsZ (ELit 0)) " ++ " (EInc (ELit 1)) " ++ " (EFst (EPair (ELit 42) " ++ " (ELit 43))))"
class MyRead a where my_read :: Expr -> Term a
instance MyRead Int where my_read (ELit a) = Lit a my_read (EInc a) = Inc (my_read a) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) my_read (EFst a) = Fst (my_read a :: Term (Int,Int)) my_read (ESnd a) = Snd (my_read a :: Term (Int,Int))
instance MyRead Bool where my_read (EIsZ a) = IsZ (my_read a) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e) my_read (EFst a) = Fst (my_read a :: Term (Bool,Bool)) my_read (ESnd a) = Snd (my_read a :: Term (Bool,Bool))
instance (MyRead a, MyRead x) => MyRead (a,x) where my_read (EPair a b) = Pair (my_read a) (my_read b) my_read (EIf p t e) = If (my_read p) (my_read t) (my_read e)
data Expr = ELit Int | EInc Expr | EIsZ Expr | EPair Expr Expr | EIf Expr Expr Expr | EFst Expr | ESnd Expr deriving (Read,Show)
data Term a where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Pair :: Term a -> Term b -> Term (a,b) Fst :: Term (a,b) -> Term a Snd :: Term (a,b) -> Term b
eval :: Term a -> a eval (Lit i) = i eval (Inc t) = eval t + 1 eval (IsZ t) = eval t == 0 eval (If b t e) = if eval b then eval t else eval e eval (Pair a b) = (eval a, eval b) eval (Fst t) = fst (eval t) eval (Snd t) = snd (eval t)
On Nov 1, 2006, at 1:32 AM, Greg Buchholz wrote:
Thanks to everyone who replied (especially Dimitrios Vytiniotis and Joost Visser). I now know the standard way to write the GADT parser. But I'm still curious if anyone has comments pertaining to the version using type classes. It seems so close to doing what we want, and it is pretty straightforward to implement. The best way I can think to describe it would be to say it uses the type system to find what it should parse next, and dies of a pattern match failure if something unexpected shows up, instead of checking to see if we can assemble a type safe tree from pre-parsed parts (does that make any sense?).
I'm curious if there could be a small change to the type system to make the fully general "my_read" possible, or if it suffers from an incurable defect.
I'm not sure what you're asking, but it's possible to get my_read :: .. => Expr -> Term a Previously given code:
-- Give a GADT for representation types data R a where Rint :: R Int Rbool :: R Bool Rpair :: R a -> R b -> R (a,b)
-- Give an existential type with a type representation data TermEx where MkTerm :: R a -> Term a -> TermEx
my_readEx :: Expr -> TermEx getTerm :: TermEx -> R a -> Term a
Given this you can define
class Rep a where rep :: R a instance Rep Int where rep = Rint instance Rep Bool where rep = Rbool instance (Rep a, Rep b) => Rep (a,b) where rep = Rpair rep rep
my_read :: Rep a => Expr -> Term a my_read e = getTerm (my_readEx e) rep
/ Ulf
Ulf Norell wrote:
I'm not sure what you're asking...
Me neither probably.
, but it's possible to get
my_read :: .. => Expr -> Term a
Previously given code:
-- Give a GADT for representation types data R a where Rint :: R Int Rbool :: R Bool Rpair :: R a -> R b -> R (a,b)
Yeah, I especially liked Joost Visser's version which is pretty slick. I was just wondering if it was possible to accomplish the same task in a different way, using type classes instead of GADTs, which would seem to work in a more top-downish fashion, as opposed to bottom-upish. But I'm not an expert enough with type systems to know if the... Ambiguous type variable `b' in the constraint: `MyRead b' arising from use of `my_read' at gadt_wobbly.hs:65:28-36 Probable fix: add a type signature that fixes these type variable(s) ...problem was fixable by adding a type signature or grafting on some additional type machinery. Thanks, Greg Buchholz
Hello Greg, It seems that I am late for the party but we used a "GADT parser" in the tool we built for our "Generating Generic Functions" paper[1]. It so happens that I made slides for this material so, if you're interested you can have a look at [2]. The motivation for doing this was that we needed to check whether a simply typed lambda calculus term satisfies a property or not. The road we took was software testing, but for that we needed evaluation and hence the GADT stuff. You might like the fact that these well-typed terms include binding constructs such as lambda abstractions and variables. The code uses some tricks that I borrowed from Conor McBride and company :). Cheers, Alexey [1] http://www.cs.uu.nl/wiki/Alexey/GeneratingGenericFunctions [2] http://abaris.zoo.cs.uu.nl:8080/wiki/pub/Alexey/GeneratingGenericFunctions/C...
participants (7)
-
Alexey Rodriguez -
Dimitrios Vytiniotis -
Greg Buchholz -
John Meacham -
Joost Visser -
Stefan Monnier -
Ulf Norell