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