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

30 Oct 2006

      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