Re: [TYPES] Purely functional programming with reference cells

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On Wed, Nov 5, 2014 at 10:48 AM, Francois Pottier <[email protected]
> wrote:

> Just a little remark. I am not sure what you mean by "this subsumes
> laziness".
> In fact, it seems that if you want to implement "laziness" (that is,
> thunks)
> using reference cells, then you need to be able to write a value into a
> previously empty cell. So, you need to relax your condition and allow the
> new
> value to be "more defined" (in some sense) than the old value.
>

I do not see why the cell would ever have to be empty. Why would the
following implementation not work?

type 'a cell = Susp of (unit -> 'a) | Unsusp of 'a
type 'a t = 'a cell ref

let susp f x = ref (Susp (fun () -> f x))

let unsusp x = ref (Unsusp x)

let force l =
  match !l with
  | Susp f -> let x = f () in l := Unsusp x; x
  | Unsusp x -> x

At no point in time is the cell empty, assuming the operation that updates
it is atomic. It always contains exactly the information required (either a
function or the result of evaluating it) to compute its only observable
result (the result of forcing the thunk).

More generally, I think you might be interested by the paper "LVars:
> Lattice-based Data Structures for Deterministic Parallelism", by
> Lindsey Kuper and Ryan R. Newton.
>

I have come across that paper before, but I have not read it particularly
carefully. If I recall correctly, the main idea is that a result whose type
is the carrier of a join semilattice can be computed beginning from a state
of no information (the semilattice's bottom) and spawning parallel tasks
that add pieces of information (the semilattice's join, although so far
only a commutative monoid is required). Furthermore, at any point, any of
the parallel tasks can query whether a particular piece of information has
already been added (this is the part that requires a semilattice).

Is there anything I have missed? In any case, I will give it another read.
Thanks for the pointer!

-- 
Eduardo León