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

[Edsko de Vries]

Hi Adam,

Let's see if I have any better luck than you trying to post long emails :)

> Edsko de Vries <devriese at cs.tcd.ie> writes:
> > 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).
> 
> Wow, this is really great!  It definitely cleans up a lot of the
> "rough edges" in previous presentations of unique types.  I think
> you're really on to something here with the idea of using multiple
> boolean-valued variables with propositional constraints rather than a
> single type-valued variable with subtyping constraints.

Thanks :)

> > 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.
> 
> Hrm, I strongly doubt this.  Are you saying that you could write a
> "uselect" that doesn't return a reference to the unique array?  What
> would its type be (with uniqueness annotations)?

Actually, it already exists and is called "select" (see _SystemArray.dcl for
its type). Here is a valid Clean program that corresponds to the example you
mentioned:

module SwapExample

import StdEnv

swap :: *{a} Int Int -> *{a}
swap arr i j
    #! a = select 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 think this example demonstrates than you can in fact do this in Clean.
Moreover, no particular ordering is implied between the two selects, so that
they could in principle be done in parallel. Now, the Clean book does not
mention any special typing rule for #!, and I don't think the papers mention it
either, but I'm pretty use the typing rule must be very similar to the rule for
"let*" in the STPLC (so both the static and dynamic semantics (roughly?)
correspond).

As far as your proposal is concerned, I'm not sure I get you. Perhaps some more examples would help. One remark though regarding partial application:

> Note that I have reversed the order of the arguments to "lookup" so
> that it never returns a closure with a captured reference to "a".

I am not completely sure what you mean by "captured". If by captured you mean
"there is a reference to the argument from a function closure", then that is
captured by the fact that the function is unique (in Clean), or (much more
directly) by the closure attribute underneath the arrow (in my proposal). This is exactly why in my system the function "const" has type

  const :: a:u <uf,!> (b:v <uf',u> a:u)
  const x y = x

That is, a partial application of const returns a function closure, and that
function closure has an element with uniqueness attribute "u".

Edsko