A Type-Theoretic Foundation of Continuations and Prompts

Amr Sabry (Indiana University)

with Zena M. Ariola (University of Oregon) and Hugo Herbelin (INRIA-Futurs)

19 September 2004

Supported by National Science Foundation grant number CCR-0204389

Outline

• Introduction: semantics of continuations and prompts

• Review: continuations and classical logic

• The essence of prompts

• Typing of continuations and prompts

• continuations and prompts and ?? logic

ICFP’04—Snowbird, Utah Page 2 of 73

Basic Control operators

• A M aborts everything, returns M to the top-level #E[A M] ↦ #M

• C (λc.M) binds the entire continuation to c

• capturing the continuation aborts; calling the continuation aborts #E[C M] ↦ #(M (λx.A E[x]))

• C can express A: we can focus on C

• Fairly well-understood from types and logic perspective

ICFP’04—Snowbird, Utah Page 3 of 73

Minimal logic and λ-calculus

\begin{aligned}A, B & : : = & X | A → B \\ M, N & : : = & x | λx.M | MN \end{aligned}

Γ, x: A ⊢ x: A

\begin{matrix}Γ, x: A ⊢ M: B \\ Γ ⊢ λx.M: A → B \end{matrix}

\begin{matrix}Γ ⊢ M: A → B Γ ⊢ N: A \\ Γ ⊢ MN: B \end{matrix}

ICFP’04—Snowbird, Utah Page 4 of 73

Control operators (Griffin POPL’90)

• Type constant ⊥ corresponding to formula False ¬A abbreviates A → ⊥

• A corresponds to Ex Falso Quodlibet

{Γ ⊢ M: ⊥ \atop Γ ⊢ A (M): A}

• C corresponds to “proof by contradiction” (Double Negation):

{Γ ⊢ M: ¬¬A \atop Γ ⊢ C(M): A}

• A “implements” intuitionistic logic

• C “implements” classical logic

ICFP’04—Snowbird, Utah Page 5 of 73

Delimited control operators

• Fundamental idea is to allow # anywhere: (Felleisen 1988) # (1 + # (2 + (C (λc. 3 + #(4 + (c (# (c 5))))))))

• In (C (λc. …)), continuation c extends to the closest # only • In (A M), expression M is returned to the closest # prompt • C and # are equivalent to shift (abbreviated S) and reset (Danvy and Filinski 1990)

ICFP’04—Snowbird, Utah Page 6 of 73

In the presence of prompts …

• no canonical type system (some proposed type systems incomparable)

• no confluence results

• no strong normalization results (and known counterexamples in some cases)

• no expressiveness results (but Thielecke et al. have studied expressiveness of continuations, exceptions, and state)

A menagerie of control operators

• In addition to A, C, #, shift, reset, we also have callcc, shift_{n}, reset_{n}, spawn, F, cupto, splitter, etc.

• Design space: continuation-passing style (CPS), iterated CPS, hierarchies of control operators and delimiters, fixed set of prompt names or dynamic generation prompt names, delimiters captured in continuations or not, lifetime of delimiters, etc.

Our goal Understand and compare these control operators using type-theory and logic.

Continuations and Classical Logic

ICFP’04—Snowbird, Utah Page 9 of 73

The legacy of Griffin

• Continuations are functions from values to ⊥

• The top-level is of type ⊥ But … C(λc.c1) ↦ 1 the top-level seems to be an int ! And there are no closed terms of type ⊥: there are no well-typed programs ! Griffin adopts a convention to solve this problem

ICFP’04—Snowbird, Utah Page 10 of 73

Formalizing Griffin’s convention

Murthy (1992), Ariola and Herbelin (2003)

• A constant tp denotes the top-level continuation:

A 6 = C(λ .tp 6) A true = C(λ .tp true)

• Implicit references to the top-level become explicit:

C(λc. 1 + c 0) becomes C(λc. tp (1 + c 0))

• Judgments Γ ⊢ M: A; T keep track of the type T of the top-level (not restricted to ⊥):

⊢ C(λ .tp 6) : A; int ⊢ C(λ .tp true) : A; bool

ICFP’04—Snowbird, Utah Page 11 of 73

The λ→_{Ctp} calculus: jumps

• Special constant tp denoting the top-level continuation

• Special category J of jumps

• A symbol ⊥ ⊥ denoting the absence of a type

• Continuations are not functions

{Γ, k: A → ⊥ ⊥ ⊢ M : A; T \atop Γ, k: A → ⊥ ⊥ ⊢ k M : ⊥ ⊥; T} →_{e}^{k}
{Γ ⊢ M : T; T \atop Γ ⊢ tp M : ⊥ ⊥; T} →_{e}^{tp}

ICFP’04—Snowbird, Utah Page 12 of 73

