1 open wref
  2 
  3 (* The identity function. We use a permission of the form [id @ b -> a]
  4    to encode the fact that [b] is a subtype of [a], and we use the
  5    function application [id x] when we wish to exploit this fact.
  6    This is a clumsy encoding, but it provides a proof-of-concept. *)
  7 
  8 (* No consumes keyword is required here, because we are dealing with
  9    duplicable types. *)
 10 
 11 val id [a] (consumes x: a) : a =
 12   x
 13 
 14 (* A suspension is either evaluated already or still suspended.
 15    In the former case, it contains just a result, of type [a].
 16    In the latter case, it contains the function [f] that was
 17    passed to [create], together with the permission [p] that
 18    [f] needs. This permission is existentially quantified. In
 19    other words, [f] is a one-shot function. *)
 20 
 21 data state a =
 22   | Evaluated { result: a }
 23   | Suspended { computation: {p: perm} ((|consumes p) -> a | p) }
 24 
 25 (* The state of a suspension is stored in a weak reference. The
 26    lock (which is part of the weak reference) ensures that the
 27    state of the suspension remains consistent even in the face
 28    of concurrent accesses. It also allows us to implement waiting
 29    until a result becomes available. *)
 30 
 31 (* The existential quantification over [b], which is a subtype of
 32    [a], is used to make [thunk] covariant in its parameter [a]. *)
 33 
 34 (* We might wish to store the information [duplicable a] as part
 35    of the definition of [thunk a]. This would allow us to remove
 36    the assumption [duplicable a => ...] in the type of [force].
 37    However, if we do that, [thunk] is no longer covariant in [a]!
 38    Subtle. But, actually, the constraint [id @ b -> a] encodes
 39    the fact that [b] is duplicable! So we can get rid of this
 40    assumption in the type of [force]. *)
 41 
 42 data thunk +a =
 43   | Thunk { thunk: {b} (wref (state b) | id @ b -> a) }
 44 
 45 (* TEMPORARY we need a type abbreviation here! *)
 46 
 47 (* Creation. *)
 48 
 49 (* The constraint [duplicable a] is required at construction time
 50    in order to construct a witness of [id @ a -> a]. *)
 51 
 52 val create [a, p : perm] duplicable a => (
 53   f: (|consumes p) -> a
 54 | consumes p
 55 ) : thunk a =
 56   let s : state a = Suspended { computation = f } in
 57   Thunk { thunk = new [state a] s }
 58 
 59 (* A custom unpacking function. This is another shortcoming of the
 60    system; if we had a generic mechanism for naming the variable
 61    that is introduced when an existential is unpacked, we would
 62    not need this. *)
 63 
 64 val unpack [a, c] (
 65   x: {b} (wref (state b) | id @ b -> a),
 66   f: [b] (wref (state b) | id @ b -> a) -> c
 67 ) : c =
 68   f x
 69 
 70 (* Evaluation. *)
 71 
 72 (* Using [wref::update] means that we hold the lock while the call to
 73    [s.computation] is in progress. As a result, if two calls to [force]
 74    occur concurrently, the second call will block until the first call
 75    is finished and has produced a result. This is the desired behavior. *)
 76 
 77 (* We do not need to explicitly require [duplicable a] because the
 78    constraint [id @ b -> a] actually encodes the fact that [b] is
 79    duplicable! Subtle. *)
 80 
 81 val force [a] (t: thunk a) : a =
 82   (* Unpack the existential, and let [b] stand for the witness. *)
 83   unpack (t.thunk, fun [b] (x: wref (state b) | id @ b -> a) : a =
 84     (* We get access to [t.thunk], under the name [x], at type
 85        [wref (state b)], where [b] is an unknown subtype of [a],
 86        as witnessed by the permission [id @ b -> a]. *)
 87     update (x, fun (consumes s: state b) : (state b, a) =
 88       (* We will now possibly update [x], by writing a new value
 89          of type [state b] into it, and return a result of type
 90          [b], which, by applying [id], we coerce to type [a]. *)
 91       match s with
 92       | Evaluated ->
 93           s, (id s.result)
 94       | Suspended ->
 95           let result : b = s.computation() in
 96           Evaluated { result = result }, id result
 97       end
 98     )
 99   )
100 
101 (*
102 Local Variables:
103 compile-command: "../mezzo lazy.mz"
104 End:
105 *)