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

[Greg Buchholz]

    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