Lambda the Ultimate

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?

hi, when looking at a new post on a page that has a long discussion, it can be pretty hard to figure out what is the parent post it is replying to. if there were some more nuanced way of the hierarchy being shown that would be neat. dunno what that would be off the top of my head, but thought it could be a metric used when evaluating possible future new default look-and-feels.