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

30 Oct 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@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