On 10/4/07, Pasqualino 'Titto' Assini <[EMAIL PROTECTED]> wrote: > It does not seem to be possible to define "typecheck" on EApp in a generic way > and is also not possible to distinguish between the different cases:
You want to pattern-match on types and the easiest way to do it is to introduce a witness GADT for types, something like: data Type a where TString :: Type String TFun :: Type a -> Type b -> Type (a -> b) ... It will be useful to write function: termType :: Term a -> Type a You'll probably have to decorate Term constructors with Type's in a few places. As for the typecheck function - it has to be able to return any Term type, dynamically. Existentially quantificated data constructors will be handy here. Here's what I use: data Dyn c = forall a. Dyn (c a) withDyn :: Dyn c -> (forall a. c a -> b) -> b withDyn (Dyn e) f = f e Your typecheck function can have type: typecheck :: Exp -> Dyn Term or rather typecheck :: Exp -> Maybe (Dyn Term) You define it recursively, getting Dyn Term for subexpressions, checking their types, building bigger Dyn Terms, and so on. You'll probably need some other support functions for working with Dyn and Type - at least I did. I think something similar is presented in Hinze's paper, recommended by Dominic. Best regards Tomasz _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe