Logical Methods in Computer Science
Vol. 2 (3:3) 2006, pp. 1–22
www.lmcs-online.org

Submitted
Published

Dec. 16, 2005
Jul. 27, 2006

RELATIONAL PARAMETRICITY AND CONTROL
MASAHITO HASEGAWA
Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502 Japan, and
PRESTO, Japan Science and Technology Agency
e-mail address: hassei@kurims.kyoto-u.ac.jp
Abstract. We study the equational theory of Parigot’s second-order λµ-calculus in connection with a call-by-name continuation-passing style (CPS) translation into a fragment
of the second-order λ-calculus. It is observed that the relational parametricity on the target calculus induces a natural notion of equivalence on the λµ-terms. On the other hand,
the unconstrained relational parametricity on the λµ-calculus turns out to be inconsistent. Following these facts, we propose to formulate the relational parametricity on the
λµ-calculus in a constrained way, which might be called “focal parametricity”.

Dedicated to Prof. Gordon Plotkin on the occasion of his sixtieth birthday

1. Introduction
The λµ-calculus, introduced by Parigot [26], has been one of the representative term
calculi for classical natural deduction, and widely studied from various aspects. Although
it still is an active research subject, it can be said that we have some reasonable understanding of the first-order propositional λµ-calculus: we have good reduction theories,
well-established CPS semantics and the corresponding operational semantics, and also some
canonical equational theories enjoying semantic completeness [16, 24, 25, 36, 39]. The last
point cannot be overlooked, as such complete axiomatizations provide deep understanding of equivalences between proofs and also of the semantic structure behind the syntactic
presentation.
The second-order λµ-calculus (λµ2), again due to Parigot [27], has been studied in depth
as a calculus for second-order classical natural deduction. In particular, strong normalization results of λµ2 [27, 23] and its extensions, e.g. with inductive types [21], have been a
central research topic, because of the proof-theoretical importance of strong normalization.
However, for λµ2, it seems that there are few attempts of giving an equational theory supported by some fine semantic structure. This situation is rather frustrating, since without
such equational and semantic accounts, we cannot discuss e.g. the correctness of the impredicative encoding of the datatypes in λµ2. For the second-order λ-calculus λ2 (system
2000 ACM Subject Classification: F.3.2.
Key words and phrases: polymorphism, parametricity, continuations.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-2 (3:3) 2006

CC

Masahito Hasegawa
Creative Commons

2

MASAHITO HASEGAWA

F) [9, 33], a subsystem of λµ2, there are several beautiful results on the relational parametricity [34] and the universal properties of impredicative constructions [1, 15, 31, 40, 44],
e.g. that µX.σ = ∀X.(σ → X) → X (where σ covariant in X) gives an initial algebra of
the functor ΛX.σ in a suitable sense. We certainly wish to have such a story for λµ2 too.
This work is an attempt to identify such an equational theory which is backed up by
certain semantic structures. Specifically, we propose a relational parametricity principle
which is sound and sufficiently powerful for deriving such equivalences on the λµ-terms.
1.1. Parametric CPS semantics. We first consider the semantics of λµ2 given by a
CPS-translation into a fragment of λ2 — that of the second-order existential types ∃X.τ ,
conjunction types τ1 ∧ τ2 , and arrow types τ → R into a distinguished type R (this choice
of the target calculus is due to a recent work of Fujita [7]). The translation (−)◦ sends
a type variable X to X, arrow type σ1 → σ2 to (σ1◦ → R) ∧ σ2◦ , and the universal type
∀X.σ to ∃X.σ ◦ — while a term M : σ is sent to [[M ]] : σ ◦ → R. It can be considered as a
natural extension of Streicher’s call-by-name CPS translation [36, 39, 43]. It follows that
this translation already gives a reasonable equational theory on λµ2, in that it validates the
standard βη-equalities1 . In fact, this is a consequence of a fibred version of the ”category
of continuations” construction [16, 36, 39].
However, this is just a starting point; we observe that, if some of the impredicative
constructions in the target calculus satisfy certain universal properties (e.g. ∃X.X is a
terminal object) which follow from the relational parametricity, then so do the impredicative
constructions in the source λµ2-calculus — but not quite in the way that we first might
expect. For instance, the type ⊥ = ∀X.X does not give an initial object (cf. [37]) — instead
it plays the role of the falsity type (or the “answer type”); in fact, we have a double-negation
elimination from (σ → ⊥) → ⊥ to σ for any σ which actually is an algebra of the doublenegation monad ((−) → ⊥) → ⊥. As another major example, ∀X.(σ → X) → X does
not give an initial algebra of ΛX.σ; it gives an initial algebra of ΛX.(σ → ⊥) → ⊥ — not
with respect to all terms but to a certain class of terms (the “focal terms”, to be mentioned
below). In particular, if X is not free in σ, ∀X.(σ → X) → X is isomorphic not to σ but
to (σ → ⊥) → ⊥. In short, impredicative encodings in λµ2 get extra double negations,
and the relational parametricity of λ2 is not consistent with the equational theory of λµ2
induced by the CPS semantics. As a consequence, we cannot encode cartesian products in
λµ2, though they can be added easily. Also we cannot express the classical disjunctions
[36], though they can be added without changing the target of the CPS translation.
1.2. Focal parametricity. These results suggest that the CPS translation into parametric
target calculus gives a reasonable semantic foundation and equational theory for λµ2, which
is sufficient for obtaining various interesting results. However, here the parametricity is
used rather indirectly, via the CPS translation; we also wish to have a decent notion of
parametricity directly within λµ2. To figure out what sort of parametricity principle can be
expected for λµ2, recall the following fact on λ2 with parametricity: given a polymorphic
term M : ∀X.F [X] → G[X] (with X covariant in F and G) and types σ1 , σ2 , the instances
1We can say more – we can show that this CPS-semantics is sound and complete with respect to the
βη-theory of λµ2. This result, together with further syntactic analysis of this CPS translation, will appear
in a forthcoming paper with Ken-etsu Fujita.

RELATIONAL PARAMETRICITY AND CONTROL

3

M σ1 : F [σ1 ] → G[σ1 ] and M σ2 : F [σ2 ] → G[σ2 ] obey the naturality, in that the following
diagram
F [f ]
- F [σ2 ]
F [σ1 ]
M σ1

M σ2

?

G[σ1 ]

?
- G[σ2 ]

G[f ]

commutes for any f : σ1 → σ2 . This is no longer true for λµ2. For example, let F [σ] = (σ →
⊥) → ⊥, G[σ] = σ and M be the double-negation elimination (which does not exist in λ2);
then the naturality for arbitrary maps implies inconsistency — we get σ ≃ (σ → ⊥) → ⊥
for every σ by letting f be the obvious map from σ to (σ → ⊥) → ⊥, which is enough to
kill the theory [20]. Similar result can be observed for other “classical” proofs, e.g. of the
Peirce law.
To this end, we look at the focus [36] (centre [32, 42], C-maps [16]) of λµ2; a focal map
is no other than an algebra morphism between the the double-negation monad mentioned
above, i.e., a map making the naturality diagram for the double-negation elimination commute. It follows that a notion of relational parametricity on λµ2 in which the construction
of the graph relations is allowed only for focal maps is consistent, as there are nontrivial
models. Together with the definability (fullness) of the CPS translation, we see that it is at
least as powerful as the parametricity on the CPS target calculus which we have mentioned
above, thus gives a powerful principle for deriving the equivalences of terms in λµ2. (We
actually conjecture that these two notions of parametricity do agree, but it is open as of
writing this article.) This principle, which we shall call focal parametricity, should be a
natural notion of parametricity for λµ2. We will sketch some use of focal parametricity for
deriving “free theorems” for λµ2 syntactically.
1.3. Towards parametricity for computational effects. At the conceptual and abstract level, this story closely resembles to the study of linear parametricity and recursion
[4, 30]. In the case of linear parametricity, the graph relations are allowed to be constructed
only from the linear maps, and a linear map is an algebra map w.r.t. the lifting monad.
We claim that, just like the linear parametricity gives a solution of accommodating nontermination and recursion in the polymorphic setting (as advocated by Plotkin [30]), the
focal parametricity provides a way of accommodating control features in the polymorphic
setting. In short:
focal parametricity
linear parametricity
=
non-termination
first-class control
As future work, it would be an interesting challenge to find a unifying framework
of linear parametricity and focal parametricity; it should be useful to have parametric
polymorphism, recursion, and control at once, as in the realistic programming languages (cf.
[14, 18, 19]). More ambitiously, we are keen to see an adequate notion of parametricity for
fairly general “effectful” settings. Possible starting points for this direction might include
the “parametricity graphs” approach [5] which allows us to deal with parametricity at
a general level (including the linear parametricity as an instance), and the “category of

