Title

Overview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Delimited Continuations for Everyone
Kenichi Asai
Ochanomizu University, Japan

September 28, 2017

Kenichi Asai

Delimited Continuations for Everyone

1/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Overview
Basics:What are continuations?
What are delimited continuations?
Examples:
How to discard continuations: times
How to extract continuations: append
How to reorder continuations: take, A-normalize
How to wrap continuations: printf, state monad
Speculation:
Toward delimited continuations in theorem proving
Kenichi Asai

Delimited Continuations for Everyone

2/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Early papers on control operators
Control/prompt
M. Felleisen [POPL 1988]“The Theory and Practice of First-Class Prompts”
Shift/reset
O. Danvy and A. Filinski [LFP 1990]“Abstracting Control”
O. Danvy and A. Filinski [MSCS 1992]“Representing Control,a Study of the CPS Transformation”
Kenichi Asai

Delimited Continuations for Everyone

3/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

What are continuations?
Continuation
The rest of the computation.
The current computation:
The rest of the computation:· · · inside [ ]· · · outside [ ]For example: 3 + [5 ∗ 2] − 1.
The current computation: 5 ∗ 2
The current continuation: 3 + [ · ] − 1.
“Given a value for [ · ], add 3 to it and subtract 1 fromthe sum.” i.e., fun x -> 3 + x - 1
Kenichi Asai

Delimited Continuations for Everyone

4/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

What are continuations?
As computation proceeds, continuation changes.
3 + [5 ∗ 2] − 1:
The current computation: 5 ∗ 2
The current continuation: 3 + [ · ] − 1.
[3 + 10] − 1:
The current computation: 3 + 10
The current continuation: [ · ] − 1.
[13 − 1]:
The current computation: 13 − 1
The current continuation: [ · ].
Kenichi Asai

Delimited Continuations for Everyone

5/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the current expressions, continuations,and their types.
1

5 * (2 * 3 + 3 * 4)2

(if 2 = 3 then "hello" else "hi")^ " world"

Kenichi Asai

Delimited Continuations for Everyone

6/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the current expressions, continuations,and their types.
1

5 * ([2 * 3] + 3 * 4)
[2 * 3] :5 * ([·] + 3 * 4) :2

(if 2 = 3 then "hello" else "hi")^ " world"

Kenichi Asai

Delimited Continuations for Everyone

6/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the current expressions, continuations,and their types.
1

5 * ([2 * 3] + 3 * 4)
[2 * 3] : int
5 * ([·] + 3 * 4) : int ->2(if 2 = 3 then "hello" else "hi")^ " world"

Kenichi Asai

Delimited Continuations for Everyone

6/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the current expressions, continuations,and their types.
1

5 * ([2 * 3] + 3 * 4)
[2 * 3] : int
5 * ([·] + 3 * 4) : int -> int2(if 2 = 3 then "hello" else "hi")^ " world"

Kenichi Asai

Delimited Continuations for Everyone

6/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the current expressions, continuations,and their types.
1

5 * ([2 * 3] + 3 * 4)
[2 * 3] : int
5 * ([·] + 3 * 4) : int -> int

2(if [2 = 3] then "hello" else "hi")^ " world"[2 = 3] :(if [·] ...) ^ " world" :Kenichi Asai

Delimited Continuations for Everyone

6/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the current expressions, continuations,and their types.
1

5 * ([2 * 3] + 3 * 4)
[2 * 3] : int
5 * ([·] + 3 * 4) : int -> int

2(if [2 = 3] then "hello" else "hi")^ " world"[2 = 3] : bool(if [·] ...) ^ " world" : bool ->Kenichi Asai

Delimited Continuations for Everyone

6/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the current expressions, continuations,and their types.
1

5 * ([2 * 3] + 3 * 4)
[2 * 3] : int
5 * ([·] + 3 * 4) : int -> int

2(if [2 = 3] then "hello" else "hi")^ " world"[2 = 3] : bool(if [·] ...) ^ " world" : bool -> string
Kenichi Asai

Delimited Continuations for Everyone

6/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

What are delimited continuations?
Delimited Continuation
The rest of the computation up to the delimiter.
Syntaxreset (fun () -> M )For example:
reset (fun () -> 3 + [5 * 2] ) - 1
The current computation: 5 ∗ 2
The current delimited continuation: 3 + [ · ].
Kenichi Asai

Delimited Continuations for Everyone

7/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the delimited continuations, and their types.
1

5 * reset (fun () -> [2 * 3] + 3 * 4)2reset (fun () ->if [2 = 3] then "hello" else "hi")^ " world"

