Lambda the Ultimate

Thanks for the reference. I'm reading it now, but this system seems to have a severe deficiency: regions are not heterogenous, but homogenous. The authors state that it is unknown whether the former can encode the latter.

The paper Matthieu provided is finally getting through to me. Introducing linear capabilities and separating them from values allows arbitrary aliasing of the value, but not the capability itself. I can see how this would permit more flexible program structures, where references can be widely shared, but only updated by the owner.

The paper also clearly explains how uniqueness/linear types are, in a sense, more general than effect typing. In short, an effectful function f1 with effect C, ie. val f: t1-C->t2, essentially maps to f: t1*C -> t2*C in a uniqueness/linear type system. However, in the latter, we need not return the same C.

I had also been confused about the 'get' signature for references requiring the region capability, as I don't see the problem in retrieving value from a reference without the capability. But I see now that references are an existential package, and so require the capability to open it. There is no fundamental safety issue I'm missing though right?

Unfortunately, I'm not very familiar at all with separation logic. They reference it in the above paper, but only to mention that their approach is similar in some sense. I am perusing the Ynot papers now. I am trying to stay away from dependently typed languages though, if only because I know they'll seduce me from my immediate goals. ;-)

I've now read through this once, so here's my brief summary. The paper introduces "negative" deallocation effects, in addition to the usual "positive" usage effects in its type and effect system. So an effect constitutes a (positive effect, negative effect) pair, where effects are sets of region names.

The language contains a 'new' operation which introduces a region name for an expression, and incurring a positive effect. It also provides a 'dispose' operation, which takes a region name and immediately frees it, incurring a negative effect. Safe deallocation consists of ensuring that no positive or negative effects of a subexpression name a region listed in the negative effects of a parent expression. This prevents use of and disposal of an already disposed region.

They conclude by stating that an extended version of this work will deal with region polymorphism and aliasing. This work does not support explicit allocation however, though I'm unclear on how significant this problem is in practice. The dispose operation can delete the name before the end of scope, so I would think this is sufficient. Please correct me if I'm wrong!

I just noticed this:

In the rule for (new ρ in e), we could require ρ ∈ ρ^-, in order to ensure that the region assigned to ρ has been disposed of when the evaluation exits its scope, but this would be just an indication, because the effects anticipated by typing are not guaranteed to occur (though it is guaranteed that no other effect can possibly occur).

So we cannot ensure that all regions have been reclaimed once a progam terminates? This would seem to strongly argue for some sort of linear type system which would ensure a region is properly reclaimed.

Is there a more refined type and effects system that can track actual effects more closely? This seems like an important property, since the effects on an if branch could differ wildly, and conservatively assuming the effects from both branches would be of only limited use beyond a certain level of complexity.