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

[oleg at pobox.com]

Ashley Yakeley wrote on the first day of 2005:
> This compiled with today's CVS GHC 6.3. I don't think you can do this
> without GADTs.

It seems we can do without GADT -- roughly with the same syntax
(actually, the syntax of expressions is identical -- types differ and
we have to write `signatures' -- i.e., instance declarations). Tested
with GHC 6.2.1.

I especially liked the example
	test3 = (runExpression s) (runExpression k) (runExpression k)
below. Its inferred type is

	-- :t test3: 
	-- test3 :: forall r. r -> r 

so, SKK must be the identity (if it terminates, that is)

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

module Expression where

-- data Sym env r where
--     FirstSym :: Sym (r,xx) r
--     NextSym :: Sym env r -> Sym (a,env) r

class SymT t env r
data FirstSym = FirstSym deriving Show
data NextSym t = NextSym t deriving Show

instance SymT FirstSym (r,xx) r
instance SymT t env r => SymT (NextSym t) (a,env) r

class SymT t env r => RunSym t env r | t env -> r where
    runSym :: t -> env -> r

-- runSym FirstSym (r,xx) = r;
instance RunSym FirstSym (r,xx) r where
    runSym _ (r,xx) = r

instance RunSym var env r => RunSym (NextSym var) (a,env) r where
    runSym (NextSym var) (a,env) = runSym var env -- the code literally



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

-- Frankly speaking, the class OpenExpression below isn't necessary
-- We could have gotten by with just RunOpenExpression
-- However, the class OpenExpression makes it easy to formulate
-- the constraint for well-formed expressions.
-- We can use that constraint elsewhere.

class OpenExpression t env r
data Lambda a t = Lambda t deriving Show
data Symbol t = Symbol t deriving Show
data Constant r = Constant r deriving Show
data Application a t1 t2 = Application t1 t2 deriving Show


instance OpenExpression t (a,env) r => OpenExpression (Lambda a t) env (a->r)
instance SymT t env r => OpenExpression (Symbol t) env r
instance OpenExpression (Constant r) env r
instance (OpenExpression t1 env (a->r),
	  OpenExpression t2 env a)
    => OpenExpression (Application a t1 t2) env r


class OpenExpression t env a => RunOpenExpression t env a | t env -> a
--class RunOpenExpression t env a | t env -> a
    where
    runOpenExpression :: t -> env -> a

instance RunOpenExpression (Constant r) env r where
    runOpenExpression (Constant r) _ = r

instance (RunOpenExpression t1 env (b->a),
	  RunOpenExpression t2 env b)
    => RunOpenExpression (Application b t1 t2) env a where
    runOpenExpression (Application t1 t2) env = 
	(runOpenExpression t1 env)
	(runOpenExpression t2 env)
    
instance RunSym var env r => RunOpenExpression (Symbol var) env r where
    runOpenExpression (Symbol var) env = runSym var env

instance RunOpenExpression t (a,env) r
    => RunOpenExpression (Lambda a t) env (a->r) where
    runOpenExpression (Lambda exp) env = \a -> runOpenExpression exp (a,env)

newtype Expression t r = MkExpression (forall env. 
				       RunOpenExpression t env r => t)

runExpression (MkExpression e) = runOpenExpression e ()


sym0 = Symbol FirstSym

sym1 = Symbol (NextSym FirstSym)

sym2 = Symbol (NextSym (NextSym FirstSym))

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

test1 = (runExpression k) sym0 sym2
test2 = (runExpression k) sym2 sym0

test3 = (runExpression s) (runExpression k) (runExpression k)
-- Note: That can only be the identity!
-- :t test3: 
-- test3 :: forall r. r -> r 

test3' = test3 "It's the identity!!! Look at the type!!!"