This compiled with today's CVS GHC 6.3. I don't think you can do this
without GADTs.
module Expression where
{
data Sym env r where
{
FirstSym :: Sym (r,xx) r;
NextSym :: Sym env r -> Sym (a,env) r
};
runSym :: Sym env r -> env -> r;
runSym FirstSym (r,xx) = r;
runSym (NextSym var) (a,env) = runSym var env;
data OpenExpression env r where
{
Lambda :: OpenExpression (a,env) r -> OpenExpression env (a ->
r);
Symbol :: Sym env r -> OpenExpression env r;
Constant :: r -> OpenExpression env r;
Application :: OpenExpression env (a -> r) -> OpenExpression env
a -> OpenExpression env r
};
newtype Expression r = MkExpression (forall env. OpenExpression env
r);
runExpression :: Expression r -> r;
runExpression (MkExpression expr) = runOpenExpression expr () where
{
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;
};
sym0 :: OpenExpression (a,env) a;
sym0 = Symbol FirstSym;
sym1 :: OpenExpression (a,(b,env)) b;
sym1 = Symbol (NextSym FirstSym);
sym2 :: OpenExpression (a,(b,(c,env))) c;
sym2 = Symbol (NextSym (NextSym FirstSym));
k :: Expression (a -> b -> a);
-- k = \x.\y -> x = \.\.1
k = MkExpression (Lambda (Lambda sym1));
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)))));
}
--
Ashley Yakeley, Seattle WA
