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

[Benjamin Franksen]

Tomasz Zielonka wrote:
> 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).

Right, now as you say it I remember the CPS trick. Used it myself some time
ago, though not even knowing the term 'CPS' back then ;-) It's a bit
cumbersome to use, though.

However, I haven't the slightest clue how to do this with existentials. Any
pointers (example/paper/wiki/whatever)?

Cheers
Ben