4

MASAHITO HASEGAWA

linear continuations construction” [12] which induces both the CPS translation and Girard
translation as special cases. See Section 7 for further discussions related to this issue.
1.4. Construction of this paper. The rest of this paper is organised as follows. In section
2 and 3 we introduce the calculi and CPS-translation which are the subject of this study.
In section 4 we consider the implications of the relational parametricity on the CPS-target
calculus. The focal parametricity is introduced in section 5, followed by examples in section
6, including focally initial algebras and the type of Church numerals. Section 7 gives an
alternative characterisation of focus, which suggests a generalisation of this work to a theory
of parametricity for general effects. We then give some concluding remarks in Section 8.
2. The calculi
2.1. The second-order λµcalculus. The second-order λµ-calculus, λµ2, is given as follows. We essentially follow Parigot’s formulation [27] (with some flavour from Selinger’s
[36]). The types are the same as those of the second-order λ-calculus λ2:
σ ::= X | σ → σ | ∀X.σ
In a typing judgement Γ ⊢ M : σ | ∆, Γ stands for the typing context of variables, while ∆
for the context of names (continuation variables).
Γ, x : σ, Γ′ ⊢ x : σ | ∆
Γ, x : σ1 ⊢ M : σ2 | ∆
Γ ⊢ λxσ1 .M : σ1 → σ2 | ∆
Γ ⊢ M : σ1 → σ2 | ∆ Γ ⊢ N : σ1 | ∆
Γ ⊢ M N : σ2 | ∆
Γ ⊢ M : σ | ∆ (X 6∈ F T V (Γ, ∆))
Γ ⊢ ΛX.M : ∀X.σ | ∆
Γ ⊢ M : ∀X.σ1 | ∆
Γ ⊢ M σ2 : σ1 [σ2 /X] | ∆
Γ ⊢ M : σ2 | α : σ1 , ∆ (β : σ2 ∈ α : σ1 , ∆)
Γ ⊢ µασ1 .[β]M : σ1 | ∆

RELATIONAL PARAMETRICITY AND CONTROL

5

The axioms for the equational theory are again the standard ones — note that we consider
the extensional theory, i.e. with the η-axioms.
(λxσ .M ) N
λxσ .M x
(ΛX.M ) σ
ΛX.M X

=
=
=
=

M [N/x]
M (x 6∈ F V (M ))
M [σ/X]
M (X 6∈ F T V (M ))

