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 *)