(* A version of [make_counter] that has abstract, but not hidden, state. *) (* It returns a package of a function of type (| p) -> int -- that is, a function that needs a certain token p -- and the token p itself. This package is wrapped in an existential quantifier, {p : perm}, so the permission p is abstract. *) val make_counter () : {p : perm} ((| p) -> int | p) = let c = newref 0 in let postincrement (| c @ ref int) : int = let x = !c in c := x + 1; x in (* We return the function [postincrement]. The type-checker performs the existential type introduction, guessing that the witness for [p] is [c @ ref int]. *) postincrement (* The trouble is, we cannot share a counter produced by [make_counter] between two threads; or the two threads would have to coordinate and exchange the token [p]. *) open thread val () = let count = make_counter() in (* This incantation gives us a way of referring to [p]. *) let flex p : perm in assert count @ (| p) -> int; (* This thread creation instruction is accepted, but consumes [p]. *) spawn (fun (| consumes p) : () = let x = count() in () ); (* Thus, this (identical) instruction is rejected. For good reason: this program has a race condition! *) spawn (fun (| consumes p) : () = let x = count() in () ) (* Local Variables: compile-command: "mezzo counter.mz" End: *)