Kenichi Asai

Delimited Continuations for Everyone

8/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the delimited continuations, and their types.
1

5 * reset (fun () -> [2 * 3] + 3 * 4)[·] + 3 * 4 :2reset (fun () ->if [2 = 3] then "hello" else "hi")^ " world"

Kenichi Asai

Delimited Continuations for Everyone

8/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the delimited continuations, and their types.
1

5 * reset (fun () -> [2 * 3] + 3 * 4)[·] + 3 * 4 : int -> int

2

reset (fun () ->if [2 = 3] then "hello" else "hi")^ " world"

Kenichi Asai

Delimited Continuations for Everyone

8/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the delimited continuations, and their types.
1

5 * reset (fun () -> [2 * 3] + 3 * 4)[·] + 3 * 4 : int -> int

2

reset (fun () ->if [2 = 3] then "hello" else "hi")^ " world"
if [·] then "hello" else "hi" :Kenichi Asai

Delimited Continuations for Everyone

8/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesIdentify the delimited continuations, and their types.
1

5 * reset (fun () -> [2 * 3] + 3 * 4)[·] + 3 * 4 : int -> int

2

reset (fun () ->if [2 = 3] then "hello" else "hi")^ " world"
if [·] then "hello" else "hi" :bool -> string
Kenichi Asai

Delimited Continuations for Everyone

8/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

shift
Syntax
shift (fun k -> M )It clears the current continuation,binds the cleared continuation to k, andexecutes the body M in the empty context.
For example:
reset (fun () -> 3 + [shift (fun k -> M )]) - 1
We will see a number of examples today.
Kenichi Asai

Delimited Continuations for Everyone

9/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

shift
Syntax
shift (fun k -> M )It clears the current continuation,binds the cleared continuation to k, andexecutes the body M in the empty context.
For example:
reset (fun () ->[shift (fun k -> M )]) - 1

We will see a number of examples today.
Kenichi Asai

Delimited Continuations for Everyone

9/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

shift
Syntax
shift (fun k -> M )It clears the current continuation,binds the cleared continuation to k, andexecutes the body M in the empty context.
For example:
reset (fun () ->[shift (fun k -> M )]) - 1
k = reset (fun () -> 3 + [·])

We will see a number of examples today.
Kenichi Asai

Delimited Continuations for Everyone

9/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

shift
Syntax
shift (fun k -> M )It clears the current continuation,binds the cleared continuation to k, andexecutes the body M in the empty context.
For example:
reset (fun () ->M ) - 1k = reset (fun () -> 3 + [·])

We will see a number of examples today.
Kenichi Asai

Delimited Continuations for Everyone

9/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to discard continuations
shift (fun _ -> M )Captured continuation is discarded.
The same as raising an exception.
For example:
reset (fun () -> 3 + shift (fun _ -> 2)) - 1
reset (fun () ->2 ) - 1k = reset (fun () -> 3 + [·])
2 - 1
1
Kenichi Asai

Delimited Continuations for Everyone

10/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesReplace [ · ] with shift (fun _ -> M ) for some M .
1

5 * reset (fun () -> [·] + 3 * 4)2reset (fun () ->if [·] then "hello" else "hi")^ " world"

We need the type of the context to fill in the body.
Kenichi Asai

Delimited Continuations for Everyone

11/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesReplace [ · ] with shift (fun _ -> M ) for some M .
1

5 * reset (fun () -> [·] + 3 * 4)shift (fun _ -> ?)2

reset (fun () ->if [·] then "hello" else "hi")^ " world"
shift (fun _ -> ?)We need the type of the context to fill in the body.
Kenichi Asai

Delimited Continuations for Everyone

11/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesReplace [ · ] with shift (fun _ -> M ) for some M .
1

2

5 * reset (fun () -> [·] + 3 * 4)shift (fun _ -> 3)❀ 15

reset (fun () ->if [·] then "hello" else "hi")^ " world"
shift (fun _ -> ?)We need the type of the context to fill in the body.
Kenichi Asai

Delimited Continuations for Everyone

11/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

ExamplesReplace [ · ] with shift (fun _ -> M ) for some M .
1

2

5 * reset (fun () -> [·] + 3 * 4)shift (fun _ -> 3)❀ 15

reset (fun () ->if [·] then "hello" else "hi")^ " world"
shift (fun _ -> "chao")❀ ”chao world”

We need the type of the context to fill in the body.
Kenichi Asai

Delimited Continuations for Everyone

