<div class="gmail_quote"><span class="Apple-style-span" style="border-collapse: collapse; -webkit-border-horizontal-spacing: 2px; -webkit-border-vertical-spacing: 2px; ">Artyom.</span></div><div class="gmail_quote"><span class="Apple-style-span" style="border-collapse: collapse; -webkit-border-horizontal-spacing: 2px; -webkit-border-vertical-spacing: 2px;"><br>
</span></div><div class="gmail_quote">I know what uniqueness means. What I meant is that the context in which uniqueness is used, for imperative sequences:<div><br></div><div>(y, s')= proc1 s x</div><div>(z, s'')= proc2 s' y</div>
<div>
.....</div><div><br></div><div>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.</div><div><br>
</div>
<div> 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.</div><div><br><div class="gmail_quote">2009/11/4 Artyom Shalkhakov <span dir="ltr"><<a href="mailto:artyom.shalkhakov@gmail.com" target="_blank">artyom.shalkhakov@gmail.com</a>></span><div>
<div></div><div class="h5"><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello,<br>
<br>
2009/11/4 Alberto G. Corona <<a href="mailto:agocorona@gmail.com" target="_blank">agocorona@gmail.com</a>>:<br>
<div>> The code executed by uniqueness types is somehow similar to the internal<br>
> code executed in a state monad (or in the case of IO, the IO monad). The<br>
> main difference is that the pairs of results (state, value) are explicitly<br>
> written in Clean by the programmer and the type sytem assures that the<br>
> order of executions makes sense at compile time, whereas in the case of the<br>
> state monad the sequence of instructions is lazily assembled at runtime in<br>
> the first step and executed in a second step. So there is a little more<br>
> overhead in haskell but the code is higher level.<br>
> Am I right?<br>
<br>
</div>I would rather say: code with uniqueness types allows for safe<br>
destructive updates.<br>
<br>
In Clean, a variable of unique type is ensured to have only one<br>
reference to it, at any time (that's why it's called "uniqueness<br>
typing"). So you can't write the code like this<br>
<br>
> f(x) + f(x)<br>
<br>
where f : *a -> int (x is of unique type), because x is clearly<br>
referenced two times here. What to do? Let f yield another reference<br>
to x! That also means that the old reference is not usable any more,<br>
since you have new one. f becomes:<br>
<br>
> f : *a -> (int, *a)<br>
<br>
and the code looks very familiar:<br>
<br>
> let (a, x') = f(x)<br>
> (b, x'') = f(x')<br>
> in a + b<br>
<br>
The function f can use destructive updates under the hood though it<br>
doesn't violate referential transparency. I bet you can you see why.<br>
<br>
I'd say that call-by-need is orthogonal to uniqueness typing.<br>
<br>
Cheers,<br>
<font color="#888888">Artyom Shalkhakov.<br>
</font></blockquote></div></div></div><br></div>
</div><br>