idris-lang/Idris-dev — pull request #1478 by edwinb (2014-08-19 20:12:47+00:00)
Title: Uniqueness types

This adds experimental support for Uniqueness types.
If x : a, and a : UniqueType, then the type system guarantees that there is only one reference to x, so it can be safely destructively updated. UniqueType is, essentially, Type with a uniqueness flag set.

So we have the following types available in Idris source now:

Type - which is the type of all types with unrestricted sharing
UniqueType - which is the type of types for values which may not be shared
Type* - which is a type polymorphic in its uniqueness (and must therefore preserve uniqueness, i.e. no sharing).

There is much to do (including proper documentation), but this is now stable, and programs which don't use UniqueType work as before.