1 (* A suspension, or thunk, is a delayed computation. A thunk is duplicable:
 2    multiple threads may request its result. The type system guarantees that
 3    the delayed computation is performed at most once. *)
 4 
 5 abstract thunk +a
 6 fact duplicable (thunk a)
 7 
 8 (* Creation. *)
 9 
10 (* The delayed computation, represented by the function [f], may need a
11    permission [p] in order to run. This permission must be passed to
12    [create] when the thunk is created. Because [f] consumes [p] and
13    [create] is given only one copy of [p], we know that [f] will be
14    invoked at most once. In other words, [f] is a one-shot function. *)
15 
16 val create: [a, p: perm] duplicable a => (
17   f: (| consumes p) -> a
18 | consumes p
19 ) -> thunk a
20 
21 (* Demand. *)
22 
23 val force: [a] thunk a -> a
24