I know what uniqueness means. What I meant is that the context in which uniqueness is used, for imperative sequences:
(y, s')= proc1 s x
(z, s'')= proc2 s' y
.....
is essentially the same sequence as if we rewrite an state monad to make the state explicit. When the state is the "world" state, then it is similar to the IO monad.
An state monad forces a single use of the implicit state variable too (unless you pass it trough the next step without changes. That can be done in Clean too.
2009/11/4 Artyom Shalkhakov
<artyom.shalkhakov@gmail.com>
Hello,
2009/11/4 Alberto G. Corona <agocorona@gmail.com>:
> The code executed by uniqueness types is somehow similar to the internal
> code executed in a state monad (or in the case of IO, the IO monad). The
> main difference is that the pairs of results (state, value) are explicitly
> written in Clean by the programmer and the type sytem assures that the
> order of executions makes sense at compile time, whereas in the case of the
> state monad the sequence of instructions is lazily assembled at runtime in
> the first step and executed in a second step. So there is a little more
> overhead in haskell but the code is higher level.
> Am I right?
I would rather say: code with uniqueness types allows for safe
destructive updates.
In Clean, a variable of unique type is ensured to have only one
reference to it, at any time (that's why it's called "uniqueness
typing"). So you can't write the code like this
> f(x) + f(x)
where f : *a -> int (x is of unique type), because x is clearly
referenced two times here. What to do? Let f yield another reference
to x! That also means that the old reference is not usable any more,
since you have new one. f becomes:
> f : *a -> (int, *a)
and the code looks very familiar:
> let (a, x') = f(x)
> (b, x'') = f(x')
> in a + b
The function f can use destructive updates under the hood though it
doesn't violate referential transparency. I bet you can you see why.
I'd say that call-by-need is orthogonal to uniqueness typing.
Cheers,
Artyom Shalkhakov.