Manipulating continuations in λ→_{Ctp}

• One can jump if and only if one captures the continuation

• Two common patterns:

A-M =^{Δ} C(λ .tp M)  (Abbrev. 1)
throw k M =^{Δ} C(λ .k M)  (Abbrev. 2)

• Type rule:

{Γ, k: A → ⊥ ⊥ ⊢ J : ⊥ ⊥; T \atop Γ ⊢ C(λk.J) : A; T} RAA

• Isomorphic to λμ (Parigot 1992) with tp

ICFP’04—Snowbird, Utah Page 13 of 73

Examples in λ→_{Ctp}

⊢ (A- 5 == "Hello") : bool; int

accurately predicts that the expression might return a bool or jump to the top-level with an int.

⊢ λx.(x + A- "Hello") : int → int; string

How to interpret the “top-level type” string ?

The calculus λ→_{Ctp} has …

• simpler reduction rules (no encoding of continuations as functions)

• which are confluent

• and normalizable when simply typed

What we have so far …

A calculus λ\overrightarrow{Ctp} for understanding continuations • with better properties than Griffin’s original formulation

ICFP’04—Snowbird, Utah Page 16 of 73

The Essence of Prompts

ICFP’04—Snowbird, Utah Page 17 of 73

Adding prompts

• A prompt is a top-level for the duration of the subexpression • Control actions always refer to the dynamically closest prompt.

• An analysis (in the paper) shows that the dynamic aspect of the prompt is all that it contributes

• to model prompts, all we need is to change the constant tp to a dynamically-bound variable t̂p.

ICFP’04—Snowbird, Utah Page 18 of 73

Forget about prompts: λ→_{Ct̂p}

• We can express # M as C(λt̂p. t̂p M)

• Semantics is just like the standard semantics for λ\overrightarrow{Ctp} but

– allow capture of t̂p in substitution:

(λy.C(λt̂p. t̂p (x y))) ˆ[(λ .C(λ .t̂p y))/xˆ]

= λy′.C(λt̂p. t̂p ((λ .C(λ . t̂p y)) y′))

– allow t̂p to escape its scope:

C(λt̂p. t̂p (λ .C(λ .t̂p y))) → λ .C(λ .t̂p y)

Important result

This is correct !

• Semantics of original control operators and prompts is preserved

ICFP’04—Snowbird, Utah Page 20 of 73

What we have so far …

A calculus λ\overrightarrow{Ct̂p} for understanding continuations and prompts:

• has better properties than Griffin’s original formulation

• a prompt is normal control + dynamic scope (Cλt̂p …)

Typing Continuations and Dynamic Scope

ICFP’04—Snowbird, Utah Page 22 of 73

Typing dynamically scoped entities

• Type-and-effect system

\begin{aligned}Γ, x: A ⊢ x: A; T & Ax \\ {Γ, x: A ⊢ M: B; T \atop Γ ⊢ λx.M: A →_{T} B; T′} & →_{i} \\ \begin{matrix}Γ ⊢ M: A →_{T} B; T & Γ ⊢ M′: A; T \\ Γ ⊢ MM′: B; T \end{matrix} & →_{e} \end{aligned}

• Can be extended to a sound type system for λ\overrightarrow{Ct̂p}

• This type system is too restrictive !

ICFP’04—Snowbird, Utah Page 23 of 73

Dynamic scope as environment-passing

• A good formal definition (Moreau 1998)

• Every expression (and hence every continuation) is passed the environment

• In our case: environment consists of the current top-level continuation

• Input type to continuation is the return type of the expression:

{Γ, k : A→ ⊥ ⊥ ⊢ J: ⊥ ⊥; T \atop Γ ⊢ C(λk.J) : A; T} RAA

• Every expression must return an environment

• The environment is really a store !

Dynamic scope as exceptions

• Exceptions are jumps to a dynamically-determined handler • In our case: using the top-level continuation jumps to the dynamically closest handler

• Interactions of exceptions and continuations from SML/NJ: – the usual callcc (not the interaction we want)

– an operator capture that we want:

{H, E[capture M]} ↦ {H, E[M (λx.A E[x])]}
NOT {H, E[M (λx.A {H, E[x]})]}

• capture and exceptions can define state ! (Thielecke 2001)

Dynamic scope + control ⇒ state

\begin{matrix}Γ, x: A; T ⊢ x: A; T Ax & {Γ, x: A; U ⊢ M: B; T \atop Γ; T′ ⊢ λx.M:A _{U} →_{T} B; T′} →_{i} \\ \begin{matrix}Γ; U_{1} ⊢ M:A _{U_{2}} →_{T_{1}} B; T_{2} & Γ; T_{1} ⊢ N:A; U_{1} \\ Γ; U_{2} ⊢ MN: B; T_{2} \end{matrix} & →_{e} \end{matrix}

