[clean-list] Re: relationship between uniqueness types and single-threaded lambda calculus?

Edsko de Vries devriese at cs.tcd.ie
Wed May 30 23:42:13 MEST 2007


Hi,

> John van Groningen <johnvg at cs.ru.nl> writes:
> > swap a i j
> > 	#! x = lookup a i
> > 	#! y = lookup a j
> > 	= update! (update! a i y) j x
> 
> Is this a valid Clean program?  I thought the Clean array operators
> had names like "select" instead of "lookup".  I'm having trouble with
> your download registration right now, so I can't try this out
> firsthand...

You don't need to register first (I've always found the website a bit
confusing in this regard). Just download Clean from

http://clean.cs.ru.nl/Download/main/main.htm

> I believe that in Clean, one would need to replace "lookup" with
> "uselect" to get the correct behavior.  However, the resulting program
> would no longer be type-correct -- "uselect" returns a pair.  So the
> program would need to be changed to "thread" the array through the
> lookups, somewhat like this:
> 
>  swap a i j
>  	#! (x,a1) = uselect a  i
>  	#! (y,a2) = uselect a1 j
>  	= update! (update! a2 i y) j x
> 
> Note that this increases the degree of sequentialization in the code
> (ie removes potential parallelism).  I believe that this threading is
> not necessary in STPLC.  So although #! and let* have similar
> meanings, STPLC can use let* in a way which does not appear to have an
> analogue in Clean (using #!)

The point John made (I think) was not that "lookup" and "update!" are
valid Clean functions, but rather, that they *could be* as far as the
type system is concerned.  

So, you *could* define a "lookup" and "update!" function just as they
are defined in in the STPLC calculus, and moreover, they'd be safe
(referentially transparent) and you could use them just like you'd use
them in the STPLC.

However, now that I think about it, I am not sure there really is a
semantic difference between using a "lookup" (using let* or #!) which
does not return a new array or using a "uselect" which returns a pair of
a new array and the item requested. You claim that the latter increases
the degree of sequentialization, but I'm not sure that is correct. The
point of let* x = e1 in e2 is that e1 _must_ be evaluated before e2 is
evaluated. From the paper (p334)

  "To do this we need three things: (..) (2) a way to sequence
  destructive updates (we will use let*, similar to let expressions but
  with a strict semantics)"

and a bit further when they explain the example you cite:

  "In our type system, simply changing the update's to update!'s will
  result in an ill-typed program, because in general there is no
  guarantee *that the lookup's wil be doe prior to the updates* [my
  emphasis]. However, if in addition we change let to let* we arrive at
  a well-typed program." 

So that means that semantically at least there is very little difference
between the two approaches (using "lookup" or using "uselect") - in both
cases, the lookups must happen before the update. Sorry if I repeat
myself, but make sure not to confuse the semantics of the particular
function "uselect" with the semantics of "lookup" - either could be
defined in Clean (and presumably also in the STPLC), and "let*" does in
fact seem to correspond quite closely (if not exactly - I'm not sure) to
"#!" in Clean. 

One more thought: let* allows to define a number of variables at the
same time, so that the two lookups for x and y could be done in either
order; I'm not sure #! in Clean allows that, although I suppose you
could probably do something like

  #! (x,y) = (lookup a i, lookup b j)

(not sure if that is valid Clean syntax, not tested - but I'd presume
so).

At this point (not knowing much more about STLPC than I did two days
ago) I would say: have a close look at polymorphism. Exactly how
polymorphic is the STPLC? And just to be cheeky and promote my own
research: how easy would it be to upgrade the STPLC to support arbitrary
rank types? (For uniqueness, see my TFP paper:

https://www.cs.tcd.ie/~devriese/pub/tfp07-paper.pdf

-- note: currently under consideration for publication, not published yet).

Edsko


More information about the clean-list mailing list