Understanding the Type of ‘call/cc’

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 α and β 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,.

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? <mark>(call/cc (λ (k) </mark>0<mark>))</mark>)
#t

The meaning of the expression is preserved because (call/cc (λ (k) e)) is the same as e when e does not reference k : call/cc calls (λ (k) e) with the current continuation as k , but e ignores it. This example reveals three parts of call/cc ’s type:

1. call/cc is being applied, so it is a function: call/cc : ___ → ___ . The placeholders ___ represent parts of the type that we do not know yet.
2. call/cc returns 0 , a number, so call/cc : ___ → Number .
3. call/cc receives 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) <mark>(k 42)</mark> 0)))
#f

This changed the output from #t to #f , because (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 call/cc ’s type:

1. k is being applied, so it is a function: call/cc : ((___ → ___) → Number) → Number .
2. k is 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 Number ): if k is called, then call/cc returns the argument to k , and if k is not called, then call/cc returns the same as the function that was passed to it.

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 0 ).

Since 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 ( string-length ), and one expecting a List ( first ): 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 : α → β .

> (zero? (call/cc (λ (k) <mark>(string-length </mark>(k 42)<mark>)</mark> 0)))
#f
> (zero? (call/cc (λ (k) <mark>(first </mark>(k 42)<mark>)</mark> 0)))
#f

Also, the use of numbers in our examples was incidental. We could replace them with strings, for example:

> (<mark>string-append</mark> <mark>"hello "</mark> (call/cc (λ (k) (first (k <mark>"world"</mark>)) <mark>"mars"</mark>)))
"hello world"

The only constraint is that the 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. Finally, we can conclude that call/cc : ((α → β) → α) → α .

Appendix: 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 ):

> (<mark>write</mark> (call/cc (λ (k) <mark>0</mark>)))
0
> (<mark>write</mark> (call/cc (λ (k) (k <mark>"42"</mark>) <mark>0</mark>)))
"42"

This disagreement is not a problem at runtime as long as the surrounding context can handle values of either type, like write can. But classical Hindley–Milner type systems have no way of representing the return type of call/cc used in this way—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 , also known as untagged unions . As opposed to ML’s variants which are tagged unions , because they are tagged with the constructor names. Thus, in Typed Racket, the type of call/cc is closer to call/cc : ((α → β) → γ) → (α ∪ γ) , where α ∪ γ represents the union of α and γ , meaning values of this type may be either α or γ . 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 "42") , which are common in Racket but must also be disallowed by languages featuring classical Hindley–Milner type systems.

Acknowledgements

I thank the following people for their comments and suggestions: Scott Smith, Sorawee Porncharoenwase, Dario Hamidi and A. B. McLin.