Uniqueness Typing Simplified

Uniqueness Typing Simplified, by Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson.

We present a uniqueness type system that is simpler than both Clean’s uniqueness system and a system we proposed previously. The new type system is straightforward to implement and add to existing compilers, and can easily be extended with advanced features such as higher rank types and impredicativity. We describe our implementation in Morrow, an experimental functional language with both these features. Finally, we prove soundness of the core type system with respect to the call-by-need lambda calculus.

Uniqueness typing is related to linear typing, and their differences have been discussed here before. Linear types have many applications. This paper describes the difference between linear and unique types:

In linear logic, variables of a non-linear type can be coerced to a linear type (dereliction). Harrington phrases it well: in linear logic, "linear" means "will not be duplicated" whereas in uniqueness typing, "unique" means "has not been duplicated".

In contrast to other papers on substructural typing, such as Fluet's thesis Monadic and Substructural Type Systems for Region-Based Memory Management, this paper classifies uniqueness attributes by a kind system. This possibility was mentioned in Fluet's thesis as well, Section 4.2, footnote 8, though the technique used here seems somewhat different.

Uniqueness typing is generally used to tame side-effects in purely functional languages. Uniqueness types have also been contrasted with monads on LTU, which are also used to tame effects, among other things. One point not discussed in that thread, is how straightforward it is to compile each approach into efficient code. It seems clear that uniqueness types have a straightforward, efficient compilation, but it's not clear to me how efficient monads can be, and how much work is required to make them efficient. This may make uniqueness or substructural types more suitable for just-in-time compilers than monads.

Comment viewing options

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

licensing issues

We have integrated our type system in Morrow, an experimental functional language developed by Daan Leijen.

Unfortunately we cannot currently make the source available due to licensing issues.

Aw shucks!

Still, at least the

Still, at least the technique is well-documented so an open-source language should be able to take advantage of it.


Any news of it being incorporated anywhere 'main stream'?

oh license


Curious about uniqueness and monads

I've been thinking about the difficulty of compiling monads to imperative code. Has work been done on attempting to ascribe uniqueness types to variables in monads, with the intention of getting back some of the imperative performance.

Tail recursion and CPS buy an awful lot

I haven't specifically seen it, though the possibility's folklore. It's less a need than you might think if the monad implementation behaves in a tail-recursive fashion though - for a simple State monad for example the state will remain in the same position in memory, being overwritten when appropriate.