[Haskell-cafe] Typed Lambda-Expressions with GADTs

1 Jan 2005


      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