[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