11/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummarytimes
The following function multiplies elements of a list:(* times : int list -> int *)let rec times lst = match lst with[] -> 1| 0 :: rest -> ???
| first :: rest -> first * times rest
Fill in the ??? so that calls like the following will return0 without performing any multiplication.
reset (fun () -> times [1; 2; 0; 4])
Kenichi Asai

Delimited Continuations for Everyone

12/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Non-solution(* times : int list -> int *)let rec times lst = match lst with[] -> 1| 0 :: rest -> 0
| first :: rest -> first * times rest
It avoids traversing the rest of the list once 0 is found,but it still multiplies elements up to 0.
times [1; 2; 0; 4]-> 1 * times [2; 0; 4]-> 1 * 2 * times [0; 4]-> 1 * 2 * 0
Kenichi Asai

Delimited Continuations for Everyone

13/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Solution: discard the continuation(* times : int list => int *)let rec times lst = match lst with[] -> 1| 0 :: rest -> shift (fun _ -> 0)| first :: rest -> first * times rest
reset (fun () -> times [1; 2; 0; 4])-> reset (fun () -> 1 * times [2; 0; 4])-> reset (fun () -> 1 * 2 * times [0; 4])-> reset (fun () -> 0)-> 0
Kenichi Asai

Delimited Continuations for Everyone

14/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to extract continuations
shift (fun k -> k)Captured continuation is returned immediately.
For example: reset (fun () -> 3 + [...] - 1)
let f = reset (fun () ->3 + shift (fun k -> k) - 1)

Kenichi Asai

Delimited Continuations for Everyone

15/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to extract continuations
shift (fun k -> k)Captured continuation is returned immediately.
For example: reset (fun () -> 3 + [...] - 1)
let f = reset (fun () ->3 + shift (fun k -> k) - 1)-> let f = reset (fun () ->shift (fun k -> k))Kenichi Asai

Delimited Continuations for Everyone

15/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to extract continuations
shift (fun k -> k)Captured continuation is returned immediately.
For example: reset (fun () -> 3 + [...] - 1)
let f = reset (fun () ->3 + shift (fun k -> k) - 1)-> let f = reset (fun () ->shift (fun k -> k))where k = reset (fun () -> 3 + [...] - 1)

Kenichi Asai

Delimited Continuations for Everyone

15/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to extract continuations
shift (fun k -> k)Captured continuation is returned immediately.
For example: reset (fun () -> 3 + [...] - 1)
let f = reset (fun () ->3 + shift (fun k -> k) - 1)-> let f = reset (fun () ->k)where k = reset (fun () -> 3 + [...] - 1)
f 10
-> 12
Kenichi Asai

Delimited Continuations for Everyone

15/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Somewhat advanced example
Here is an identity function on a list:(* id : ’a list -> ’a list *)let rec id lst = match lst with[] -> [] (* A *)| first :: rest -> first :: id rest
By modifying the line (* A *), extract the continuation
at (* A *) when called as follows:
reset (fun () -> id [1; 2; 3])
What does the extracted continuation do?
Kenichi Asai

Delimited Continuations for Everyone

16/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Solution(* id : ’a list -> ’a list *)let rec id lst = match lst with[] -> shift (fun k -> k)| first :: rest -> first :: id rest
reset (fun () -> id [1; 2; 3])-> reset (fun () -> 1 :: id [2; 3])-> reset (fun () -> 1 :: 2 :: id [3])-> reset (fun () -> 1 :: 2 :: 3 :: id [])The captured cont. conses 3, 2, and 1 in this order.
Kenichi Asai

Delimited Continuations for Everyone

17/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Solution# let append123 =reset (fun () -> id [1; 2; 3]) ;;append123 : int list => int list = <fun># append123 [4; 5; 6] ;;- : int list = [1; 2; 3; 4; 5; 6]# let append lst1 =reset (fun () -> id lst1) ;;append : ’a list -> ’a list -> ’a list = <fun># append [1; 2; 3] [4; 5; 6];;
- : int list = [1; 2; 3; 4; 5; 6]
Kenichi Asai

Delimited Continuations for Everyone

18/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to reorder continuations: take
Given a list and a number n, return the given list where
the n-th element is moved to the front.
take [0; 1; 2; 3; 4] 0 = [0; 1; 2; 3; 4]take [0; 1; 2; 3; 4] 3 = [3; 0; 1; 2; 4]
take [0; 1; 2; 3; 4] 5 = [0; 1; 2; 3; 4]Seemingly easy:
The original list is almost reconstructed as is.
Only the designated element is moved.
but:
The n-th element might not exist.
When found, it must be carried over to the front.
Kenichi Asai

