# The empty type; it has no values typename Void = [||]; # abstract computation over effect row e with return values of type a typename Comp(e::Row, a) = () ~e~> a; # helper functions for invoking Choose and Failure operations sig choose : (a, a) {Choose:Bool|_}~> a fun choose(x,y) {if (do Choose) {x} else {y}} sig fail : Comp({Failure:Void|_}, a) fun fail() {switch (do Failure) { }} # Coin toss model # The type Toss models the coins, while the computation toss # models a single coin toss. typename Toss = [|Heads|Tails|]; sig toss : Comp({Choose:Bool|_}, Toss) fun toss() { choose(Heads,Tails) } # The handler positive is an interpretation of 'choose'. It always selects true. sig positive : (Comp({Choose:Bool},a)) {}~> a handler positive(m) { case Choose(k) -> k(true) case Return(x) -> x } # The handler allResults enumerates the sample space by # invoking the continuation twice: First with true, then with false. sig allResults : (Comp({Choose:Bool},a)) {}~> [a] handler allResults(m) { case Choose(k) -> k(true) ++ k(false) case Return(x) -> [x] } # To apply the above handlers to toss in Links, type: # links> positive(toss); # links> allResults(toss); # # We extend the toss-model to a drunk coin toss. # A drunkard may fail to catch the coin after tossing it into the air. # Inside the drunk coin toss we embed our previous toss-model. sig drunkToss : Comp({Choose:Bool,Failure:Void|_},Toss) fun drunkToss() { if (choose(true,false)) { toss() } else { fail() } } # The Maybe type typename Maybe(a) = [|Just:(a)|Nothing|]; # The open handler maybeResult is an exception handler. # Exception handlers ignore the continuation parameter. sig maybeResult : (Comp({Failure:Void|e},a)) -> Comp({Failure{_}|e},Maybe(a)) open handler maybeResult(m) { case Failure(_) -> Nothing case Return(x) -> Just(x) } # At the Links toplevel type: # links> allResults(maybeResult(drunkToss)); # to enumerate all possible outcomes of a drunk toss. # Next we introduce randomness as an effect. sig rand : Comp({Rand:Float|_},Float) fun rand() {do Rand} # Now, we can give a random interpretation of choice. (To be precise: "Random" depends on our interpretation of randomness) # Assuming rand() draws a uniformly distributed float, this handler will interpret 'Choose' as true with probability ~0.5, # and false with probability ~0.5. sig randomResult : (Comp({Choose:Bool,Rand:Float|e},a)) -> Comp({Choose{_}, Rand:Float|e},a) open handler randomResult(m) { case Choose(k) -> k(rand() < 0.5) case Return(x) -> x } # We can interpret 'Rand' using Links' built-in random number generator. sig handleRandom : (Comp({Rand:Float|e},a)) -> Comp({Rand{_}|e},a) open handler handleRandom(m) { case Rand(k) -> k(random()) case Return(x) -> x } # At the Links' toplevel type: # links> handleRandom(randomResult(maybeResult(drunkToss)))(); # to evaluate the drunk toss under our random interpretation. (Run it multiple times!) # Under the previous interpretation we either get Just a result or Nothing. # We can give alternative interpretation of Failure which restarts the computation m # in the event of Failure. sig persevere : (Comp({Failure:Void|e},a)) -> Comp({Failure{_} |e},a) open handler persevere(m) { case Failure(_) -> persevere(m)() case Return(x) -> x } # Now type: # links> handleRandom(randomResult(persevere(drunkToss)))(); # to obtain either Heads or Tails from a drunk toss.