µα.[β](µγ.M )
µασ .[α]M
σ
→σ
1
2 .M ) N
(µα
∀X.σ
1 .M ) σ
(µα
2

=
=
=
=

µα.M [β/γ]
M (α 6∈ F N (M ))
µβ σ2 .M [[β](− N )/[α](−)]
µβ σ1 [σ2 /X] .M [[β](− σ2 )/[α](−)]

In the last two axioms, we make uses of so-called ”mixed substitution”; for instance,
M [[β](− N )/[α](−)] means replacing occurances of the form [α]L in M by [β](L N ) recursively.
In the sequel, we frequently use the following syntactic sugar. First, we let ⊥ be the
type ∀X.X — the type of falsity. We may also write ¬σ for σ → ⊥. Using ⊥, we define the
“named term”
[β]M ≡ µα⊥ .[β]M : ⊥
(where M : σ, β : σ, with α fresh) and the µ-abstraction
µασ .M : σ ≡ µασ .[α](M σ)
for M : ⊥. It follows that µασ .[β]M = µασ .[β]M holds.
With this ⊥, we can express the double-negation elimination in λµ2 by making use of
both the polymorphic and classical features:
Cσ = λm¬¬σ .µασ .m (λxσ .[α]x) : ¬¬σ → σ
As expected, we have Cσ (λk¬σ .k M ) = M . The properties of ⊥ and Cσ will be further
studied later under parametricity assumptions.
2.2. Target: the {∃, ∧, ¬}calculus. In tthe literature, the second-order λ-calculus (λ2)
is often taken as the target of the CPS translation for λµ2. Fujita observed that it actually
suffices to consider a fragment of λ2 with negations, conjunctions and existential types as
a target [7]. In this paper we follow this insight.
τ

::= X | R | ¬τ | τ ∧ τ | ∃X.τ

¬τ can be considered as a shorthand of τ → R. The type R can be replaced by ∃X.¬X ∧ X,
but for simplicity we keep R as a type constant. The syntax of terms is a fairly standard one,
though for conjunctions we employ a slightly less familiar elimination rule (with let-binding)
so that it parallels that of the existential types.
Γ, x : τ, Γ′ ⊢ x : τ
Γ, x : τ ⊢ M : R
Γ ⊢ λxτ .M : ¬τ
Γ ⊢ M : ¬τ Γ ⊢ N : τ
Γ⊢MN :R

6

MASAHITO HASEGAWA

Γ ⊢ M : τ1 Γ ⊢ N : τ2
Γ ⊢ hM, N i : τ1 ∧ τ2
Γ ⊢ M : τ1 ∧ τ2 Γ, x : τ1 , y : τ2 ⊢ N : τ3
Γ ⊢ let hxτ1 , y τ2 i be M in N : τ3
Γ ⊢ M : τ1 [τ2 /X]
Γ ⊢ hτ2 , M i : ∃X.τ1
Γ ⊢ M : ∃X.τ1 Γ, x : τ1 ⊢ N : τ2 X 6∈ F T V (Γ, τ2 )
Γ ⊢ let hX, xτ1 i be M in N : τ2
Again, we employ the standard βη-axioms.
(λxσ .M ) N
λxσ .M x
let hx, yi be hL, M i in N
let hx, yi be M in N [hx, yi/z]
let hX, xi be hτ, M i in N
let hX, xi be M in N [hX, xi/z]

=
=
=
=
=
=

M [N/x]
M (x 6∈ F V (M ))
N [L/x, M/y]
N [M/z]
N [τ /X, M/x]
N [M/z]

3. CPS translation
3.1. The CPS translation. We present a call-by-name CPS translation which can be
considered as an extension of that introduced by Streicher [16, 39, 36] (rather than the
translations by Plotkin [29], Parigot [27] or Fujita [7] which introduce extra negations and
do not respect extensionality).
X◦ = X
(σ1 → σ2 )◦ = ¬σ1◦ ∧ σ2◦
(∀X.σ)◦ = ∃X.σ ◦
[[xσ ]]
[[λxσ1 .M σ2 ]]
[[M σ1 →σ2 N σ1 ]]
[[ΛX.M σ ]]
[[M ∀X.σ1 σ2 ]]
σ
[[µα 1 .[β σ2 ]M σ2 ]]
where

λhxσ , y τ i.M
λhX, y τ i.M

=
=
=
=
=
=

◦

x¬σ
◦
◦
λhx¬σ1 , kσ2 i.[[M ]] k
◦
λkσ2 .[[M ]] h[[N ]], ki
◦
λhX, kσ i.[[M ]] k
◦
λkσ1 [σ2 /X] .[[M ]] hσ2◦ , ki
◦
λασ1 .[[M ]] β

≡ λz σ∧τ .let hxσ , y τ i be z in M
≡ λz ∃X.τ .let hX, y τ i be z in M

RELATIONAL PARAMETRICITY AND CONTROL

7

3.2. Soundness. The type soundness follows from a straightforward induction.
Proposition 3.1 (type soundness).
Γ ⊢ M : σ | ∆ =⇒ ¬Γ◦ , ∆◦ ⊢ [[M ]] : ¬σ ◦
◦ when Γ is x : σ , . . . , x
◦
where ¬Γ◦ is x1 : ¬σ1◦ , . . . , xm : ¬σm
1
1
m : σm , and ∆ = α1 :
◦
◦
σ1 , . . . , αn : σn for ∆ = α1 : σ1 , . . . , αn : σn .

Note that (σ[τ /X])◦ ≡ σ ◦ [τ ◦ /X], [[M [N/x]]] ≡ [[M ]][[[N ]]/x], and also [[M [σ/X]]] ≡
[[M ]][σ ◦ /X] hold. Then we have the equational soundness:
Proposition 3.2 (equational soundness).
Γ ⊢ M = N : σ |∆ =⇒ ¬Γ◦ , ∆◦ ⊢ [[M ]] = [[N ]] : ¬σ ◦
In addition, we have the definability result:
Proposition 3.3 (fullness).
¬Γ◦ , ∆◦ ⊢ N : ¬σ ◦ =⇒ N = [[M ]] for some Γ ⊢ M : σ | ∆
This can be proved by providing an inverse translation of the CPS translation, so that
¬Γ◦ , ∆◦ ⊢ P : ¬σ ◦ =⇒ Γ ⊢ P −1 : σ | ∆
¬Γ◦ , ∆◦ ⊢ C : σ ◦ =⇒ Γ ⊢ C −1 [−σ ] : ⊥ | ∆
¬Γ◦ , ∆◦ ⊢ A : R =⇒ Γ ⊢ A−1 : ⊥ | ∆
hold, where
Program : ¬σ ◦
P ::= x | λk.A
◦
Continuation : σ C ::= k | hP, Ci | hσ ◦ , Ci | let hx, ki be C in C | let hX, ki be C in C
Answer : R
A ::= P C | let hx, ki be C in A | let hX, ki be C in A
as follows.

x−1 = x
= µkσ .A−1

◦
(λkσ .A)−1

k−1
hP, Ci−1
hσ ◦ , Ci−1
(let hx, ki be C1 in C2 )−1
(let hX, ki be C1 in C2 )−1

=
=
=
=
=

[k][−]
C −1 [− P −1 ]
C −1 [− σ]
C1−1 [λx.µk.C2−1 [−]]
C1−1 [ΛX.µk.C2−1 [−]]

(P C)−1 = C −1 [P −1 ]
(let hx, ki be C in A)−1 = C −1 [λx.µk.A−1 ]
(let hX, ki be C in A)−1 = C −1 [ΛX.µk.A−1 ]
This can be considered as a “continuation-grabbing style transformation” in the sense of
Sabry [35]. It follows that for any ¬Γ◦ , ∆◦ ⊢ M : ¬σ ◦ there exists ¬Γ◦ , ∆◦ ⊢ P : ¬σ ◦
generated by this grammar such that P = M — it suffices to take the β-normal form [7].
Moreover we can routinely show that [[P −1 ]] = P . Thus the CPS translation enjoys fullness:
all terms are definable modulo the provable equality. This definability is important for
relating the parametricity principles for the source and target calculi.

8

MASAHITO HASEGAWA

3.3. A semantic explanation. Here is a short explanation of why this CPS translation
works, intended for readers with category theoretic background — on the “categories of
continuations” construction [16, 39, 36], and on fibrations for polymorphic type theories
[17]. As a response category C with a response object R induces a control category RC
with RC (X, Y ) = C(RX , RY ), a fibred response category with finite products and simple
coproducts (for existential quantifiers) induces a fibred control category with finite products
and simple products (for universal quantifiers). Let us write CΓ for the response category
over the type-context Γ. We assume that the weakening functor π ∗ : CΓ → CΓ×A has a left
adjoint ∃A : CΓ×A → CΓ subject to the Beck-Chevalley condition. Thus
CΓ×A (X, π ∗ (Y )) ≃ CΓ (∃A (X), Y )
We then have

RCΓ×A (π ∗ (X), Y ) =
≃
≃
≃
≃
=

∗

CΓ×A (Rπ (X) , RY )
π ∗ (X)
)
CΓ×A (Y, RR
X
∗
R
CΓ×A (Y, π (R ))
X
CΓ (∃A (Y ), RR )
CΓ (RX , R∃A (Y ) )
RCΓ (X, ∃A (Y ))

Hence π ∗ , regarded as the weakening functor from RCΓ to RCΓ×A , has a right adjoint given
by ∃A , which can be used for interpreting the universal quantifier. Our CPS transformation
is essentially a syntactic interpretation of this semantic construction.
4. CPS semantics with the parametric target calculus
4.1. Parametricity for the target calculus. As the target calculus can be seen as a
subset of λ2 (via the standard encoding of the conjunctions and existential types), we can
define the relational parametricity for the target calculus in the same way as for λ2, e.g.
logic for parametricity [31, 40], system R [1], or system P [5]. One may directly define the
parametricity principle (often called the simulation principle) for the existential type, see
for example [31].
In this paper we only consider the relations constructed from the graphs of termsin-context, identity, and σ ∗ ’s obtained by the following construction, which we shall call
“admissible relations”.
Among admissible relations, the most fundamental are the graph relations. Given a
term f (x) : τ2 with a free variable x : τ1 we define its graph relation hx ⊢ f (x)i : τ1 ↔ τ2
(hf i for short) by u hf i v iff f (u) = v.
Given a type τ whose free type variables are included in X1 , . . . , Xn and admissible
relations s1 : τ1 ↔ τ1′ , . . . , sn : τn ↔ τn′ , we define an admissible relation τ ∗ as follows.
• Xi∗ = si : τi ↔ τi′
• R∗ is the identity relation on the terms of type R
• (¬τ )∗ : ¬τ [τ1 /X1 , . . . ] ↔ ¬τ [τ1′ /X1 , . . . ] is the relation so that f (¬τ )∗ g iff x τ ∗ y
implies f x R∗ g y (hence f x = g y)
• (τ ∧τ ′ )∗ : (τ ∧τ ′ )[τ1 /X1 , . . . ] ↔ (τ ∧τ ′ )[τ1′ /X1 , . . . ] is the relation so that u (τ ∧τ ′ )∗ v
iff u = hx, x′ i, v = hy, y ′ i and x τ ∗ y, x′ τ ′∗ y ′
• (∃X.τ )∗ : ∃X.τ [τ1 /X1 , . . . ] ↔ ∃X.τ [τ1′ /X1 , . . . ] is the relation so that u (∃X.τ )∗ v iff
u = hτ ′ , xi, v = hτ ′′ , yi and x τ [r/X]∗ y for some admissible r : τ ′ ↔ τ ′′

RELATIONAL PARAMETRICITY AND CONTROL

9

In the last case, the relation τ [r/X]∗ : τ [τ ′ /X] ↔ τ [τ ′′ /X] is defined as τ ∗ with X ∗ = r.
One may further define admissible relations ¬r, r ∧ s and ∃X.r for admissible r, s, so that
(¬τ )∗ = ¬τ ∗ , (τ ∧ τ ′ )∗ = τ ∗ ∧ τ ′∗ and (∃X.τ )∗ = ∃X.τ ∗ hold.
Let idτ : τ ↔ τ be the identity relation on the terms of type τ . The relational parametricity asserts that, for any τ whose free type variables are included in X1 , . . . , Xn and
τ1 , . . . , τn , M : τ [τ1 /X1 , . . . , τn /Xn ] implies M τ ∗ M with si = idτi .
Its consistency follows immediately from that of the parametricity for λ2.
Proposition 4.1. As consequences of the parametricity, we can derive:
(1) ∃X.X gives a terminal object ⊤ with a unique inhabitant ∗, so that for any M : ⊤
we have M = ∗.
(2) ∃X.¬(τ ∧ X) ∧ X (which could be rewritten as ∃X.(X → ¬τ ) ∧ X) gives a final
coalgebra νX.¬τ of ΛX.¬τ where X only occurs negatively in τ .
(3) (as an instance of the last case) the isomorphism ∃X.¬(τ ∧ X) ∧ X ≃ ¬τ holds if X
does not occur freely in τ .
Their proofs are standard, cf. papers cited above [31, 1, 40, 5].
Below we will see the implications of these parametricity results on the target calculus.
We refer to the λµ2-theory induced by the CPS translation into this parametric target
calculus as λµ2P .
4.2. The falsity type. As a first example, let us consider the falsity type ⊥ = ∀X.X in
λµ2. We have
⊥◦ = (∀X.X)◦ = ∃X.X ≃ ⊤
and
(σ → ⊥)◦ = ¬(σ ◦ ∧ ⊥◦ ) ≃ ¬(σ ◦ ∧ ⊤) ≃ ¬σ ◦
Since ∃X.X is terminal (with a unique inhabitant ∗) in the parametric target calculus,
◦
we obtain [[µασ .M ]] = λασ .[[M ]]∗ and [[[β]M ]] = λu∃X.X .[[M ]]β, which coincide with Streicher’s translation. As a consequence, the following equations on the named terms and
µ-abstractions are all validated in λµ2P .
(µασ1 →σ2 .M ) N
(µα∀X.σ1 .M ) σ2
[α′ ](µασ .M )
[α⊥ ]M

=
=
=
=

µβ σ2 .M [[β](− N )/[α](−)]
µβ σ1 [σ2 /X] .M [[β](− σ2 )/[α](−)]
M [α′ /α]
M

Thus the type ⊥ serves as the falsity type as found in some formulation of the λµ-calculus.
In addition, we can show that (σ, Cσ : ((σ → ⊥) → ⊥) → σ) is an algebra of the doublenegation monad ((−) → ⊥) → ⊥ on the term model.
4.3. Initial algebra? A more substantial example is the “initial algebra” µX.F [X] =
∀X.(F [X] → X) → X, with X positive in F [X] (here we see an unfortunate clash of µ’s for
the name-binding and for the fixed-point on types, but this should not cause any serious

10

MASAHITO HASEGAWA

problem). We calculate:
(µX.F [X])◦ =
=
≃
≃
≃
=
≃

(∀X.(F [X] → X) → X)◦
∃X.¬(¬F [X]◦ ∧ X) ∧ X
νX.¬¬F [X]◦
¬¬F [X]◦ [νX.¬¬F [X]◦ /X]
¬¬F [X]◦ [(µX.F [X])◦ /X]
¬¬(F [µX.F [X]])◦
((F [µX.F [X]] → ⊥) → ⊥)◦

This suggests that µX.F [X] is isomorphic not to F [µX.F [X]] but to its double negation
(F [µX.F [X]] → ⊥) → ⊥. One might think that this contradicts the standard experience on
λ2 with parametricity, where we have an isomorphism in : F [µX.F [X]] → µX.F [X]. Since
λµ2 subsumes λ2, we have this in in λµ2 too; however, it should not be an isomorphism,
regarding the CPS interpretation above (otherwise it causes a degeneracy). The truth is
that, in λµ2P , the term
in♯ = λm.µα.m (λx.[α](in x)) : ((F [µX.F [X]] → ⊥) → ⊥) → µX.F [X]
is an isomorphism. It still is not an initial algebra of (F [−] → ⊥) → ⊥; we shall further
consider this issue later. For now, we shall emphasize that the parametricity principle for
λ2 should not be used for λµ2, at least without certain constraint — otherwise in would be
an isomorphism, hence a degeneracy follows (because we have (σ → ⊥) → ⊥ ≃ σ for every
σ).
4.4. Other impredicative encodings. Recall other impredicative encodings of logical
connectives:
⊤ = ∀X.X → X
σ1 ∧ σ2 = ∀X.(σ1 → σ2 → X) → X
σ1 ∨ σ2 = ∀X.(σ1 → X) → (σ2 → X) → X
∃X.σ = ∀Y.(∀X.(σ → Y )) → Y
Their CPS translations into the parametric target calculus satisfy:
⊤◦
(σ1 ∧ σ2 )◦
(σ1 ∨ σ2 )◦
(∃X.σ)◦

≃
≃
≃
≃

R
¬(¬σ1 ◦ ∧ ¬σ2◦ )
¬¬σ1◦ ∧ ¬¬σ2◦
¬∃X.¬σ ◦

As easily seen, these defined logical connectives in the source calculus do not obey the
standard universal properties as in the parametric models of λ2. In short, they are all
“double-negated”, hence amount to some classical encodings:
• σ1 ∧ σ2 is not a cartesian product of σ1 and σ2 , but isomorphic to (σ1 → σ2 → ⊥) →
⊥. It is possible to add cartesian product types σ1 ×σ2 to λµ2, but then we also need
to add coproduct types τ1 + τ2 to the target calculus, so that (σ1 × σ2 )◦ = σ1◦ + σ2◦
and σ1 ∧ σ2 ≃ ¬¬(σ1 × σ2 ).
• ⊤ is not a terminal object, but isomorphic to ⊥ → ⊥. We can add a terminal object
1 to λµ2 and an initial object 0 to the target, so that 1◦ = 0 and ⊤ ≃ ¬¬1.
• σ1 ∨ σ2 is not a coproduct of σ1 and σ2 , but isomorphic to (σ1 → ⊥) → (σ2 → ⊥) →
⊥. If there is a coproduct σ1 + σ2 , then it should follow that σ ∨ τ ≃ ¬¬(σ + τ ).
On the other hand, it is not possible to enrich λµ2 with an initial object without
a degeneracy, cf. Selinger’s note on control categories [37]. Alternatively we might

RELATIONAL PARAMETRICITY AND CONTROL

11

add the “classical disjunction types” σ1 ℘σ2 [36] with (σ1 ℘σ2 )◦ = σ1◦ ∧ σ2◦ — hence
σ1 → σ2 ≃ ¬σ1 ℘σ2 and σ1 ∨ σ2 ≃ ¬¬σ1 ℘¬¬σ2 . We note that ⊥ = ∀X.X serves as
the unit of this classical disjunction.
• ∃X.σ does not work as the existential type; it is isomorphic to ¬∀X.¬σ.
4.5. Answer-type polymorphism. Note that the answer type R has been considered
just as a constant with no specific property. In fact we could have used any type for R —
Everything is defined polymorphically regarding R. Thus we can apply the “answer-type
polymorphism” principle (cf. [43]): in particular, a closed term of type σ in λµ2 can be
considered to be sent to a λ2-term of type ∀R.¬σ ◦ . This way of reasoning goes behind the
parametricity principle for our target calculus, but it is justified by the parametricity of λ2.
For instance, consider the type ⊤ = ∀X.X → X of λµ2. We have
∀R.¬⊤◦ ≃ ∀R.¬R
≃ ∀R.R → R
≃ 1
in λ2 with parametricity. This means that, although ⊤ is not a terminal object in λµ2, it
has a unique closed inhabitant. Similarly, we have ∀R.¬⊥◦ ≃ ∀R.R ≃ 0, thus we see that
there is no closed inhabitant of ⊥ in λµ2.
However, such reasonings based on the answer-type polymorphism become much harder
for more complicated types. The force of answer-type polymorphism in this setting seems
still not very obvious.
5. Focal parametricity
We have seen that the CPS semantics with respect to the target calculus with relational parametricity induces a reasonable equational theory λµ2P . However, here the
parametricity is used rather indirectly, via the CPS translation. We now consider a notion
of parametricity which is directly available within λµ2.
5.1. CPS translating relations. The key of formulating the relational parametricity is
the use of graph relations of terms (considered as representing a functional relation): without
graph relations, relational parametricity reduces to just the basic lemma of the (secondorder) logical relations. On the other hand, it does not have to allow all terms to be used
for constructing relations. In fact, in linear parametricity [30] only linear (or strict) maps
are allowed to be used for constructing graph relations, and this choice allows a weaker
notion of parametricity which can accommodate recursion. Naturally, we are led to look
for a characterisation of λµ-terms which can be used for graph relations without breaking
the soundness with respect to the CPS semantics into the parametric target calculus.
Now suppose that we are allowed to use the graph relation hf i : σ1 ↔ σ2 of a term
x : σ1 ⊢ f (x) : σ2 . To ensure the soundness of the use of this graph relation, we shall consider
the CPS translation of such relations. For instance, we hope that hf i will be sent to a relation
between types σ2◦ and σ1◦ in the target calculus. However, since x : ¬σ1◦ ⊢ [[f (x)]] : ¬σ2◦ , we
have some relation σ2◦ ↔ σ1◦ only when [[f (x)]] = λk.x (g (k)) for some k : σ2◦ ⊢ g(k) : σ1◦ in
the target calculus. If there is such g, we can complete the translation of the relations and
reduce the parametricity principle on λµ2 to the parametricity on the target calculus.

12

MASAHITO HASEGAWA

Fortunately, there is a way to characterise such “translatable” f ’s in the λµ-calculus
without performing the CPS-translation (modulo a technical assumption on the CPS-target,
known as “equalising requirement” [22]). It is the notion of “focus”, which we now recall
below.
5.2. Focus.
Definition 5.1. A λµ2-term M : σ1 → σ2 is called focal if it is an algebra morphism from
(σ1 , Cσ1 ) to (σ2 , Cσ2 ), i.e. the following diagram commutes.
(σ1 → ⊥) → ⊥
Cσ1

(M →⊥)→⊥

-

Cσ2

?

σ1

(σ2 → ⊥) → ⊥
?

M

- σ2

That is:
M (µασ1 .k (λxσ1 .[α]x)) = µβ σ2 .k (λxσ1 .[β](M x)) : σ2
holds for any k : (σ1 → ⊥) → ⊥.2
In any λµ2-theory, focal terms compose, and the identity λxσ .x is obviously focal. So,
the (equivalence classes of) focal maps form a category. Hereafter we shall call it the focus
of the λµ2-theory.
While this characterisation of focal maps is concise and closely follows the semantic
considerations in [36, 19], there is a subtle problem; the βη-axioms of λµ2 are too weak to
establish the focality of some important terms. This is because we have used the polymorphic feature of λµ2 for expressing Cσ — it involves the falsity type ⊥ = ∀X.X, but the
axioms of λµ2 do not guarantee that ⊥ does work properly. If there were not sufficiently
many focal maps, the parametricity principle restricted on focal maps would be useless.
To see this issue more clearly, we shall look at another “classical” combinator (the
Peirce law)
Pσ1 ,σ2 = λm.µασ1 .[α](m (λxσ1 .µβ σ2 .[α]x)) : ((σ1 → σ2 ) → σ1 ) → σ1
which does not make use of polymorphism, and the “abort” map (Ex Falso Quodlibet)
Aσ = λx⊥ .x σ : ⊥ → σ
which is defined without the classical feature. It is well known that the double-negation
elimination is as expressible as the Peirce law together with Ex Falso Quodlibet, see e.g.
[2]. This is also the case at the level of (uniformity of) proofs. Let us say that M : σ1 → σ2
is repeatable if
(M →σ3 )→M
- (σ2 → σ3 ) → σ2
(σ1 → σ3 ) → σ1
Pσ1 ,σ3

Pσ2 ,σ3

?

σ1

?

M

- σ2

2In [16], a focal map from σ to ⊥ is called a “C-term of type σ ”. C-terms of type σ with a free name
1
1
1

of σ2 correspond to focal maps from σ1 to σ2 , thus these notions (and the associated constructions of the
CPS target categories via C-terms (C-maps) [16] and via focus [36]) are essentially the same.

RELATIONAL PARAMETRICITY AND CONTROL

13

commutes for each σ3 ; and discardable if
Aσ 1

σ1

⊥

M

Aσ

@ 2
R
@
- σ2

commutes.
Proposition 5.2. In a λµ2-theory, M : σ1 → σ2 is focal if and only if it is both repeatable
and discardable.
We note that the corresponding result in the call-by-value setting has been observed by
Führmann [8] as the characterisation of algebraic values as repeatable discardable expressions. Here we follow his terminology.
This reformulation allows us to see that only the second diagram of A’s involves the
polymorphically defined ⊥ and needs to be justified by additional conditions.3 On the other
hand, the first diagram of P ’s is not problematic, as it does not make use of polymorphism
at all.
5.3. Additional axioms. To this end, we add more axioms to λµ2 before thinking about
parametricity. They are
(1) λxσ1 →σ2 .x N : (σ1 → σ2 ) → σ2 is discardable for any N : σ1
(2) λx∀X.σ .x σ1 : ∀X.σ → σ[σ1 /X] is discardable for any σ and σ1
(3) λxσ .[α]x : σ → ⊥ is discardable for any α : σ
which are equivalent to asking
(1) M (σ1 → σ2 ) N = M σ2 for any M : ⊥ and N : σ1
(2) M (∀X.σ) σ1 = M (σ[σ1 /X]) for M : ⊥
(3) [α](M σ) = M for M : ⊥ and α : σ (α 6∈ F N (M ))
and also equivalent to
(1) (µασ1 →σ2 .M ) N = µβ σ2 .M [[β](− N )/[α](−)]
(2) (µα∀X.σ1 .M ) σ2 = µβ σ1 [σ2 /X] .M [[β](− σ2 )/[α](−)]
(3) [α′ ](µασ .M ) = M [α′ /α]
Note that λµ2P discussed in Section 4 satisfies these conditions. Also we shall note that
λxσ1 →σ2 .x N , λx∀X.σ .x σ1 , λx⊥ .[α](x σ) are all repeatable in λµ2. Together with these
additional axioms, they become focal. (Alternatively, we could have ⊥ as a type constant
and assume the standard axiomatization of λµ-calculus with the falsity type [16, 36] — in
that case C is defined without polymorphism, and this problem disappears.)
Below we develop the focal parametricity principle on top of λµ2 with these additional
axioms.
3This problem was overlooked in the preliminary version of this paper [13] where it was wrongly assumed

that repeatability alone would imply focality.

14

MASAHITO HASEGAWA

5.4. A parametricity principle for λµ2. Given a focal f : σ1 → σ2 we define its graph
relation hf i : σ1 ↔ σ2 by u hf i v iff f u = v. Also, let idσ : σ ↔ σ be the identity relation
on the terms of type σ. In this paper we only consider the relations given by the graphs
of focal maps, identity, and σ ∗ ’s obtained by the following construction, which we shall call
“focal relations”.
Given a type σ whose free type variables are included in X1 , . . . , Xn and focal relations
s1 : σ1 ↔ σ1′ , . . . , sn : σn ↔ σn′ , we define a focal relation σ ∗ as follows.
• Xi∗ = si : σi ↔ σi′
• (σ → σ ′ )∗ : (σ → σ ′ )[σ1 /X1 , . . . ] ↔ (σ → σ ′ )[σ1′ /X1 , . . . ] is the relation so that f (σ →
σ ′ )∗ g iff x σ ∗ y implies (f x) σ ′∗ (g y)
• (∀X.σ)∗ : ∀X.σ[σ1 /X1 , . . . ] ↔ ∀X.σ[σ1′ /X1 , . . . ] is the relation so that u (∀X.σ)∗ v
iff (u σ ′ ) σ[r/X]∗ (v σ ′′ ) holds for any focal relation r : σ ′ ↔ σ ′′
The focal relational parametricity asserts that, for any σ whose free type variables are
included in X1 , . . . , Xn , M : σ[σ1 /X1 , . . . , σn /Xn ] implies M σ ∗ M with si = idσi .
Thus the only departure from the standard parametricity principle is the condition that
the graph relation construction is allowed only on focal maps. Note that this restriction
is necessary; if we apply parametricity to polymorphic terms ΛX.CX or ΛX.PX,σ , we will
get the naturality diagrams above for any term which is allowed to be used for the graph
relation construction.
5.5. On consistency and soundness. The consistency of focal parametricity (in the sense
that the equational theory of λµ2 with focal parametricity is not trivial) follows from the
fact that there are non-trivial parametric models of λ2 in which there is an object R so
τ
that the continuation monad T τ = RR satisfies the “equalising requirement” [22], i.e. each
component ητ : τ → T τ of its unit is an equaliser of ηT τ and T ητ . (Here we employ the
syntax of the CPS target calculus as an internal language for such models, where the CPS
translation is considered to give a semantic interpretation.) In such models, for any focal
term f : σ1 → σ2 , there exists a unique y : σ2◦ ⊢ g(y) : σ1◦ such that [[f x]] = λy.x (g(y)) (cf.
[36]).
Using this fact, given a focal relation r : σ1 ↔ σ2 , we construct an admissible relation
r ◦ : σ2◦ ↔ σ1◦ as follows. For a graph relation hf i : σ1 ↔ σ2 , we let hf i◦ = hgi : σ2◦ ↔ σ1◦
where g is the unique map as given above. For σ ∗ , σ ∗◦ is defined by straightforward
induction: (σ → σ ′ )∗◦ = ¬σ ∗◦ ∧ σ ′∗◦ , (∀X.σ)∗◦ = ∃X.σ ∗◦ (where the parameter relations si
are replaced by s◦i ).
Theorem 5.3. In such a model, given a focal relation r : σ1 ↔ σ2 , M r N implies
[[N ]] ¬r ◦ [[M ]].
Theorem 5.4 (consistency). Focal parametricity is consistent.
We do not know if the term model of the parametric target calculus satisfies the equalising requirement — if so, by the definability result, the parametricity on the target and the
focal parametricity on λµ2 should agree. Alternatively we should consider a refined target
calculus with a construct ensuring the equalising requirement, as detailed in Taylor’s work
on sober space (“a lambda calculus for sobriety” [41]). For now, we only know that one
direction is true (thanks to the definability).
Theorem 5.5. An equality derivable in λµ2P is also derivable in λµ2 with focal parametricity.

RELATIONAL PARAMETRICITY AND CONTROL

15

6. Examples
We show that certain impredicative encodings in λµ2 satisfy universal properties with
respect to the focus using the focal parametricity principle.
6.1. Focal decomposition. We start with a remark on the following “focal decomposition”
[36] (analogous to the linear decomposition σ1 → σ2 =!σ1 ⊸ σ2 [10]): there is a bijective
correspondence between terms of σ1 → σ2 and focal terms of ¬¬σ1 → σ2 natural in σ1 and
focal σ2 .
f : ¬¬σ1 → σ2 focal
f ♭ = f ◦ ησ1 = λxσ1 .f (λk.k x) : σ1 → σ2
g♯

= Cσ2 ◦ ¬¬g =

g : σ1 → σ2
σ
λm.µβ 2 .m (λxσ1 .[β](g x))

: ¬¬σ1 → σ2 focal

♯

♭

Proposition 6.1. g♯ = g for any g : σ1 → σ2 , while f ♭ = f holds for f : ¬¬σ1 → σ2 if
and only if f is focal.
6.2. Falsity as a focally initial object. Now we shall proceed to reason about impredicative encodings in λµ2. The first example is the falsity ⊥ = ∀X.X.
First, we note that Aσ = λx⊥ .x σ : ⊥ → σ is focal. The parametricity on ⊥ says x ⊥∗ x
for any x : ⊥. Since hAσ i : ⊥ ↔ σ, we have x ⊥ hAσ i x σ, i.e. Aσ (x ⊥) = x ⊥ σ = x σ. By
extensionality we get x = x ⊥ for x : ⊥.
Now suppose that g : ⊥ → σ is focal. Again by the parametricity on ⊥ we know x ⊥∗ x
for any x : ⊥, hence x ⊥ hgi x σ. Thus g (x ⊥) = x σ; but x = x ⊥, so we have g x = x σ,
hence g = λx⊥ .x σ = Aσ .
So we conclude that Aσ is the unique focal map from ⊥ to σ. This means that ⊥ is
initial in the focus.
6.3. Focally initial algebra. As in λ2, there is a fairly standard encoding
µX.F [X] = ∀X.(F [X] → X) → X
foldσ = λaF [σ]→σ .λxµX.F [X] .x σ a : (F [σ] → σ) → µX.F [X] → σ
in = λy.ΛX.λkF [X]→X .k (F [foldX k] y) : F [µX.F [X]] → µX.F [X]
for which the following diagram commutes (just by β-axioms).
F [µX.F [X]]

in -

F [fold a]

µX.F [X]
fold a

?

F [σ]

a

?
- σ

Therefore in is a weak initial F -algebra. However, as we noted before, in is not an initial
F -algebra — in fact it is not even an isomorphism. By applying the focal decomposition

16

MASAHITO HASEGAWA

above, we obtain the commutative diagram
¬¬F [µX.F [X]]
¬¬F [fold a♭ ]

in♯-

µX.F [X]
fold a♭

?

¬¬F [σ]

?
- σ

a

for any focal a : ¬¬F [σ] → σ. We show that fold a♭ is the unique focal map making this
diagram commute, thus in♯ is an initial ¬¬F [−]-algebra in the focus.
We sketch a proof which is fairly analogous to that for the corresponding result in
parametric λ2 as given in [1]. First, from the parametricity on µX.F [X] we obtain that
F [σ1 ]

a-

F [h]

h

?

F [σ2 ]

b

µX.F [X]

σ1

?
- σ2

implies

folda

||

σ1
h

?

µX.F [X]

?
- σ2

fold b

whenever h is focal. We also have M (µX.F [X]) in = M for any M : µX.F [X] as a corollary
(thanks to extensionality). By combining these observations, now we have the desired result.
That is, if h : µX.F [X] → σ is focal and satisfies h ◦ in♯ = a ◦ ¬¬F [h], then
foldσ a♭ x = h (foldµX.F [X] in x)
= h (x (µX.F [X]) in)
= hx
so by extensionality we conclude foldσ a♭ = h. This also implies that in♯ is an isomorphism,
with the inverse given by fold¬¬µX.F [X] (¬¬F [in]).
As a special case, by letting F be a constant functor, we obtain isomorphisms between
(σ → ⊥) → ⊥ and ∀X.(σ → X) → X where X is not free in σ. With some further
calculation we see that in♯ = λm.ΛX.λkσ→X .µαX .m (λxσ .[α](k x)) is the inverse of λn.n ⊥ :
(∀X.(σ → X) → X) → (σ → ⊥) → ⊥. We will see more about this isomorphism in Section
7.
6.4. The type of Church numerals. We conclude this section by a remark on the type
of Church numerals N = ∀X.X → (X → X) → X. Recall that, in λ2 with parametricity,
N is an initial algebra of ∀X.X → (− → X) → X ≃ 1 + (−), i.e. a natural numbers object,
whose closed inhabitants are equal to the Church numerals Sn O which can be given by, as
usual,
O = ΛX.λxX f X→X .x
: N
S = λnN .ΛX.λxX f X→X .f (n X x f ) : N → N
It is no longer true in λµ2, as observed by Parigot, as there are closed inhabitants which
are not equal to Church numerals, e.g.
µαN .[α](S (µβ N .[α]O)) = ΛX.λxX f X→X .µαX .[α](f (µβ X .[α]x)) : N
In contrast, N in λµ2 with focal parametricity is a focally initial algebra of ∀X.X → (− →
X) → X ≃ ⊥ → (− → ⊥) → ⊥; this can be shown in the same way as the case of focally

RELATIONAL PARAMETRICITY AND CONTROL

17

initial algebras. Spelling this out, we have a focal map in : (⊥ → (N → ⊥) → ⊥) → N,
and for any focal g : (⊥ → (σ → ⊥) → ⊥) → σ there exists a unique focal foldσ g : N → σ
making the following diagram commute.
⊥ → (N → ⊥) → ⊥

in -

N

⊥→(foldσ g→⊥)→⊥

foldσ g

?

⊥ → (σ → ⊥) → ⊥

g

?
- σ

To see this, it is useful to observe the following bijective correspondence (a variant of the
focal decomposition): given focal g : (⊥ → (σ → ⊥) → ⊥) → σ we have
go = g (λx⊥ kσ→⊥ .x)
: σ
gs = λy σ .g (λx⊥ kσ→⊥ .k y) : σ → σ
and conversely, for a : σ and f : σ → σ we have a focal map
ϕa,f = λm⊥→(σ→⊥)→⊥ .µασ .m ([α]a) (λy σ .[α](f y)) : (⊥ → (σ → ⊥) → ⊥) → σ
It follows that (ϕa,f )o = a and (ϕa,f )s = f hold for any a and f , while ϕgo ,gs = g for any
focal g. Now we define
foldA g = λnN .n A go gs : N → A
in
= ϕO,S
: (⊥ → (N → ⊥) → ⊥) → N
It then follows that the diagram above commutes — and the focal parametricity implies
that foldA g is the unique such focal map.
7. A general characterisation
So far, we concentrated on the relational parametricity for λµ2. One may feel that
this story is very specific to the case of λµ2, or of the first-class continuations, and is not
immediately applicable to other computational effects.
In this section we describe an alternative characterisation of the focus, which makes
sense in any extension of λ2. Namely, we show that, any λ2-theory is equipped with a monad
L, such that each type is equipped with an algebra structure — and then see that, in the
case of λµ2 with focal parametricity, this monad L is isomorphic to the double-negation
(continuation) monad, and focal maps are precisely the algebra maps of the monad L.
This suggests a natural generalisation of this work to a theory of parametricity for general
computational effects.
7.1. A monad on λ2. Let Lσ = ∀X.(σ → X) → X (with no free X in σ), and define
ησ
= λxσ .ΛX.λkσ→X .k x
: σ → Lσ
2
µσ
= λz L σ .ΛX.λkσ→X .z X (λy Lσ .y X k) : L2 σ → Lσ
L(f ) = λy Lσ1 .ΛX.λhσ2 →X .y X (h ◦ f )
: Lσ1 → Lσ2 (f : σ1 → σ2 )
Proposition 7.1. On the term model of any λ2-theory, (L, η, µ) forms a monad.

18

MASAHITO HASEGAWA

One might think that this is trivial as Lσ is isomorphic to σ when we assume the
standard parametricity. This is not always the case however, as we have already seen,
Lσ ≃ (σ → ⊥) → ⊥ in the focally parametric λµ2.
Proposition 7.2. ασ = λy Lσ .y σ (λxσ .x) : Lσ → σ is an algebra of the monad (L, η, µ).
Thus each σ is canonically equipped with an algebra structure ασ . Again one may think
that this is trivial, as under the standard parametricity ασ is just an isomorphism with ησ
being an inverse. However, again it is not the case in a non-trivial λµ2-theory.
Now we define the notion of linear maps in terms of the monad L and the canonical
algebras ασ — this is close to what we do in (axiomatic) domain theory for characterising
the strict maps, and also in control categories for characterising the focal maps.
Definition 7.3. f : σ1 → σ2 is linear when it is an algebra morphism from ασ1 to ασ2 , i.e.
f ◦ ασ1 = ασ2 ◦ L(f ) holds.
Lσ1

L(f )

- Lσ2

ασ1

ασ2

?

σ1
That is, f is linear when

f

?
- σ2

f (M σ1 (λxσ1 .x)) = M σ2 f
holds for any M : Lσ1 . We may write f : σ1 ⊸ σ2 for a linear f : σ1 → σ2 . Under the
standard parametricity every f : σ1 → σ2 is linear, while for focal parametricity on λµ2
we have that linear maps are precisely the focal maps (see below). In passing, we note the
following interesting observation.
Proposition 7.4. In a λ2-theory, the following conditions are equivalent.
(1) algebras on σ1 → σ2 and ∀X.σ are determined in the pointwise manner, i.e.
ασ1 →σ2 = λf L(σ1 →σ2 ) .λxσ1 .ασ2 (L(λgσ1 →σ2 .g x) f )
α∀X.σ = λxL(∀X.σ) .ΛX.ασ (L(λy ∀X.σ .y X) x)
(2) λxσ1 →σ2 .x N is linear for any N : σ1 , and λx∀X.σ .x σ1 is linear for any σ and σ1 .

Note that they are very close to the “additional axioms” for λµ2 discussed in Section 5.
Also note that, if a λ2-theory satisfies one of these conditions, µσ and αLσ agree for every
σ. and we have a “linear decomposition” correspondence between the maps of σ1 → σ2 and
the linear maps of Lσ1 → σ2 .
7.2. Focal maps as algebra maps. Now we shall consider the double-negation monad
¬¬σ = (σ → ⊥) → ⊥ on λµ2 with focal parametricity.
Proposition 7.5. In a focally parametric λµ2-theory, Cσ : ¬¬σ → σ is an algebra of the
double-negation monad.
Corollary 7.6. f : σ1 → σ2 is focal if and only if it is an algebra map from Cσ1 to Cσ2 .
Proposition 7.7. The monad (L, η, µ) is isomorphic to the double negation monad in the
≃
focally parametric λµ2, with λxLσ .x ⊥ : Lσ → ¬¬σ.

RELATIONAL PARAMETRICITY AND CONTROL

19

Proposition 7.8. The following diagram commutes in a focally parametric λµ2-theory:
λxLσ .x ⊥-

Lσ

@
@
R
@

ασ

¬¬σ

Cσ

σ

Corollary 7.9. f : σ1 → σ2 is linear if and only if it is focal.
Thus a focal map in a focally parametric λµ2-theory can be characterised just in terms
of the monad L which is defined for arbitrary λ2-theory.
We believe that the monad L deserves much attention. It has been considered trivial,
but now we know that it does characterise an essential notion (focus) in the case of relational
parametricity under the presence of control feature. In fact, the story does not end here;
under the presence of non-termination or recursion, L behaves like a lifting monad — indeed
it is a lifting in the theory of linear parametricity, because
Lσ = ∀X.(σ → X) → X = ∀X.!(!σ ⊸ X) ⊸ X ≃ !σ
where the last isomorphism follows from the fact that ∀X.!(F [X] ⊸ X) ⊸ X gives an
initial algebra of F , cf. [4].
These observations suggest that there exists a general framework similar to (axiomatic
or synthetic) domain theory where the lifting monad can be replaced by any strong monad
— a continuation monad for example — on which a theory of parametricity for general
computational effects can be built. Recently, Alex Simpson has made a progress in this
direction, by developing a two-level polymorphic type theory (for interpreting types and
algebras of a monad) in a constructive universe [38]. His work fits very well with the case
of linear parametricity for recursion; it is plausible that it also explains the case of focal
parametricity for first-class control.
8. Conclusion and future work
We have studied the relational parametricity for λµ2, first by considering the CPS
translation into a parametric fragment of λ2, and then by directly giving a constrained
parametricity for λµ2. The later, which we call “focal parametricity”, seems to be a natural
parametricity principle under the presence of first-class controls — in the same sense that
linear parametricity works under the presence of recursion and non-termination.
There remain many things to be addressed in future. In the previous section, we already
discussed a research direction towards a relational parametricity for general effects. Below
we shall briefly mention some future work more closely related to the main development of
this paper.
Firstly, we are yet to complete the precise comparison between focal parametricity on
λµ2 and the parametricity on the CPS target calculus. This involves some subtle interaction
between parametricity and a technical condition (equalising requirement).
Secondly, we should study focal parametricity for extensions of λµ2. As we observed,
λµ2 with focal parametricity does not have many popular datatypes, e.g. cartesian products,
and classical disjunction types which however can be added with no problem. Adding
general initial algebras is problematic (having an initial object already means inconsistency),
but it might be safe to add certain carefully chosen instances. On the other hand, final
coalgebras seem less problematic, though a generic account for them in λµ2 is still missing.

20

MASAHITO HASEGAWA

Perhaps we also need to consider the CPS translation of such datatypes (cf. [3]) in a
systematic way.
An interesting topic we have not discussed in this paper is the Filinski-Selinger duality
[6, 36] between call-by-name and call-by-value calculi with control primitives. In fact it is
straightforward to consider its second-order extension: in short, universal quantifiers in callby-name (as studied in this paper) amount to existential quantifiers in call-by-value. We
are not sure if the call-by-value calculus with existential quantifiers itself is of some interest.
However, it can be a good starting point to understand the call-by-value parametric polymorphism (possibly with computational effects), from both syntactic and semantic aspects.
In particular, it should provide new insights on the famous difficulty of accommodating
first-class continuations in ML type system [11].
Finally, we also should consider if there is a better (ideally semantic) formulation of
focal relations. In this paper we only consider those coming from focal maps, but it seems
natural to regard a subalgebra (of the double-negation monad) of Cσ1 ×σ2 as a focal relation
between σ1 and σ2 , where we assume the presence of cartesian product σ1 × σ2 . This looks
very closely related to Pitts’ ⊤⊤-closed relations for λ2 with recursion [28].
Acknowledgement
I thank Ken-etsu Fujita for discussions and cooperations related to this work. I am also
grateful to Ryu Hasegawa, Paul-André Melliès and Alex Simpson for comments, discussions
and encouragements.
References
[1] M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. Theoret. Comput. Sci.
121:9–58, 1993.
[2] Z.M. Ariola and H. Herbelin. Minimal classical logic and control operators. In Proc. Automata, Languages and Programming, Springer Lecture Notes in Comput. Sci. 2719, pp.871–885, 2003.
[3] G. Barthe and T. Uustalu. CPS translating inductive and coinductive types. In Proc. Partial Evaluation
and Semantics-Based Program Manipulation, pp.131–142, 2002.
[4] G.M. Bierman, A.M. Pitts, and C.V. Russo. Operational properties of Lily, a polymorphic linear lambda
calculus with recursion. In Proc. Higher Order Operational Techniques in Semantics, Electronic Notes
in Theoretical Computer Science 41, 2000.
[5] B.P. Dunphy. Parametricity as a Notion of Uniformity in Reflexive Graphs. PhD thesis, University of
Illinois, 2002.
[6] A. Filinski. Declarative continuations: an investigation of duality in programming language semantics.
In Proc. Category Theory and Computer Science, Springer Lecture Notes in Comput. Sci. 389, pp.224–
249, 1989.
[7] K. Fujita. Galois embedding from polymorphic types into existential types. In Proc. Typed Lambda
Calculi and Applications, Springer Lecture Notes in Comput. Sci. 3461, pp.194–208, 2005.
[8] C. Führmann. Varieties of effects. In Proc. Foundations of Software Science and Computation Structures,
Springer Lecture Notes in Comput. Sci. 2303, pp.144–159, 2002.
[9] J.-Y. Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre
supérieur. Thèse d’Etat, Université Paris VII, 1972.
[10] J.-Y. Girard. Linear logic. Theoret. Comp. Sci. 50:1–102, 1987.
[11] B. Harper, B.F. Duba and D. MacQueen. Typing first-class continuations in ML. J. Funct. Programming
3(4):465–484.
[12] M. Hasegawa. Semantics of linear continuation-passing in call-by-name. In Proc. Functional and Logic
Programming, Springer Lecture Notes in Comput. Sci. 2998, pp.229–243, 2004.

RELATIONAL PARAMETRICITY AND CONTROL

21

[13] M. Hasegawa, Relational parametricity and control (extended abstract). In Proc. Logic in Computer
Science, pp.72–81, 2005.
[14] M. Hasegawa and Y. Kakutani. Axioms for recursion in call-by-value. Higher-Order and Symbolic Comput. 15(2/3):235–264, 2002.
[15] R. Hasegawa. Categorical data types in parametric polymorphism. Math. Struct. Comp. Sci. 4(1):71–
109, 1994.
[16] M. Hofmann and T. Streicher. Completeness of continuation models for λµ-calculus. Inf. Comput.
179(2):332–355, 2002.
[17] B. Jacobs. Categorical Logic and Type Theory. Elsevier, 1999.
[18] Y. Kakutani. Duality between call-by-name recursion and call-by-value iteration. In Proc. Computer
Science Logic, Springer Lecture Notes in Comput. Sci. 2471, pp.506–521, 2002.
[19] Y. Kakutani and M. Hasegawa. Parameterizations and fixed-point operators on control categories.
Fundam. Inform. 65(1/2):153–172, 2005.
[20] J. Lambek and P. Scott (1986) Introduction to Higher-order Categorical Logic. Cambridge University
Press.
[21] R. Matthes. Parigot’s second order λµ-calculus and inductive types. In Proc. Typed Lambda Calculi and
Applications, Springer Lecture Notes in Comput. Sci. 2044, pp.329–343, 2001.
[22] E. Moggi. Notions of computation and monads. Inf. Comput. 93(1):55–92, 1991.
[23] K. Nakazawa and M. Tatsuta. Strong normalization proof with CPS-translation for second order classical
natural deduction. J. Symb. Log. 68(3):851–859, 2003. Corrigendum: J. Symb. Log. 68(4):1415–1416,
2003.
[24] C.-H.L. Ong. A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations (preliminary extended abstract). In Proc. Logic in Computer Science, pp.230–241, 1996.
[25] C.-H.L. Ong and C.A. Stewart. A Curry-Howard foundation for functional computation with control.
In Proc. Principles of Programming Languages, pp.215–227, 1997.
[26] M. Parigot. λµ-calculus: an algorithmic interpretation of classical natural deduction. In Proc. Logic
Programming and Automated Reasoning, Springer Lecture Notes in Comput. Sci. 624, pp.190–201,
1992.
[27] M. Parigot. Proofs of strong normalisation for second order classical natural deduction. J. Symb. Log.
62(4):1461–1479, 1997.
[28] A. Pitts, Parametric polymorphism and operational equivalence. Math. Struct. Comp. Sci. 10:321–359,
2000.
[29] G.D. Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoret. Comput. Sci. 1(1):125–159,
1975.
[30] G.D. Plotkin. Type theory and recursion (extended abstract). In Proc. Logic in Computer Science,
pp.374, 1993.
[31] G.D. Plotkin and M. Abadi. A logic for parametric polymorphism. In Proc. Typed Lambda Calculi and
Applications, Springer Lecture Notes in Comput. Sci. 664, pp.361–375, 1993.
[32] A.J. Power and E. Robinson. Premonoidal categories and notions of computation. Math. Struct. Comp.
Sci. 7(5):453–468, 1997.
[33] J.C. Reynolds. Towards a theory of type structure. In Proc. Colloque sur la Programmation, Springer
Lecture Notes in Comput. Sci. 19, pp.408–425, 1974.
[34] J.C. Reynolds. Types, abstraction and parametric polymorphism. In Proc. IFIP 9th World Computer
Congress, Information Processing 83, pp.513–523, 1983.
[35] A. Sabry. Note on axiomatizing the semantics of control operators. Tech. Rep. CIS-TR-96-03, University
of Oregon, 1996.
[36] P. Selinger. Control categories and duality: on the categorical semantics of the lambda-mu calculus.
Math. Struct. Comp. Sci. 11(2):207–260, 2001.
[37] P. Selinger. Some remarks on control categories. Manuscript, 2003.
[38] A. Simpson. Relational parametricity for computational effects. Manuscript, 2006.
[39] T. Streicher and B. Reus. Classical logic, continuation semantics and abstract machines. J. Funct.
Program. 8(6):543–572, 1998.
[40] I. Takeuti. An axiomatic system of parametricity. Fundam. Inform. 33(4):397–432, 1998.
[41] P. Taylor. Sober spaces and continuations. Theory and Applications of Categories 10(12):248–300, 2002.

22

MASAHITO HASEGAWA

[42] H. Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh,
1997.
[43] H. Thielecke. Answer type polymorphism in call-by-name continuation passing. In Proc. European Symposium on Programming, Springer Lecture Notes in Comput. Sci. 2986, pp.279–293, 2004.
[44] P. Wadler. Theorems for free! In Proc. Functional Programming Languages and Computer Architecture,
pp.347–359, 1989.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view
a copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 559 Nathan Abbott Way, Stanford, California 94305, USA.

