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

[Tomasz Zielonka]

On Mon, Jan 22, 2007 at 11:34:32PM +0100, Benjamin Franksen wrote:
> I would be interested whether you can not only /check/ well-typedness, but
> also /establish/ it, i.e. is it possible to have the input to the
> type-checker be an /untyped/ representation (such as obtained by parsing a
> program in text form) and the output be a typed one (or else a type error)?
> 
> 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.

You can do this with existential types and with higher-rank polymorphism (the
latter if you write your parser in CPS).

Best regards
Tomasz