I was honored to be an invited speaker at the Workshop on Theory and Practice of Delimited Continuations last month. The organizers—Alexis Saurin, Hugo Herbelin, and Noam Zeilberger—did a great job at putting together a friendly and informative event. Here are some fragmentary notes.

Zena Ariola, Hugo Herbelin, David Herman, and Dan Keith: Let’s change the abort in Filinski’s implementation of shift/reset from strict to lazy. (1) When a top-level reset is present as there is supposed to be, the implementation still works as specified. (2) Moreover, in the unspecified situation where there is no top-level reset, the implementation behaves more consistently.

Pierre Boutillier and Hugo Herbelin: Types better not depend on impure terms, so require reset around terms that occur in types.

Noam Zeilberger: Presheaves are {a fancy name for, the constructive content of, the result of categorifying} Kripke semantics. Kripke’s worlds and their relationships are the objects and morphisms of the category that the presheaf is a functor from. Can we identify the dependency in dependent types with the dependency in evaluation order?

Roshan James and I debated the computational content of the movie Primer. The question boiled down to this: using the mechanism in the movie, can you build (a la “Constraining Control”) a box that reports how many times it has been used, total (throughout all time)? My answer is no because I model the movie using the following monad, which I should explain in writing some day:

data Tree a = Leaf a | Branch (Tree a) (Tree a)

newtype Primer w a = Primer ((a -> Tree w) -> Tree w)
instance Monad (Primer w) where
  return a       = Primer (\c -> c a)
  Primer m >>= k = Primer (\c -> m (\a ->
                   let Primer n = k a in n c))
runPrimer :: Primer w w -> Tree w
runPrimer (Primer m) = m Leaf

data Box w a = Box { exit :: Maybe a
                     , enter :: a -> Primer w () }
newBox :: Primer w (Box w a)
newBox = Primer (\c ->
  let enter a = Primer (\c' ->
                Branch (c' ()) (c (Box (Just a) enter)))
  in c (Box Nothing enter))

Moe Masuko and Kenichi Asai implemented shift/reset in Caml Light. Their group is writing many interesting programs on top of this platform (such as declarative game-strategy search with alpha-beta pruning). Masuko’s and Herbelin’s presentations made me think it might make more sense to put one big reset around the entire REPL rather than one reset around each REPL interaction. This way, in the typical REPL that allows creating new top-level bindings using “let”, if we accidentally shadow a binding with another of the same name, we could still get back the old binding by invoking a previously captured REPL continuation.

Roshan P. James and Amr Sabry: yield is popular, and people even speak of it as a “delimited I/O” facility. I wonder if the popularity is because the type of yield is first-order?

General discussion

Christophe Calvès’s PhD thesis has a part about a hierarchy of monad transformers. Filinski’s recent paper “Monads in Action” presents an operational model of side effects in which monads are dynamically layered. Implementing this model in terms of shift/reset (with a proof of correctness and all that) would be nice and is an open problem as far as we know! In particular, we’d like dynamically layered regions of monadic effects.

Speaking of layering: The examples we currently have of using cupto/set in practice all have the flavor of making one present-stage (aka metalanguage) prompt/cell per future-stage (aka object-language) binder:

• Balat et al.’s “Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums”
• Label every binder in a λ-term with how many times that bound variable is used
• Transform a λ-term to make contraction explicit, for example turning “λx.xx” into “λx. let x₁=x and x₂=x in x₁x₂”

So, if we represent the input term by “de Bruijn Notation as a Nested Datatype” (Bird and Paterson), can we write any of these examples using a control hierarchy like Danvy and Filinski’s that makes the absence of uncaught shifts patent to the type system? The use of type-level functions and polymorphic recursion is allowed.

What is the distinction between undelimited and delimited continuations? Führmann’s thesis concerns the distinction? I feel the important distinction is whether an expression is polymorphic or not in the answer type.

What is a continuation, some reviewers ask? I take the “continuation stance” (cf Dennett’s intentional stance) when appropriate: something is a continuation when a direct-style transformation that makes it implicit simplifies the program overall. In the end the answer depends on what is representation.

Conversations outside the workshop

Olivier Hermant explained deduction modulo to me: augment first-order logic with equations or rewriting rules to capture things hard to express in first-order logic such as transitivity or arithmetic. Uniform metatheoretic results such as proof normalization across many modulo. Is this tool good for natural logic?

Peter Dybjer is hooking up Agda to first-order automatic theorem provers. The idea is to describe the existence of an Agda proof as a first-order formula, so if the theorem prover says yes then you trust that there is an Agda proof. This way, hopefully the end user of Agda only needs to give the broad outlines of a proof like what induction or pattern matching to do.

TLCA papers to read: “Classical Call-by-Need and Duality” (Ariola, Herbelin, and Saurin), “Game Semantics and Uniqueness of Type Inhabitants in the Simply-Typed Lambda-Calculus” (Pierre Bourreau and Sylvain Salvati), “A Filter Model for λμ” (Steffen Van Bakel, Franco Barbanera, and Ugo De Liguoro).

I agreed with Barry Jay that “well typed” and “simply typed” should never be hyphenated, but then I wondered: do these phrases perhaps have specialized meanings that justify hyphens?