Delimited Continuations for Everyone

19/39

type found_t = Found of int | NotFound(* int list -> int -> found_t * int list *)let rec loop lst n = match lst with[] -> (NotFound, [])| first :: rest ->if n = 0 then (Found first, rest)
else let (found, l) = loop rest (n - 1) in(found, first :: l)(* take : int list -> int -> int list *)let take lst n = match loop lst n with
(NotFound, l) -> l
| (Found e, l) -> e :: lTitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Simpler solution(* loop : ’a list => int => ’a list *)let rec loop lst n = match lst with[] -> []| first :: rest ->if n = 0 thenshift (fun k -> first :: k rest)
else first :: (loop rest (n - 1))(* take : ’a list -> int -> ’a list *)let take lst n = reset (fun () -> loop lst n)
take [0; 1; 2; 3; 4] 3 = [3; 0; 1; 2; 4]
Kenichi Asai

Delimited Continuations for Everyone

21/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

A-normalization
Given an (arithmetic) expression, return the same
expression where subexpressions are uniquely named.
-a - (b - c - d) becomes:
let e1 = b - c inlet e2 = e1 - d inlet e3 = a - e2 in e3

a

- d
b c

Each ‘-’ expression is uniquely named using let.
When A-normalizer encounters b - c, it has toinsert corresponding let expression at the beginning.
Kenichi Asai

Delimited Continuations for Everyone

22/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

A-normalization(* loop : expr_t => expr_t *)let rec loop expr = match expr with
Var (x) -> Var (x)| Minus (e1, e2) ->let nf1 = loop e1 in
let nf2 = loop e2 in
let x = gensym "e" inshift (fun k ->Let (x, Minus (nf1, nf2), k (Var x)))(* anf : expr_t -> expr_t *)let anf expr = reset (fun () -> loop expr)
Kenichi Asai

Delimited Continuations for Everyone

23/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

A-normalization: example execution| Minus (e1, e2) ->(reshown)
let nf1 = loop e1 in
let nf2 = loop e2 in
let x = gensym "e" inshift (fun k ->Let (x, Minus (nf1, nf2), k (Var x)))hloop[[a - (b - c - d)]]i→ hg(loop[[a]] - loop[[b - c - d]])i→ hg(a - g(loop[[b - c]] - loop[[d]]))i→ hg(a - g(g(loop[[b]] - loop[[c]]) - loop[[d]]))i→ hg(a - g( g(b - c) - loop[[d]]))i→ hlet e1 = b - c in hg(a - g(e1 - loop[[d]]))ii
Kenichi Asai

Delimited Continuations for Everyone

24/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

A-normalization
P. Thiemann “Cogen in Six Lines,” ICFP 1996.
The paper describes how to write a compiler
generator (“cogen”) for λ-calculus.
Three lines for variable, abstraction, and application.
Six lines because each has static/dynamic variants.
A-normalization (via shift/reset) is crucially used toserialize expressions.
The technique also known as “let insertion” inpartial evaluation.
Kenichi Asai

Delimited Continuations for Everyone

25/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to wrap continuations

shift (fun k -> fun () -> k "hello")
Abort The current computation is aborted with athunk.
Access It receives () from outside the context.
Resume The aborted computation is resumed with"hello".

Kenichi Asai

Delimited Continuations for Everyone

26/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to wrap continuations
reset (fun () ->shift (fun k -> fun () -> k "hello" )^ " world") ()↓ Abortreset (fun () ->fun () -> k "hello" ) ()k = reset (fun () -> [ ] ^ " world")↓ Access( fun () -> k "hello" ) ()↓ Resume
reset (fun () -> "hello" ^ " world")
Kenichi Asai

Delimited Continuations for Everyone

27/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to wrap continuations: printf
Fill in the hole so that the following program:reset (fun () ->"hello " ^ [...] ^ "!") "world" ;;would return "hello world!". (The hole acts as %s.)
Can you fill in the following hole:
reset (fun () ->"It’s " ^ [...] ^ " o’clock!") 8 ;;so that it returns "It’s 8 o’clock!"? (%d)
Kenichi Asai

Delimited Continuations for Everyone

28/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Solution
reset (fun () ->"hello " ^shift (fun k -> fun x -> k x ) ^"!") "world" ;;(%s)

or even shift (fun k -> k) would do.
reset (fun () ->(%d)"It’s " ^shift (fun k ->fun x -> k (string_of_int x) ) ^" o’clock!") 8 ;;Kenichi Asai

