[clean-list] Re: relationship between uniqueness types and
single-threaded lambda calculus?
Edsko de Vries
devriese at cs.tcd.ie
Mon Jun 4 18:00:50 MEST 2007
Hey,
> > (1) The arr is assumed non-unique within the let* block, and
> > (2) The definitions in the let* block must be evaluated before the body
>
> Ah, this definitely helps a lot. By the way, is there any
> documentation of #! more detailed than the Clean 2.1 report? The
> report doesn't mention these aspects, though I think it would have
> helped a lot if it did.
Not that I know off, and to be honest, those rules were based on the
rules for let* rather than the rules for #! (since I have never seen the
rules for #! :-) For example, consider
Linear types can change the world!
Philip Wadler. In M. Broy and C. Jones, editors, Programming Concepts
and Methods, Sea of Galilee, Israel, April 1990. North Holland,
Amsterdam, 1990.
(Section 4 discussed "let!").
> > selectx :: {Int} Int -> StrictPair Int
>
> Thank you once again!
>
> One more question, however. Why does the compiler complain when I
> change selectx to this?
>
> selectx :: {Int} Int -> StrictPair {Int}
> selectx x y = Sp (select x y) {1,2}
>
> Does the compiler somehow use the knowledge that "a (StrictPair Int)
> cannot contain references to an {Int}" to reason about uniqueness?
> That would explain why it doesn't like the version of selectx which
> returns an (unrelated) {Int} as part of its result.
Now this one has me stumped. I have no idea. Here is an even simpler program:
module SwapExample
import StdEnv
selectx x y = (select x y, undef)
swap arr i j
#!
a = selectx arr i
b = select arr j
= (update (update arr i b) j (fst a))
Start :: *{Int}
Start = swap {1,2,3,4,5} 2 3
that program has a type error, but if I change the location of the "fst" to
module SwapExample
import StdEnv
selectx x y = (select x y, undef)
swap arr i j
#!
a = fst (selectx arr i)
b = select arr j
= (update (update arr i b) j a)
Start :: *{Int}
Start = swap {1,2,3,4,5} 2 3
I am not sure what is going on here; maybe somebody else what to jump in here?
Edsko
More information about the clean-list
mailing list