Re: [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

The first argument is the folklore GADT for representing types:

(I'm using GADT notation here, but normal ADT syntax would do just fine as well.)

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

one...

shortcut and just try converting a regular data type to our generalized

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)

"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


...Of course, that makes perfect sense, since, if we're applying "Fst"

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


is this even the right way to build a parser for the GADT evaluator
example?  Notice the repetition needed: the "If", "Fst", and "Snd"

comment on this example, and the fact that it will evaluate with no
problems.

This just about works, except for the definitions for the "Fst" and Probable fix: add a type signature that fixes these type variable(s) to a term, then we don't care about the other branch of the "Pair". You ...but how does a person fix this to work in the more general case? Or defintions have to be copied to all three instances. Also, feel free to

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:[EMAIL PROTECTED]
mobile +351-91-6253618 | http://www.di.uminho.pt/~joost.visser

GadtParser.hs
Description: Binary data

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe