Delimited continuations manipulate the control flow of programs. Similar to control structures like conditionals or loops they allow to deviate from a sequential flow of control.
We use exception handling as another example for control flow manipulation and later show how to implement it using delimited continuations. Finally, we show that nondeterminism can also be expressed using delimited continuations.
| /* | |
| * I add this to html files generated with pandoc. | |
| */ | |
| html { | |
| font-size: 100%; | |
| overflow-y: scroll; | |
| -webkit-text-size-adjust: 100%; | |
| -ms-text-size-adjust: 100%; | |
| } |
| type prop = | |
| True | | |
| Var of char | | |
| And of prop * prop | | |
| Not of prop | | |
| N of prop | | |
| U of prop * prop | |
| (* slow! *) | |
| let eventually p = U (True, p) |
| \documentclass[a4paper]{article} | |
| \input{./hoare.tex} | |
| \begin{document} | |
| \begin{hoare} | |
| \heq[a]{m * (a-b) > 0}{n := a-b}{m * n > 0}{\A} | |
| \heq[b]{1 * (a-b) > 0}{m := 1}{m * (a-b) > 0}{\A} | |
| \heq[c]{a > b}{m := 1}{m * (a-b) > 0}{\PrE(b)} | |
| \heq[d]{a > b}{m := 1; n := a-b}{m * n > 0}{\Seq(c, a)} | |
| \end{hoare} |
| #!/usr/bin/env sh | |
| # A .merlin must be present nearby the file. | |
| # With dune it can be generated by calling `dune build @check`. | |
| FILE="$1" | |
| dune build @check | |
| ocamlmerlin single dump -what ppxed-source -filename "$FILE" < "$FILE" | jq -r '.value' | ocamlformat --name="$FILE" - |
| type term = | |
| | Lam of (term -> term) | |
| | Pi of term * (term -> term) | |
| | Appl of term * term | |
| | Ann of term * term | |
| | FreeVar of int | |
| | Star | |
| | Box | |
| let unfurl lvl f = f (FreeVar lvl) |
