[Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs

[Ashley Yakeley]

In article <41D808C3.7010408 at cs.nott.ac.uk>,
 Conor McBride <ctm at cs.nott.ac.uk> wrote:

> The latter also means that the existential type encoding of 'some good
> term' doesn't give you a runnable term. There is thus no useful
> future-proof way of reflecting back from the type level to the term
> level. Any existential packaging fixes in advance the functionality
> which the hidden data can be given: you lose the generic functionality
> which real first-order data possesses, namely case analysis.

If I understand you correctly, without GADTs/datatype families, you 
cannot create Expression as a type-constructor without Oleg's auxiliary 
"t" argument that in fact encodes the structure of the expression. Is 
that right? I certainly can't see any way of getting rid of it: if, as 
you say, you existentially package it, the compiler can't deduce 
runnability.

-- 
Ashley Yakeley, Seattle WA