Home » forums » LtU Forum

Type systems for acyclic terms

I've been looking for type systems which guarantee that terms are acyclic, in a context with mutability, of course. Any references? Thoughts?

By marco at 2018-02-08 04:14 | LtU Forum | previous forum topic | next forum topic | other blogs | 2921 reads

Comment viewing options

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

Linear types

Linear types (or some separation logics) can guarantee acyclicity in presence of mutability -- through the usual trick of "mutability or sharing, pick one". For example, if I remember correctly, the [Mezzo](http://protz.github.io/mezzo/) programming language has this property. This would also hold of the subset of Rust without reference-counted data (Rc, Arc).

By gasche at Thu, 2018-02-08 08:04 | login or register to post comments

Don't want that

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

By marco at Thu, 2018-02-08 09:43 | login or register to post comments

Sized types

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

By gasche at Thu, 2018-02-08 17:51 | login or register to post comments

Something like that

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!

By marco at Fri, 2018-02-09 08:26 | login or register to post comments