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

[Tomasz Zielonka]

On 10/4/07, Pasqualino 'Titto' Assini <tittoassini at gmail.com> 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