Hello,
2009/11/4 Alberto G. Corona
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.