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

[Pasqualino 'Titto' Assini]

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