[ 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