Delimited Continuations for Everyone

29/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to wrap continuations: printf
The shown solution uses shift and reset.
O. Danvy “Functional Unparsing,” JFP 1998.
This paper shows how printf can be written
type-safe in the standard functional languages(without dependent types).
It is written in continuation-passing style (CPS) anduses continuation in a non-trivial way.

Kenichi Asai

Delimited Continuations for Everyone

30/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummaryState monad
Define the following without using a mutable cell:
put stores a value into a mutable cell, andget retrives a value from the mutable cell.
For example, the following expression evaluates to 11.
put 3; (get () + put 4; get ()) + get ()idea
Let the context higher-order, and the mutable cell ispassed outside the context (just as we did for printf).
Kenichi Asai

Delimited Continuations for Everyone

31/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummaryState monadreset (fun () -> ... expression ...) 0
The cell (0) is passed as an argument of the context.
let get () = shift (fun k -> fun v -> k v v)
let put v = shift (fun k -> fun _ -> k () v)
For example,
reset (fun () -> ...[get ()]...) 0-> reset (fun () -> fun v -> k v v) 0-> (fun v -> k v v) 0-> k 0 0-> reset (fun () -> ...[0]...) 0
Kenichi Asai

Delimited Continuations for Everyone

32/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummaryState monad

A. Filinski “Representing Monads,” POPL 1994.
Any monads can be represented in direct style using
shift/reset.
Includes complete code in SML.

Kenichi Asai

Delimited Continuations for Everyone

33/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Future: shift/reset in theorem proving?
The current proof assistants do not allow exception(nor shift/reset).
If we could introduce shift and reset into theorem
proving, we are liberated from writing monadic proofs.
Questions:
Curry-Howard isomorphism for shift and reset?
What is the type of shift?
What is the logical meaning of shift?
Kenichi Asai

Delimited Continuations for Everyone

34/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Curry-Howard isomorphism
Typed functional language
Intuitionistic logic
Γ⊢e:A
∆⊢A
“Under type environment Γ, “Under assumption ∆,e has type A.”
A holds.”
Γ, x : A ⊢ x : A∆, A ⊢ A

Γ, x : B ⊢ e : AΓ ⊢ fun x -> e : B → A∆, B ⊢ A∆⊢B⊃AΓ⊢f:B→A Γ⊢a:B
Γ⊢f a:A∆⊢B⊃A ∆⊢B∆⊢A

e has type A
if ⊢ e : A can be derived.

A holds
if ⊢ A can be derived.

Kenichi Asai

Delimited Continuations for Everyone

35/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

What is the type of shift?
We have to take the type of the context into account.
Pure (non-shift) expression can appear in any
context (answer-type polymorphic).
Shift restricts the type of its context.
The function put and get can appear only in thehigher-order context.
In general, a function type has the form:
impure A -> B @cps[C, D]
pure ∀α.A -> B @cps[α, α]∼= A -> B

What does this type mean logically?
Kenichi Asai

Delimited Continuations for Everyone

36/39

T. Griffin “A Formulae-as-Types Notion of Control,”
POPL 1990.
call/cc has type ((α → β) → α) → α, which isclassic (Peirce’s law).
It does not take the answer type into account.
What about shift?
Shift moves around a part of computation.
Logically, it cuts and pastes a part of proof tree.
Is this somehow meaning of A -> B @cps[C, D]?
Conjecture
Shift is intuitionistic: even if we use shift, we cannot
construct a term having a classic type.

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

Summary
Shift and reset are simple, but quite expressive.
We have a type system for shift and reset,
but their relationship to logic is unknown.
Q: We can always turn a program with shift/reset
into a program without by CPS transforamtion.
Are shift/reset really necessary?
A: Yes, just like higher-order functions whosenecessity must have been questioned long timeago. They provide us with higher level ofabstraction.
Kenichi Asai

Delimited Continuations for Everyone

38/39

TitleOverview

BasicsDiscardExtract

Reorder

A-normal

Wrap

State

FutureSummary

How to use shift/reset
OchaCaml
shift/reset-extension of Caml Light:
http://pllab.is.ocha.ac.jp/~asai/OchaCaml
Scheme Racket and Gauche support shift/reset.
Haskell Delimcc Library.
Scala Implementation via selective CPS translation.
OCaml Delimcc Library or emulation via call/cc.
Happy programming withshift and reset!
Kenichi Asai

Delimited Continuations for Everyone

39/39