Hi, probably, I missed part of your problem, and there are quite a few concepts in your email, so I'll take it slowly. embedding untyped lambda into Haskell is fairly simple, as long as you don't want to print terms, or visualise reductions: data U = In { out :: U -> U } deriving Show this gives you a universal type, an embedding of unary functions into that type, and a projection of unary functions out of that type. so you can keep your haskell implementation busy evaluating embedded lambda terms like this one: (\x-> (out x) x) (In (\x-> (out x) x)) -- keep ready to hit ctrl-c as you say that you also want to represent the application structure, the type gets a little more complex (using the part of your Term type that is the image of correct sentences, implicitly encoding the types as well): -- just local quantification, no GADTs needed -- the type parameter encodes the type of the semantic object represented data SemTerm a = forall b . App (SemTerm (b->a)) (SemTerm b) | Sem a Unlike your Term type, this SemTerm type only holds type-correct applications and other semantic objects, such as primitive functions from your lexicon. there is no need to distinguish functions of different arities or to encode types explicitly (Z, U??, B??, ..), thanks to currying and embedded typing. so there is no need for an explosion of cases, either in the SemTerm type or in its application. just use Sem to inject your predefined functions/words, and App to apply them to arguments, and evaluation becomes simply: eval :: SemTerm a -> a eval (App f e) = (eval f) (eval e) eval (Sem e) = e so can can have your cake (representation) and eat it (embedded typing and evaluation): rv = Sem (reverse::String->String) tl = Sem tail pp = Sem (++) dot = Sem (.) hi = Sem "hi " there = Sem "there!" x = App rv (App (App (App dot tl) rv) (App (App pp hi) there)) main = print $ (x ,eval x) *Main> main ((<function> (((<function> <function>) <function>) ((<function> "hi ") "there!") )),"hi there") if you actually wanted to have representations of the function types as well, you could use Typeable, but typeOf only works for non-polymorphic types (so you can ask for 'typeOf x' or 'typeOf rv' in the attached code, but you would need to specialise the other function types to disambiguate the computation of type representations, as already done for rv). there are probably other requirements that stand against this representation (?), but at least it solves some of the issues you mentioned. and it uses fewer features (no GADTs, no template haskell). cheers, claus