[Haskell-cafe] Transforming a ADT to a GADT

[oleg at okmij.org]

Florian Lorenzen wrote:
> Now, I'd like to have a function
> > typecheck :: Exp -> Maybe (Term t) 
> > typecheck exp = <...>
> that returns the GADT value corresponding to `exp' if `exp' is type
> correct.

Let us examine that type:
	typecheck :: forall t. Exp -> Maybe (Term t) 

Do you really mean that given expression exp, (typecheck exp) should
return a (Maybe (Term t)) value for any t whatsoever? In other words,
you are interested in a type-*checking* problem: given an expression _and_
given a type, return Just (Term t) if the given expression has the given
type. Both expression and the type are the input. Incidentally, this
problem is like `read': we give the read function a string
and we should tell it to which type to parse. If that is what you
mean, then the solution using Typeable will work (although you may
prefer avoiding Typeable -- in which case you should build type
witnesses on your own).


> that returns the GADT value corresponding to `exp' if `exp' is type
> correct.
Your comment suggests that you mean typecheck exp should return
(Just term) just in case `exp' is well-typed, that is, has _some_
type. The English formulation of the problem already points us towards 
an existential. The typechecking function should return (Just term)
and a witness of its type:

	typecheck :: Exp -> Sigma (t:Type) (Term t)

Then my
> data TypedTerm = forall ty. (Typ ty) (Term ty)

is an approximation of the Sigma type. As Erik Hesselink rightfully
pointed out, this type does not preclude type transformation
functions. Indeed you have to unpack and then repack. If you 
want to know the concrete type, you can pattern-match on the type
witness (Typ ty), to see if the inferred type is an Int, for example.


Chances are that you wanted the following

	typecheck :: {e:Exp} -> Result e
where Result e has the type (Just (Term t)) (with some t dependent on
e) if e is typeable, and Nothing otherwise. But this is a dependent
function type (Pi-type). No wonder we have to go through contortions
like Template Haskell to emulate dependent types in Haskell. Haskell
was not designed to be a dependently-typed language.