Lambda the Ultimate

I want acyclic terms, this is too restrictive. The goal is to have sharing, which can be reference counted, but avoid cycles.

Sized types have also been proposed to avoid self-reference issues. I don't know of applications of sized types to a language with mutation, but I think they would probably work for what you want to do. The idea is to track, for each value in your system, a kind of "ghost parameter" in its static type that describes its "size" or "age", with the invariant that, in a complex structure, sub-structures are always smaller/younger than their parent (the invariant is obtained when creating the super-structure or when observing the children of a structure, and checked statically at mutation time). You then need size-polymorphism and good inference of sizes for programming to be practical, but that seems compatible with both sharing and mutation.

(Sized types are used in this way to avoid universe inconsistencies in type theories, and have also been proposed to deal with non-termination of recursive functions.)

Yah. I could think of something like that too. But I expect I would quickly find out it isn't worth it since you run into Rice too easily. It's probably a nontrivial property to track, relates too much to program behavior because everybody can write a 'if (unproven_theorem_is_true) create_a_cycle;' statement.

Just checking for prior work. But thanks!