[Haskell-cafe] Simple GADT parser for the eval example
Joost Visser
joost.visser at di.uminho.pt
Mon Oct 30 20:10:41 EST 2006
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 at 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 at di.uminho.pt
mobile +351-91-6253618 | http://www.di.uminho.pt/~joost.visser
-------------- next part --------------
A non-text attachment was scrubbed...
Name: GadtParser.hs
Type: application/octet-stream
Size: 1841 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20061031/160544ac/GadtParser.obj
-------------- next part --------------
More information about the Haskell-Cafe
mailing list