Understanding the Type of
Pre-requisites: First-class continuations and
call/cc (this article does not cover what they are, how they work, or why they are useful, only their type); and reading Racket code.
In classical Hindley–Milner type systems (for example, the core of the type systems in ML and Haskell), the function
call/cc (short for
call-with-current-continuation) has type
call/cc : ((α → β) → α) → α, where
β are type variables that can be instantiated with any type. This type is interesting, particularly in how it relates to logic, but like most topics surrounding first-class continuations, it is unintuitive. In this short article, we derive
call/cc’s type step-by-step by using Racket expressions as examples. Racket is dynamically typed, but we can use it to reason about static types as well. In Typed Racket the type of
call/cc is a bit more elaborate, see appendix.
We start with a simple expression:
> (zero? 0) #t
We can surround the
0 in this expression with an use of
call/cc without changing its output:
> (zero? (call/cc (λ (k) 0))) #t
The meaning of the expression is preserved because
(call/cc (λ (k) e)) is the same as
e does not reference
(λ (k) e) with the current continuation as
e ignores it. This example reveals three parts of
call/ccis being applied, so it is a function:
call/cc : ___ → ___. (The placeholders
___represent parts of the type that we do not know yet.)
0, a number, so
call/cc : ___ → Number.
call/ccreceives a function as argument,
(λ (k) 0) : ___ → Number, so
call/cc : (___ → Number) → Number.
To fill in the blank we need an expression that uses
k. But we do not want to change the return type of the function passed as
call/cc’s argument, so we use
k before the
0, for example:
> (zero? (call/cc (λ (k) (k 42) 0))) #f
This changed the output from
(k 42) takes execution back to the outer addition, skipping over the remainder of the function passed as
call/cc’s argument (the remainder being just the
0 in this case). This expression is equivalent to
(zero? 42), and it reveals two other parts of
kis being applied, so it is a function:
call/cc : ((___ → ___) → Number) → Number.
kis called with a number:
call/cc : ((Number → ___) → Number) → Number.
It is not a coincidence that these three types agree (in our example, they are all
kis called, then
call/ccreturns the argument to
k, and if
kis not called, then
call/ccreturns the same as the function that was passed to it (see the appendix for the full story).
The final blank is
k’s return type, and to fill it we have to explore how
k’s output may be used. But
k is not a regular function, it is a first-class continuation produced by
call/cc. A first-class continuation does not return; it has no output. When we call
k, execution resumes on the surrounding of the call to
call/cc and never returns. For example, when we call
k in the previous expression, execution resumes on the outer addition and never returns to the rest of the function that was passed as
call/cc’s argument (the
k has no output, it can appear in any context, and its return type can be anything. For example, consider the following two expressions in which the call to
k appears in two different contexts: one expecting a
string-length), and one expecting a
> (zero? (call/cc (λ (k) (string-length (k 42)) 0))) #f > (zero? (call/cc (λ (k) (first (k 42)) 0))) #f
Both expressions above have valid types, so both of the following hold:
call/cc : ((Number → String) → Number) → Number, and
call/cc : ((Number → List) → Number) → Number. In general,
call/cc : ((Number → β) → Number) → Number, where
β is a type variable that can be instantiated with any type. This is similar to how
raise can appear in any context, because execution will skip that context up to the closest catch, so its return type can be anything:
raise : α → β.
Alternative Argument: The continuation
(zero? •), where
• represents the hole that we plug with a value to continue the computation. We can reify
k as a function
(λ (x) (zero? x)) : Number → Boolean, and we can replace
β without loss of generality. This
k is not a regular function, however, because execution discards the context under which it is called.
The use of numbers in our examples was incidental. We could replace them with strings, for example:
> (string-length (call/cc (λ (k) (first (k "hi")) "hello"))) 2
The only constraint is that these three types must agree: the return type of
call/cc, the return type of the function passed as argument to
call/cc, and the type of
k’s argument (see the appendix for the full story). Finally, we can conclude that
call/cc : ((α → β) → α) → α.
call/cc’s type in Typed Racket
We had to compromise on the type for
call/cc in the classical Hindley–Milner type system (
call/cc : ((α₁ → β) → α₂) → α): we had to constrain the type
α₁ of the argument passed to the continuation
k to be the same as the return type
α₂ of the function passed to
call/cc. This constraint is artificial and is not present in Racket, as shown by the following expressions in which these types disagree (
α₁ = String and
α₂ = Number):
> (write (call/cc (λ (k) 0))) 0 > (write (call/cc (λ (k) (k "42") 0))) "42"
This disagreement is not a problem at runtime as long as the surrounding context can handle values of either type—as
write can. But classical Hindley–Milner type systems have no way of representing the return type of
call/cc used in this manner—there is no way to write that
call/cc may return either a
String or a
Number—so languages with classical Hindley–Milner type systems disallow these kinds of expressions.
To type check expressions like the last example, Typed Racket’s type system has to go beyond the classical Hindley–Milner type systems, featuring something called union types. In particular, Typed Racket’s type system features untagged unions, as opposed to ML’s variants which are tagged unions, because they are tagged with constructor names. Thus, in Typed Racket, the type of
call/cc is closer to
call/cc : ((α → β) → γ) → (α ∪ γ), where
α ∪ γ represents the union of
γ, meaning values of this type may be either
γ. The actual type of
call/cc in Typed Racket is a bit more elaborate, but for reasons that go beyond the scope of this article.
Union types are useful beyond esoteric language features like
call/cc. For example, they allow type checking conditionals in which the branches produce different types, for example,
(if ___ 0 "hi"), which are common in Racket but must also be disallowed by languages featuring classical Hindley–Milner type systems.
I thank the following people for their comments and suggestions: Scott Smith, Sorawee Porncharoenwase, Dario Hamidi, and A. B. McLin.