[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs

[Martin Sulzmann]

Hi,

So far, we've seen GADTs encodings based on
the ideo of turning each (value) pattern clause 
into an (type class) instance declaration.

There's also another encoding based on the idea
of providing (value) evidence for type equality.
(Explored by example by quite a few people,
see upcoming paper for references).

A formal result can be found here:
A Systematic Translation of Guarded Recursive Data Types to
Existential Types
by Martin Sulzmann and Meng Wang
http://www.comp.nus.edu.sg/~sulzmann/

Example encodings for some of the
examples we've seen so far can be found below.

Martin

----- Examples encodings -----------

{-# OPTIONS -fglasgow-exts #-}

data E a b = E (a->b,b->a)
{-
data Sym env r 
    = forall xx.(env = (r,xx)) => FirstSym
    | forall env' a.(env=(a,env')) => NextSym (Sym env' r)
-}

data Sym env r 
    = forall xx. FirstSym (E env (r,xx))
    | forall env' a. NextSym (Sym env' r) (E env (a,env'))
{-
runSym :: Sym env r -> env -> r
runSym FirstSym (r,xx) = r
runSym (NextSym var) (a,env) = runSym var env
-}
-- have to play the pair trick because pattern doesn't match
runSym :: Sym env r -> env -> r
runSym (FirstSym (E (g,h))) pair {-(r,xx)-} = (fst (g pair))
runSym (NextSym var (E (g,h))) pair {-(a,env)-} = runSym var (snd (g
pair))

{-
data OpenExpression env r
    = forall a r'.(r=(a->r')) => Lambda (OpenExpression (a',env) r')
    | forall r'. Symbol (Sym env r)
    | Constant r
    | forall a. Lambda (OpenExpression env (a -> r))
                       (OpenExpression env a)
-}

data OpenExpression env r
    = forall a r'. Lambda (OpenExpression (a,env) r') (E r (a->r'))
    | Symbol (Sym env r)
    | Constant r
    | forall a. Application (OpenExpression env (a -> r))
                            (OpenExpression env a)
{-
runOpenExpression :: OpenExpression env a -> env -> a
runOpenExpression (Constant r) _ = r
runOpenExpression (Application ar a) env = (runOpenExpression ar env)
(runOpenExpression a env)
runOpenExpression (Lambda exp) env = \a -> runOpenExpression exp
(a,env)
runOpenExpression (Symbol var) env = runSym var env
-}

runOpenExpression :: OpenExpression env a -> env -> a
runOpenExpression (Constant r) _ = r
runOpenExpression (Application ar a) env = (runOpenExpression ar env)
(runOpenExpression a env)
runOpenExpression (Lambda exp (E (g,h))) env = h (\a ->
runOpenExpression exp (a,env))
runOpenExpression (Symbol var) env = runSym var env

newtype Expression r = MkExpression (forall env. OpenExpression env r)

runExpression :: Expression r -> r
runExpression (MkExpression expr) = runOpenExpression expr () 

eid = E (id,id)
sym0 :: OpenExpression (a,env) a
sym0 = Symbol (FirstSym eid)

sym1 :: OpenExpression (a,(b,env)) b
sym1 = Symbol (NextSym (FirstSym eid) eid)

sym2 :: OpenExpression (a,(b,(c,env))) c
sym2 = Symbol (NextSym (NextSym (FirstSym eid) eid) eid)

    
k :: Expression (a -> b -> a)
-- k = \x.\y -> x = \.\.1
k = MkExpression (Lambda (Lambda sym1 eid) eid)

s :: Expression ((a -> b -> c) -> (a -> b) -> a -> c)
-- s = \x.\y.\z -> x z (y z) = \.\.\.2 0 (1 0)
s = MkExpression (Lambda (Lambda (Lambda (Application (Application
sym2 sym0) (Application sym1 sym0)) eid) eid) eid)


test3 = (runExpression s) (runExpression k) (runExpression k)
						   {-# OPTIONS
-fglasgow-exts #-}
import Control.Monad.State (MonadState (..))
data E a b = E (a->b,b->a)

data State s a
  = forall b. Bind (State s a) (a -> State s b) (E a b)
  | Return a 
  | Get (E a s)
  | Put s (E a ()) 

runState :: State s a -> s -> (s,a)
runState (Return a) s = (s,a)
runState (Get (E (g,h))) s = (s,(h s))
runState (Put s (E (g,h))) _ = (s,(h ()))
runState (Bind (Return a) k (E (g,h))) s 
  = let --cast :: State s b -> State s a
	cast (Return a) = Return (h a)
	cast (Get (E (g',h'))) =  Get (E (\x-> g' (g x),\x->h (h' x))) 

	cast (Put s (E (g',h'))) = Put s (E (\x->g' (g x),\x->h (h'
x)))
	cast (Bind s' k' (E (g',h'))) = Bind (cast s') (\x->k' (g x))
(E (\x->g' (g x),\x->h (h' x)))
    in runState (cast (k a)) s
runState (Bind (Get (E (g1,h1))) k (E (g,h))) s 
  = let cast (Return a) = Return (h a)
	cast (Get (E (g',h'))) =  Get (E (\x-> g' (g x),\x->h (h' x))) 

	cast (Put s (E (g',h'))) = Put s (E (\x->g' (g x),\x->h (h'
x)))
	cast (Bind s' k' (E (g',h'))) = Bind (cast s') (\x->k' (g x))
(E (\x->g' (g x),\x->h (h' x)))
    in runState (cast (k (h1 s))) s
runState (Bind (Put s (E (g1,h1))) k (E (g,h))) _  
  = let cast (Return a) = Return (h a)
	cast (Get (E (g',h'))) =  Get (E (\x-> g' (g x),\x->h (h' x))) 

	cast (Put s (E (g',h'))) = Put s (E (\x->g' (g x),\x->h (h'
x)))
	cast (Bind s' k' (E (g',h'))) = Bind (cast s') (\x->k' (g x))
(E (\x->g' (g x),\x->h (h' x)))
    in runState (cast (k (h1 ()))) s
runState (Bind (Bind m k1 (E (g1,h1))) k2 (E (g,h))) s 
  = runState m (\x -> Bind (k1 x) k2 (E (g,h))) s 


{-
instance Monad (State s) where
    (>>=) = Bind
    return = Return

instance MonadState s (State s) where
    get = Get
    put = Put
-}