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