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