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

[Alexey Rodriguez]

Hello Greg,It seems that I am late for the party but we used a GADT parser in the tool we built for our Generating Generic Functions paper[1]. It so happens that I made slides for this material so, if you're interested you can have a look at [2].
The motivation for doing this was that we needed to check whether a simply typed lambda calculus term satisfies a property or not. The road we took was software testing, but for that we needed evaluation and hence the GADT stuff.
You might like the fact that these well-typed terms include binding constructs such as lambda abstractions and variables. The code uses some tricks that I borrowed from Conor McBride and company :).Cheers,
Alexey[1] http://www.cs.uu.nl/wiki/Alexey/GeneratingGenericFunctions[2] 
http://abaris.zoo.cs.uu.nl:8080/wiki/pub/Alexey/GeneratingGenericFunctions/CompileGGF.pdf
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Ulf Norell]

On Oct 31, 2006, at 2:19 AM, Dimitrios Vytiniotis wrote:


-- Give a GADT for representation types
data R a where
  Rint :: R Int
  Rbool :: R Bool
  Rpair :: R a - R b - R (a,b)

-- Give an existential type with a type representation
data TermEx where
  MkTerm :: R a - Term a - TermEx

-- we use Weirich's higher-order type-safe cast to avoid deep  
traversals

-- one can replace the type_cast with a more simple traversal-based
-- version.


...complicated higher order stuff...

For instance:

 data a :==: b where
   Refl :: a :==: a

 (===) :: Monad m = R a - R b - m (a :==: b)
 Rint  === Rint  = return Refl
 Rbool  === Rbool = return Refl
 Rpair a b === Rpair c d = do
 Refl - a === c
 Refl - b === d
 return Refl
 a === b = fail $ show a ++  =/=  ++ show b

 cast :: a :==: b - c a - c b
 cast Refl x = x

In particular one wants to extract the Term part of a TermEx:

 getTerm :: Monad m = TermEx - R a - m (Term a)
 getTerm (MkTerm r' t) r = do
   Refl - r === r'
   return t

/ Ulf

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

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

[Greg Buchholz]

Thanks to everyone who replied (especially Dimitrios Vytiniotis and
Joost Visser).  I now know the standard way to write the GADT parser.
But I'm still curious if anyone has comments pertaining to the version
using type classes.  It seems so close to doing what we want, and it is
pretty straightforward to implement.  The best way I can think to
describe it would be to say it uses the type system to find what it
should parse next, and dies of a pattern match failure if something
unexpected shows up, instead of checking to see if we can assemble a
type safe tree from pre-parsed parts (does that make any sense?).

I'm curious if there could be a small change to the type system to
make the fully general my_read possible, or if it suffers from an
incurable defect. 

Thanks, 
Greg Buchholz 

 {-# OPTIONS -fglasgow-exts #-}  
 
 main = print test
 
 test :: Int 
 test = eval.my_read.read $
 (EIf (EIsZ (ELit 0))   ++
  (EInc (ELit 1))   ++
  (EFst (EPair (ELit 42)++
   (ELit 43
 
 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 :: Term (Int,Int))
 my_read (ESnd a)= Snd (my_read a :: Term (Int,Int))
 
 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 :: Term (Bool,Bool))
 my_read (ESnd a)= Snd (my_read a :: Term (Bool,Bool))
 
 instance (MyRead a, MyRead x) = MyRead (a,x) 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)
 
 data Expr = ELit Int
   | EInc Expr
   | EIsZ Expr 
   | EPair Expr Expr
   | EIf Expr Expr Expr
   | EFst Expr
   | ESnd Expr
 deriving (Read,Show)
 
 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)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[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

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

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

[John Meacham]

I don't have an answer, but would be extremely interested in knowing
one!

one of my first attempts to use GADTs was to do something similar,
implemening the simple polymorphic lambda calculus in a way that
transformations could be guarenteed typesafe statically, but then when I
went and tried to write an interpreter, I couldn't figure out how to
read in programs to interpret.

it seems you would want something like first class existentials 'Exp
(exists a . a)' or something like that.

John

-- 
John Meacham - ⑆repetae.net⑆john⑈
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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


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

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

[Dimitrios Vytiniotis]

Just noticed Joost Visser's message but since I
had (essentially a very similar) response I thought I might
send it off as well ... It includes the conditional cases.

Regards,
-d


{-# OPTIONS_GHC -fglasgow-exts #-}

module Main where

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

data Expr = ELit Int
  | EInc Expr
  | EIsZ Expr
  | EPair Expr Expr
  | EIf Expr Expr Expr
  | EFst Expr
  | ESnd Expr
deriving (Read,Show)

-- Give a GADT for representation types
data R a where
  Rint :: R Int
  Rbool :: R Bool
  Rpair :: R a - R b - R (a,b)

-- Give an existential type with a type representation
data TermEx where
  MkTerm :: R a - Term a - TermEx

-- we use Weirich's higher-order type-safe cast to avoid deep traversals
-- one can replace the type_cast with a more simple traversal-based
-- version.

data CL c a d = CL (c (d,a))
data CR c a d = CR (c (a,d))

type_cast :: forall a b c. R a - R b - c a - c b
type_cast Rint Rint x = x
type_cast Rbool Rbool x = x
type_cast (Rpair (ra::(R a0)) (rb::(R b0)))
(Rpair (ra'::(R a0')) (rb'::(R b0'))) x =
let g = (type_cast ra ra' :: ( (CL c b0)  a0 - (CL c b0) a0' ))
h = (type_cast rb rb' :: ( (CR c a0') b0 - (CR c a0') b0'))
in case (g (CL x)) of
 CL x' - case (h (CR x')) of
CR y' - y'
type_cast _ _ _  = error cannot cast!


-- give only the cases for Eif and Elit, the others are similar
my_read :: Expr - TermEx
my_read (ELit i) = MkTerm Rint (Lit i);
my_read (EIf p t e) =
case (my_read p) of
  MkTerm rb b -
  case rb of
Rbool -
   case (my_read t) of
 MkTerm r1 t1 -
   case (my_read e) of
 MkTerm r2 t2 -
MkTerm r2 (If b (type_cast r1 r2 t1) t2)
_ - error conditional not boolean!

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