Re: [Haskell-cafe] The "Exp -> Term a" problem (again), how to dynamically create (polymorphic) typed terms in Haskell ??

Hello Tomasz, thank you very much for your advice. Just a quick question, why using your own Dyn rather than Data.Dynamic? Regards, titto On Thursday 04 October 2007 08:57:11 Tomasz Zielonka wrote:

On 10/4/07, Pasqualino 'Titto' Assini 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