22 Jan
2007
22 Jan
'07
11:11 p.m.
On 1/22/07, Benjamin Franksen <benjamin.franksen@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