[Haskell-cafe] Transforming a ADT to a GADT

[Erik Hesselink]

On Fri, Sep 14, 2012 at 2:27 PM, Erik Hesselink <hesselink at gmail.com> wrote:
> In general, I think you have to work inside an existential. So you
> hide the type of the parsed Term inside an existential. If you want to
> apply functions to this Term, you unpack, call the function, and
> repack.

Maybe I should expand what I mean by this. Let's say you have:

      data SomeTerm where
        SomeTerm :: Term a -> SomeTerm

Your typecheck function goes:

    typecheck :: Exp -> SomeTerm

and you want to apply:

    transform :: Term t -> Term t

You should do something like:

    f (SomeTerm t) = SomeTerm (transform t)

Or, more generally:

    onSomeTerm :: (forall t. Term t -> Term t) -> SomeTerm -> SomeTerm
    onSomeTerm f (SomeTerm t) =  SomeTerm (f t)

Erik