Reified Lambda Functions

[Neal Gafter]

On Tue, Jan 19, 2010 at 1:39 PM, Howard Lovatt <howard.lovatt at iee.org> wrote:
> 2010/1/17 Neal Gafter <neal at gafter.com>
>> I still believe there are fatal errors in your approach.
>
> It is not clear to me where you think the errors are, perhaps you
> could elaborate.

Sure: I don't believe your scheme can be shown to result in a type
system that is sound (avoids heap pollution).  Soundness in this case
is the property that every variable of function type refers to a
lambda that is a subtype of the variable's type, or is the result of a
series of your cast operations from a lambda that is a subtype of the
variable's type, or is null.  I can't tell you "where the errors are"
because soundness is a global property of a type system, not a local
one.

> The examples you have provided have proved productive in expanding all the
> corner cases (thanks)

I don't believe that the problems exposed so far are "all the corner
cases", they are just a few.

> but the fundamentals have not changed. Effectively I
> have just applied the same techniques to more situations; which is very
> encouraging. If you have more examples that would be useful.

I think it is time to produce more formal evidence of soundness,
rather than relying on absence of counterexamples.  I believe you'll
find that further difficult examples will arise naturally from that
effort.

>> I think what you need to do is provide a proof
>> - or at least show how a proof can be constructed - that demonstrates
>> that, using this approach, a variable of function type cannot be made
>> to store a reference (or a reference that is the result of one of your
>> cast functions) to a lambda that is incompatible with the variable's
>> type.
>
> The basic idea is that you can reify a lambda based on compiler knowledge of
> what the type is (and there is a runtime check that the compiler is
> correct). This doesn't seem to me to be an outrageous idea, the only way it
> gets the types wrong are due to *existing* holes in the type system and then
> these are caught by an extra runtime check. Were do you feel that an extra
> type hole is introduced.

"Where do you feel that an extra type hole is introduced" is not a
proper soundness argument for a type system.  If you try to construct
a soundness argument, I suspect you'll find further problem areas
(e.g. the interaction of covariant arrays and function types).

Cheers,
Neal