[Haskell-cafe] Simple GADT parser for the eval example

[Joost Visser]

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 --------------