[Haskell] Re: Even higher-order abstract syntax: typeclasses vs GADT

[Jim Apple]

On 1/22/07, Benjamin Franksen <benjamin.franksen at bessy.de> wrote:
> From my very limited understanding of these issues I would say it is not
> possible, neither with type-classes nor with G[AR]DTs because it would mean
> the return type of the function 'typecheck' would have to vary depending on
> the input data, hence you'd need a genuinely dependent type system for such
> a feat.

GADTs are darn near dependent types. Tim Sheard, James Hook, and
Nathan Linger caim that extensible kinds complete the equation in

"GADTs + Extensible Kinds = Dependent Programming"
http://web.cecs.pdx.edu/~sheard/papers/GADT+ExtKinds.ps

Jim