uniqueness typing

Dana Harrington dgharrin@ucalgary.ca
Tue, 12 Mar 2002 15:52:29 -0700


Andre W B Furtado wrote:
> I found the following text when visiting the Clean (a functional language)
> site:
> 
> "Clean is the only functional language in the world which has a special type
> system, uniqueness typing. It enables to update function arguments
> destructively retaining the purity of the language."

I believe Mercury borrowed their uniqueness type (mode) system from 
Clean. But since Mercury is functional/logical then I guess its still 
true that Clean is the only functional language with a uniqueness type 
system.

> Then I have some questions:
> 1. Can anyone explain what does "update function arguments destructively"
> mean?

Uniquely typed values are guaranteed to be referenced at most once under 
program evaluation, these values can be modified in-place. As an 
example, suppose I have an array and I want to modify an element.  In 
general I need to create a whole new copy of the array in order to make 
the modification since there may be other places in the program that 
require access to the old array.  However, if I know that the old array 
has no other references (because the array has a unique type) then I do 
not need to make a copy, I can just modify the original array.  This has 
obvious efficiency benefits.

> 2. If this is a desirable thing, why does Haskell not implement it?

- Uniqueness types, of course, require replacing the type system, this 
is a non-trivial task,
- Destructive updates can already be accomplished with compiler 
supported libraries using monads,
- Uniqueness types invalidate some program transformations.

On the other hand I think uniqueness types are quite useful. 
Particularly as they allow much more flexible interaction between 
mutable data-structures than monadic approaches.  I don't know of any 
concrete reasons a uniqueness type system couldn't be added to Haskell.

This seems like a fine time to insert a plug for my Master's thesis, 
which describes a denotational semantics of uniqueness types:
http://www.cpsc.ucalgary.ca/~danaha/uniqueness-types.ps

Dana