Breaking region nesting in type-and-effect systems?

Type and effect systems have been studied in the context of region-based memory management. The Disciple compiler is a recent example of such a system, and the MLKit has had such a region system for quite some time.

Unfortunately, the Tofte-Talpin region calculus and its variants requires nested region lifetimes, which turns out to be unnatural for some programs.

Substructural region systems relax this restriction, by reifying region deallocation as an explicit operation. Instead, the authority to use and free a region is encapsulated in a linear capability.

It's not clear to me why this approach of separating deallocation to break the lifetime nesting would not work in a type and effect system. I'm not specifically referring to the Tofte-Talpin type and effect system, but whether some type and effect system could be designed which avoids the nesting restrictions. Has this been studied anywhere, and if not, what are the difficulties in designing such a type and effect system?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Hope this helps

The paper "Functional Translation of a Calculus of Capabilities" by Charguéraud and Pottier seems related. They use the annotated arrow à la Tofte-Talpin sometimes but it seems not always possible in their system where they have a richer type structure, coming from this ability to talk about regions/capabilities. They also compare the different approaches at the end, which may give you other pointers. They do not consider type inference there, which is maybe what you were primarily interested in, but i'm pretty sure they will.

Thanks for the reference.

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.

It can be done but...

If you think it through, you'll realize it's possible, but that the critical issue is tracking potential region aliases.

Consider the following simple function:

foo [r1 r2:rgn](x:int@r2) = free r1 ; !x

The function is parameterized by 2 regions r1 and r2, deallocates r1, and then reads a reference x in region r2. This code is only okay if we record a constraint that r1 != r2. So in general, your effect system is going to have to track inequalities for regions. And, assuming you want to support any sort of abstraction (e.g., H.O. functions or ADTs), you're going to also need support for sets of regions and tracking that a given region r is not in a set.

Finally, if allocation is separate, then you have to worry about generating and tracking fresh region names. That is, the type of "new_region" needs to reflect the fact that it's returning some r that is not equal to any other region that has already been allocated (else when you deallocate it, you won't be able to prove it's safe to access those other regions.)

All of these headaches are handled quite nicely by moving to a substructural type system. Matthew Fluet and I encoded this sort of alias tracking with a linear type system, but you could also go with something based on separation logic (as we do in Ynot).

Hope that helps...

The paper Matthieu provided

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. ;-)

Typing Safe Deallocation

Just came across Typing Safe Deallocation, which seems to be what I'm looking for.

Brief summary: Typing Safe Deallocation

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

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 e ffects anticipated by typing are not guaranteed to occur (though it is guaranteed that no other eff ect 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.

Statically safe resource deallocation

Greg Morrisett wrote

Finally, if allocation is separate, then you have to worry about generating and tracking fresh region names. That is, the type of "new_region" needs to reflect the fact that it's returning some r that is not equal to any other region t hat has already been allocated (else when you deallocate it, you won't be able to prove it's safe to access those other regions.)

They are all major headaches indeed. One can still implement safe
allocation in Haskell -- just to get a taste of the feature and whet
one's appetite for a better language. We can use a parameterized
`monad', which tracks, at the type level, the input and the output
states of a computation. An allocation operation will create a fresh
label (e.g., using a type-level Peano counter, also carried in the
type-state) for the created resource handle and add the label to the
type-state tracked by the monad. A deallocation operation will remove
the label from the type-state. Any operation on the resource has the
type with a type-level constraint that checks that the label of the
handle is a member of the type-state. The implementation of that idea
is still a major headache, and makes one wish for a `typekind'

It is even possible to use the technique when resource allocation and
deallocation depends on a dynamic test. For example, given two locks, we
assert one of them depending on a dynamic test. We can still statically
ensure the lock protocol (no lock can be asserted or released
twice and all asserted locks must be released at the end of the