Still sound but more expressive: # (1 + S(λc. 2 == c 3)) Olivier Danvy and Andrzej Filinski might now say:

We could have told you so in 1989 !

ICFP’04—Snowbird, Utah Page 26 of 73

Or more clearly …

In classical logic, the following formulae are all equivalent:

A ∧ ¬T → B  (t̂p as an environment)
= A → B ∨ T  (t̂p as an exception)
= A ∧ ¬T → B ∧ ¬T (t̂p as a state)

A logic with effect annotations?

Let’s just get rid of all these annotations and have a simple elegant type system.

• Possible

• Type system is nicer

• Can be implemented in a standard type system (SML, Ocaml, etc)

• But we lose strong normalization (if the top-level type is not atomic)

• and we start accepting terms that may refer to non-existing prompts.

What we have so far …

A calculus λ\overrightarrow{Ct̂p} for understanding continuations and prompts:

• has better properties than Griffin’s original formulation

• a prompt is normal control + dynamic scope (Cλt̂p …)

• two not-very-pretty type-and-effect systems

Subtractive Logic

ICFP’04—Snowbird, Utah Page 30 of 73

Interpreting effects

• If we don’t want effects, translate using monads

• Map (k: A →_{U} ⊥ ⊥)^{∗} to (k: A^{∗} ∧ ¬U^{∗} → ⊥ ⊥)

• LHS: restrict contexts where k can be called by requiring a toplevel continuation of type U

• RHS: pass a top-level continuation of type U to k A continuation to the continuation is a … metacontinuation

Olivier Danvy and Andrzej Filinski might now say:

We could have told you so in 1990 !

The dual of implication

What is the type A ∧ ¬B ? In classical (but not intuitionistic) logic, we have:

¬(A → B) = ¬(¬A ∨ B)
= ¬¬A ∧ ¬B
= A ∧ ¬B

It is the negation of implication This suggests we can use the dual of implication: subtraction A−B (introduced at least by 1974)

ICFP’04—Snowbird, Utah Page 32 of 73

To subtract or not to subtract

A − B is the same as A ∧ ¬B but better:

• More “abstract.” A continuation k has type A − T → ⊥ ⊥

⋆ Because A − T iff A ∧ ¬T continuations need metacontinuations (Danvy and Filinski 1990) ⋆ Because A − T iff ¬(¬T → ¬A) delimited continuations are also the “difference of two continuations” (Queinnec and Moreau 1994)

• Makes sense even in the absence of first-class continuations (Crolard 2004)

even : int → bool
evenEncoding : ¬int ∨ bool

The λ→−_{C} calculus
Γ, x: A ⊢ x: A Ax {Γ, x: A ⊢ M: B \atop Γ ⊢ λx.M:A → B} →_{i}
\begin{matrix}Γ ⊢ M:A → B & Γ ⊢ M′:A \\ Γ ⊢ MM′: B \end{matrix} →_{e}
{Γ, k: A → ⊥ ⊥ ⊢ J: ⊥ ⊥ \atop Γ ⊢ C(λk.J): A} RAA {Γ, k: A → ⊥ ⊥ ⊢ M: A \atop Γ, k: A → ⊥ ⊥ ⊢ k M: ⊥ ⊥} →_{e}^{k}
\begin{matrix}Γ ⊢ M: A & Γ, □: B ⊢ k E: ⊥ ⊥ \\ Γ ⊢ (M, k E): A − B \end{matrix} −_{i}

Γ ⊢ M: A − B Γ, x: A, k: B → ⊥ ⊥ ⊢ M′: C

Γ ⊢ let (x, k) = M in M′: C −_{e}

Type system is also sound

ICFP’04—Snowbird, Utah Page 34 of 73

How to use λ→−_{C}

• As a source language if you want

• By embedding in it other languages with control operators

– embeddings arrange for managing the prompt (or top-level continuation or metacontinuation) using subtraction

– (y (# x)) translates as y ((C(λtp′.tp′ x), tp □)) The current top-level continuation is “saved” using the subtraction introduction and a new top-level continuation is used for receiving the value of x.

Important results

This is correct !

• Types and semantics of original control operators and prompts is preserved

• Well-typed terms are strongly normalizing • Consistent with known CPS transformations of the control operators

Conclusions

ICFP’04—Snowbird, Utah Page 37 of 73

Remember …

• Do not sweep the top-level continuation under the rug (tp)

• A continuation is not a function (⊥ ⊥)

• A little bit of dynamic scope can help (#)

• Regular continuations augmented with one dynamically-scoped continuation can express all other effects including state

• Type-and-effect systems or monads are essential sometimes • Logic helps !

• Subtractive logic is the right way to think about advanced control operators (some of them at least)

Future work

… skipping …

A