Extensional Universal Types for Call-by-Value
Kazuyuki Asada
Research Institute for Mathematical Sciences, Kyoto University, Japanasada@kurims.kyoto-u.ac.jp

Abstract. We propose λc 2η -calculus, which is a second-order polymorphic call-by-value calculus with extensional universal types. Unlike product types or function types in call-by-value, extensional universal types
are genuinely right adjoint to the weakening, i.e., β-equality and ηequality hold for not only values but all terms. We give monadic stylecategorical semantics, so that the results can be applied also to languages like Haskell. To demonstrate validity of the calculus, we constructconcrete models for the calculus in a generic manner, exploiting “relevant” parametricity. On such models, we can obtain a reasonable classof monads consistent with extensional universal types. This class admits
polynomial-like constructions, and includes non-termination, exception,
global state, input/output, and list-non-determinism.

1

Introduction

Polymorphic lambda calculi like System F [11,30] have been widely studied andalso used in some practical programing languages like ML and Haskell as theirsemantical background. With universal types in them, we can abstract terms defined uniformly for each type into one term, which improves usability, efficiency,
readability and safety. Moreover in impredicative polymorphic lambda calculi,
we can encode various datatypes like products, coproducts, initial algebras, andfinal coalgebras with universal types. These datatypes have merely weak universal properties in System F, but they are truly universal if we assume relationalparametricity [31,34,29,1,16,7].
As well as purely functional calculi, extensions of polymorphic lambda calculi
to call-by-name calculi/languages with some computational effects have beenstudied: with a fixed-point operator [28,4,5], and with first-class continuations[14].
While call-by-value is one of the most frequently used evaluation strategy
in practical programing languages, extensions to call-by-value polymorphic languages raise a subtle problem on the treatment of universally typed values.
Suppose that we have a type-abstracted term Λα.M . Then, is this a value atall? Or should we treat this as a value, only when M is a value? It corresponds
to the choice whether we evaluate M under the type abstraction, or do not (asfunction closure). This problem does not occur in modern ML, because, due tovalue restriction, M must always be a value.
When we set Λα.M as a value only when so is M , then we can obtain
extensional universal types, i.e., “type” η-equality, for some reasonable class of2effects. We call the η-equality Λα.M α = M (α ∈/ FTV (M )) for type abstraction
type η-equality, and also the β-equality (Λα.M ) σ = M [σ/α] for type abstraction
type β-equality. Clearly, if we treat Λα.M as a value for any term M , then typeη-equality does not hold in general, as function types in call-by-value.
We expect that such type η-equality can be useful for program transformation
to optimize programs. Also we can use it when reasoning with parametricity forcall-by-value, for type η-equality is often used in parametric reasoning.
In the present paper we propose a second-order polymorphic call-by-value
lambda calculus with extensional universal types. We give syntax and its soundand complete categorical semantics, and describe how we can construct concretemodels with a variety of computational effects.
Our main contribution is to show that, for some parametric models or semantic setting, we can obtain a reasonable class of effects which are compatible
with extensional universal types. The class includes non-termination, exception,
global state, input/output, and list-non-determinism. We can not show at present
whether (commutative) nondeterminism (like finite or infinite powersets, multisets and probabilistic non-determinism) and continuations belong to the class ofmodels or not.
We use Moggi’s monadic semantics [25,26,27,2] rather than direct-style semantics for call-by-value calculi [10,21]. One reason is that it is easier to represent
the class of effects considered in the present paper. The monads modeling theeffects mentioned above are respectively lifting monad (−)+1, exception monads
S(−) + E, global state monads ((−) × S) , input monads µβ. (−) + β U , output
monads µβ. (−) + (U × β), and the list monad µβ.1 + (−) × β. As these examples, this class is characterized as that of all “polynomial” monads constructedby constants, products, separated sum, powers, final coalgebras, and linearly
initial algebras; the last construction is explained in Section 6.4.
One more reason to use monadic semantics is because we can apply the
results to call-by-name (meta-)languages with monads like Haskell, as well as
to call-by-value languages as object languages like ML. In (some simplified)
Haskell, only fixed-point operators involving the non-termination effect exists inthe call-by-name object language, and other effects are treated via monadic styletranslations with various monads. The semantics which we give with “relevant”
parametricity and fixed-point operators in Section 6 is close to such subset of
Haskell, with extensional universal types.
1.1

Related Work

Harper et al. studied two kinds of call-by-value (and two kinds of call-by-name)extensions of the higher order polymorphic lambda calculus System Fω with firstclass continuations [12]. The difference between the two call-by-value extensions
is exactly as above, i.e., whether, for a type-abstracted term, we evaluate theinside of the body or not. They took an operational semantics-based approach,and noted there the failure of proving the preservation theorem which assertsthat a closed answer-typed term is evaluated to a closed answer-typed term. Thus
first-class continuations raise difficulty to obtain extensional universal types.

3

Recently in [22], Møgelberg studied polymorphic FPC, a call-by-value functional language with recursive types and hence a fixed-point operator. The universal types in this language are not designed to be extensional. However, it
seems that we can make it extensional because the effect used there is nontermination, though the problems to adjust other features of the language likerecursive types are not trivial.
An extension of System F with parametricity to call-by-push-value [20] wasalso studied [23]. The paradigm of call-by-push-value is similar to that of themonadic metalanguages, and it might be possible to express our results in termsof call-by-push-value. Call-by-push-value can be also used to translate call-byname languages as done in [24].
1.2

OutlineIn Section 2, we introduce two second order computational lambda calculi. Oneis λc 2η -calculus which has extensionality on universal type, and the other is
λc 2-calculus which does not.
Section 3 is devoted to preliminaries for semantics in later sections. In Section
4, we give categorical semantics for the calculi given in Section 2. These sections
3 and 4 may be skipped by readers who are not particularly interested in generalsemantic framework.
In Section 5, we start to look at concrete models for λc 2η -calculus. First we
describe a class of monads which admit extensional universal types, then weshow in two sections that they indeed form concrete models. In Section 5, wetreat parts which hold in relatively general, i.e., only by categorical property andby parametricity. In Section 6, we consider more specific models with fixed-point
operators and “relevant” parametricity.
Lastly, we give some concluding remarks in Section 7.

2

Second Order Computational Lambda Calculi

In this section, we introduce two calculi: second order computational λ-calculus(λc 2-calculus for short) and second order computational λ-calculus with extensional universal types (λc 2η -calculus for short). These are extensions of Moggi’s
computational lambda calculus (λc -calculus), listed in Figure 1, with universal
types.
We give the λc 2-calculus in Figure 2, and the λc 2η -calculus in Figure 3.
Note that the classes of values include e.g. π1 hV, V 0 i. A “value” here means an“effect-free” term, rather than a canonical form.
The differences between the λc 2-calculus and the λc 2η -calculus are not in thedefinitions of types or terms but only in equation theories, i.e., the values andthe axioms. The universal types in the λc 2-calculus satisfy type β-equality for
any term and type η-equality for only values, while those in the λc 2η -calculus
satisfy type β- and η-equality for any term. We call such universal types with full
type η-equality extensional universal types. In the paper we put the focus on the

4Types σ ::= b | σ → σ | 1 | σ × σ
Terms M ::= x | cσ | λxσ .M | M M | ∗ | hM, M i | π0 M | π1 M
Values V ::= x | cσ | λxσ .M | ∗ | hV, V i | π0 V | π1 V
Evaluation Contexts E ::= [−] | EM | V E | hE, M i | hV, Ei | π0 E | π1 E
where b ranges over base types, and cσ ranges over constants of type σ
Typing Rules:Γ `x:σ(x: σ ∈ Γ )Γ `∗:1Γ ` cσ : σ

Γ, x: σ ` M : τΓ ` λxσ .M : σ → τΓ `M :σ Γ `N :τΓ ` hM, N i : σ × τΓ `M :σ→τ Γ `N :σΓ ` MN : τΓ `M :σ×τΓ ` π0 M : σΓ `M :σ×τΓ ` π1 M : τ

πi hV0 , V1 i = Vi(i = 0, 1)

Axioms:(λxσ .M ) V = M [V /x]
λxσ .V x = V
V =∗

(x ∈
/ FV (V ))(V : 1)hπ0 V, π1 V i = V(λxσ .E [x]) M = E [M ](x ∈/ FV (E))

Fig. 1. The λc -calculus

λc 2η -calculus, to demonstrate how many effects are consistent with extensional
universal types.
In Section 6, we give relevant parametric models with fixed-point operators
as concrete models for the λc 2η -calculus. And there is a reasonably wide classof monads on the models, including non-termination, exception, global state,
input, output, and list-non-determinism.
Such fixed-point operators are not included in the syntax of the λc 2η -calculus.
Also, the λc 2η -calculus includes no proper axioms which induce computational
effects, as well as the λc -calculus. However, with such models, we will be able
to extend the λc 2η -calculus with suitable axioms and terms which induce suchcomputational effects, and also with call-by-value fixed-point operators [15]. Alternatively, we will also be able to define “second order monadic metalanguages”
which have call-by-name fixed-point operators [32] and in which we can simulate
such extended λc 2η -calculi by use of corresponding monads.

3

Preliminaries for Semantics

This section is devoted to preliminaries for some category theoretical notions.
Notation: ‘⇒’ is used for exponentials in a CCC (cartesian closed category).
An identity on A is written also as just A. For 2-cells, ‘∗’ and ‘◦’ mean horizontal
and vertical compositions respectively.
For a functor p being a fibration, we say an object X is over an object I(resp. an arrow f is over an arrow u) if pX = I (resp. pf = u). A functor

5Types σ ::= ... | α | ∀α.σ
Terms M ::= ... | Λα.M | M σ

Values V ::= ... | Λα.M
Evaluation Contexts E ::= ... | Eσ

Typing Rules: All the rules in the λc -calculus in which a kind context Ξ is added tothe all contexts, and:
Ξ | Γ ` M : ∀α.σ
Ξ | Γ ` M τ : σ [τ /α]Ξ, α | Γ ` M : σ(α ∈/ FTV (Γ ))Ξ | Γ ` Λα.M : ∀α.σ

Axioms: All the axioms in the λc -calculus where the evaluation contexts are extended
as above, and:(Λα.M ) σ = M [σ/α]Λα.V α = V(α ∈/ FTV (V ))Fig. 2. The λc 2-calculus, extended from the λc -calculus

Types σ ::= ... | α | ∀α.σ
Terms M ::= ... | Λα.M | M σ

Values V ::= ... | Λα.V | V σ
Evaluation Contexts E ::= ... | Eσ

Typing Rules are the same as those in the second order λc -calculus (λc 2-calculus).
Axioms: All the axioms in the λc -calculus where the evaluation contexts are extended
as above, and:(Λα.M ) σ = M [σ/α]Λα.M α = M(α ∈/ FTV (M ))Fig. 3. The λc 2η -calculus, extended from the λc -calculus

p : E −→ B is called a fibration if for any arrow u : J −→ I in B and object
X over I, there is an object u∗ X over J and an arrow ūX : u∗ X −→ X over uwhich is cartesian: for any object Z over K, arrow h : Z −→ X in E and arrowv : K −→ J in B s.t. ph = u ◦ v, there is unique arrow g : Z −→ u∗ X over v
satisfying h = ūX ◦ g.
For most of basic fibred category theory in the context of categorical semantics, we refer to [19]. In the present paper we use fibred-category-theoretical
notions only with a fixed base category. FibB is the 2-category of all fibrations,fibred functors and fibred natural transformations over a fixed base category B.
A fibred monad (over B) is an internal monad in the 2-category FibB [33].
For a fibred monad T , we can construct the Kleisli adjunction U ` F : p −→ pT
in FibB (cf. [17]). For a fibration (p, ⊗, I, α, λ, ρ) with fibred products, for which
we use the tensor notation, a strong fibred monad (T, η, µ, τ ) over p is a fibred
monad (T, η, µ) and fibred natural transformation τ : ⊗ ◦ (p × T ) =⇒ T ◦ ⊗satisfying
the¡¡¢¢ four equations: λ ∗ T = (T ∗ λ) ◦ (τ ∗ hCI , pi), (τ ∗ (⊗ × p)) ◦α ∗ p2 × T = (T ∗ α) ◦ (τ ∗ (p × ⊗)) ◦ (⊗ ∗ τ ), η ∗ ⊗ = τ ◦ (⊗ ∗ (p × η)),τ ◦ (p × µ) = (µ ∗ ⊗) ◦ (T ∗ τ ) ◦ (τ ∗ (p × T )), where CI := I ◦ ! : p −→ 1 −→ p
is the constant fibred functor of I.

64

Categorical Semantics for Second Order Computational
Lambda Calculi

In this section, we give categorical semantics for the λc 2-calculus and the λc 2η calculus. As mentioned in the introduction, we use monadic style semantics
rather than direct style semantics for call-by-value. They are equivalent [10],since we include into the definitions below the equalizing requirement, whichasks each component ηA of the unit of a monad T is an equalizer of T ηA andη TA .
First we define a “λc -version of polymorphic fibration”, which models theλc -calculus and type variables, but does not model universal types.
Definition 1 A polymorphic λc -model consists of(i) a cartesian polymorphic fibration, i.e. a fibration p : E −→ B which has
products in the base category, generic object Ω and fibred products,(ii) a fibred strong monad T on p satisfying the equalizing requirement fiberwise,and(iii) fibred Kleisli exponentials, i.e., a family of right adjoint functors X( (−)
(−)×X

F

I
to the composite functors FI ((−) × X) : EI −→ EI −→(ET )I where I isan object in B and X is over I in p, and which satisfies the Beck-Chevalley
condition:
for any u : J −→ I in B and X over I in p, the natural transformation fromu∗ ◦ (X( (−)) to (u∗ X( (−)) ◦ u∗ T induced by the natural isomorphismfrom FJ ((−) × u∗ X) ◦ u∗ to u∗ T ◦ FI ((−) × X) is isomorphic.
¤

If we have the first and the second item in the above definition, and if the
fibration is a fibred CCC, then we get the third item of polymorphic λc -model
for free by composition of the Kleisli adjunction and the adjunction defining
cartesian closedness. All the examples in the present paper are such models.
In the following, we use Ω for a generic object of a fibration, if it exists andthere is no ambiguity.
Definition 2 Let p be a polymorphic λc -model. By change-of-base of the Kleisli
embedding F : p −→ pT along (−) × Ω : B −→ B, we have a fibred functor
F Ω : pΩ −→ pT Ω . In addition, the reindexing functors induced by the projections∗
give a “weakening” fibred functor π(−),Ω: p −→ pΩ . Then,– Kleisli simple Ω-products is a fibred right adjoint functor to the compositeof these two fibred functors, and– a λc 2-model is a polymorphic λc -model p which has Kleisli simple Ω-products.¤
As the case of fibred Kleisli exponentials for a fibred CCC, if we have apolymorphic λc -model p which has simple Ω-products, then we obtain Kleisli
simple Ω-products in a quite similar way, and hence a λc 2-model for free. So any
λ2-fibration [19] which has the second item in Definition 1 forms a λc 2-model.
Definition 3 A λc 2η -model is a polymorphic λc -model p whose Kleisli fibrationpT has simple Ω-products.
¤

7

It is easily seen that all λc 2η -models are λc 2-models.
An interpretation of the λc 2η -calculus in a λc 2η -model is defined by inductions on type formation and on typing rules. This can be done in a quite similar
way to that of λc -calculus [25], with referring to that of System F [19], too.
Q On the type abstraction rule, [[Ξ | Γ ` Λα.M : ∀α.σ]] : [[Γ ]] −→ [[∀α.σ]] :=[[σ]] in (pT )[[Ξ]] is defined as the transposition of the composite [[Ξ, α | Γ ` M :σ]] ◦ (“canonical isomorphism”) : π ∗ [[Γ ]] ∼= [[Γ ]] −→ [[σ]] in (pT )[[Ξ,α]] = (pT )[[Ξ]]×Ω
under simple Ω-products adjointness.
On the type application
rule, first we have an arrow [[Ξ | Γ ` M : ∀α.σ]] :Q[[Γ ]] −→ [[∀α.σ]] := [[σ]] in (pT )[[Ξ]] with its transposition m : π ∗ [[Γ ]] −→ [[σ]] in]](pT )[[Ξ]]×Ω , and also have an arrow [[τ ]] : [[Ξ]] −→ Ω in B, where (−) is the correspondence induced by the generic object. Then [[Ξ | Γ ` DM τ : σ [τ /α]E∗]] : [[Γ ]] −→]∼ id[[Ξ]] , [[τ ]] π ∗ [[Γ ]] −→[[σ [τ /α] ]] in (pT )[[Ξ]] is defined as the composite [[Γ ]] =D
E∗]
id[[Ξ]] , [[τ ]] [[σ]] ∼= [[σ [τ /α] ]], where the last isomorphism is the canonical isomorphism from a semantic type substitution
lemma
D
E proved routinely, and the]
middle arrow is the reindexing of m by id[[Ξ]] , [[τ ]] .
Theorem 4 The class of all λc 2η -models are sound and complete for the λc 2η calculus with respect to the above interpretation.
¤
Proof. Soundness follows routinely by induction. For completeness, a term model
can be constructed in the same way as those for System F [19] and for the λc calculus [10].
¥Now we shall introduce a subclass of the class of λc 2η -models. All concretemodels we give in the present paper belong to this class.
Definition 5 A monadic λc 2η -model is a polymorphic λc -model such that p
and pT has simple Ω-products and the Kleisli embedding F : p −→ pT preservesthem.
¤
The notion of monadic λc 2η -models is natural for monadic style translation. The preservation of simple Ω-products by the identity-on-objects functor
F means that we use the same universal types before and after the monadic styletranslation. If we are interested in extensional universal types only for call-byvalue languages themselves, then we should expand the semantics to the class of
λc 2η -models. However, if we are also interested in monadic metalanguages, thenit is very simple and hence important to use the same universal types between
the value (non-effect) language (base category of a monad) and various effectfullanguages (Kleisli categories), since in a monadic metalanguage we may use morethan one monad, as we do so in Haskell.
Proposition 6 Let p be a polymorphic λc -model such that p has simple Ωproducts.
(1) If pT has simple Ω-products, then the fibred right adjoint functor U : pT −→p preserves simple Ω-products.

8(2) p is a monadic λc 2η -model, (i.e., pT has simple Ω-products and the fibred
functor F : p −→ pT preserves simple Ω-products,) if and only if the underlying fibred endofunctor T of the monad preserves simple Ω-products.
¤
By this proposition, it turns out that, in order to find a monadic λc 2η -model,
we only have to pay attention to the underlying endofunctor of aQmonad, without
Q
considering η nor µ. This is because the canonical arrow T ( A) −→TA
respects η and µ, since the reindexings preserve them. This simplification is very
useful as we use in the next section.

5

Concrete Models

In this section, we start to study concrete monadic λc 2η -models.
In order to obtain monadic λc 2η -models, we use Proposition 6 (2). For a λ2fibration and a fibred strong monad on it satisfying the equalizing requirement, if
the underlying
Q
Qfibred endofunctor of the monad preserves simple Ω-products, i.e.,
if T ( A) ∼= T A holds, then they form a monadic λc 2η -model. So we analyze
what kind of fibred functors preserve simple Ω-products in λ2-fibrations.
5.1

The Class of Monads

We describe here the class of monads considered in the present paper. For thesake of simplicity, we concentrate on the underlying endofunctors of monads.
First let us consider the following class of functors. In order to consider initial
algebras and final coalgebras, we consider multi-ary functors as well as unary
endofunctors.
T ::= γ | C | 1 | T × T | T + T | T C | µγ.T | νγ.T
This class is constructed inductively by projections, (i.e., variables γ,) constantfunctors, finite products, binary coproducts, powers, (i.e., exponentials whose
domains are constants,) initial algebras, and final coalgebras. Basically we would
like to consider something like the above class, but there is a problem.
All we need to show is that the underlying fibred endofunctors of fibred
monads preserve simple Ω-products, so it is sufficient to prove that the constructions defining inductively the above class (in the fibred setting) preserve
simple Ω-products. However, it is shown in Section 6.1 that coproducts do notnecessarily commute with universal quantifier in System F even with parametricity, and so we need some special morphism in a λ2-fibration considered here. In
the paper, we use models having fixed-point operators to resolve it. So, in order to avoid well-known conflict between fixed-point operators and coproducts,
we consider linear (more precisely, relevant) models by which we can relax relational parametricity inducing coproducts as in [28,5], and replace coproductswith separated sums and initial algebras with linearly initial algebras. Linearly
initial algebras are, roughly, something which are initial algebras only in a linear model. These notions of separated sums and linearly initial algebras will be
explained in Section 6.3 and 6.4 respectively.

9

Now let us describe the class of monads considered in the present paper. It isthe class of all fibred monads whose underlying fibred endofunctors are includedin the following class (1).
T ::= γ | 1 | T × T | T C | νγ.T | C | T ⊕T | µ◦ γ.T(1)

In the above, ⊕ is separated sum, and µ◦ γ.T is linearly initial algebras. These
constructions form fibred functors, see Sections 5.2, 6.3, and 6.4 for final coalgebras, separated sums, and linearly initial algebras respectively.
From now on we show that simple Ω-products are preserved by (i): products,
powers, final coalgebras, (ii): constant fibred functors, (iii): separated sums, andlinearly initial algebras.
On the constructions of (i), we can show that they preserve simple Ω-productsby their categorical universal property, because they are right adjoint as wellas simple Ω-products. For constants of (ii), however, we need more property
like parametricity, and for separated sums and linearly initial algebras of (iii),
we need additionally more structures like fixed-point operators. We consider
products, powers, final coalgebras in the next subsection, constants are treatedin the next, and separated sums and linearly initial algebras are postponed to
the next section.
In the paper, we do not mind whether such constructions as above are available or not, and do only show that they preserve simple Ω-products if they exist.
If we try to show existence of e.g. parameterized initial algebras for multi-aryfunctor, to treat the list monad and input monads, then we need to introduce
the notion of “fibrations and fibred functors enriched over a monoidal fibration”,
and perhaps need to use fibrations with indeterminates [17]. For space reason we
postpone such detailed work elsewhere, which is less problematic because the existence of the constructions represented in syntax is well known by polymorphic
encoding with parametricity.
5.2

Products, Powers and Final Coalgebras

Here, we investigate constructions which preserve simple Ω-products by only
universal property.
Lemma 7 Let B be a cartesian category, and K be any object of B.
(1) The subcategory of FibB consisting of all fibrations having simple K-products,
and all fibred functors preserving simple K-products, is cartesian subcategory.
(2) Let p be a fibration having simple K-products and fibred finite products.
Then the fibred functors × : p × p −→ p, and 1 : 1 −→ p preserve simple
K-products.
(3) Moreover assume that p is a fibred CCC. Then for any X over 1 in p, the“power” fibred functor X⇒ (−) : p −→ p preserves simple K-products. ¤10We can also add final coalgebras into the above list, if they exist sufficiently
in the sense described below. The same things hold from here to Definition 8 forboth initial algebras and final coalgebras in the dual way, so we do with initial
algebras, since more examples of effects use initial algebras.
Let p, q be fibrations with the same base category B, and F : q × p −→ p be afibred functor. We say that F : q × p −→ p has initial algebras with parameters,
if for any X over I in q, the endofunctor F (X, −) : EI −→ EI has initial algebra(µF X, αX : F (X, µF X) −→ µF X), and if the reindexings preserve them, i.e.,
for any X over I in q and any arrow u : J −→ I in B, the unique algebra
map from the initial algebra µF (u∗ X) to the algebra F (u∗ X, u∗ (µF X)) ∼=u∗ αu∗ F (X, µF X) −→X u∗ (µF X) is isomorphism.
If F is in the case, then the assignment which maps an object X over I in q
to the object µF X over I in p extends to the unique fibred functor µF : q −→ psuch that the family of maps (αX : F (X, µF X) −→ µF X)X forms into a fibred
natural transformation from F (−, µF −) to µF .
Definition 8 For a fibred functor F : q × p −→ p having initial algebras withparameters, there is the initial algebras fibred functor µF : q −→ p as above.
Similarly, if F : q × p −→ p has final coalgebras with parameters, which isdefined in the dual way, then we have the final coalgebras fibred functor νF :q −→ p with the fibred natural transformation from νF to F (−, νF −).
¤Lemma 9 Let B be a cartesian category, K be an object of B, p, q be fibrations
having simple K-products, and F : q × p −→ p be a fibred functor having final
coalgebras with parameters. Then, if F preserves simple K-products, the fibred
functor νF : q −→ p also preserves simple K-products.
¤
Typical usage of the above is to get endofunctors with q = p (or pn ), but wewill use a coKleisli fibration for q with linear models in Section 6.4.

5.3

Constant

In this short subsection, the construction using constants is added.
For a λ2-fibration p and any object X over 1, the fibred functor X : 1 −→ ppreserves simple Ω-products if p satisfies suitable parametricity, including relational parametricity, linear parametricity, and focal parametricity.
In this case of constants we do not need additional arrows differently fromthe case in the next section, because we can adopt the (unique)projection asQ
the inverse arrow of the canonical (diagonal) arrow X −→ X.
SAt this point, we can add global state monads ((−) × S) and output monadsµ β. (−) + (U × β) ∼= (−) × (µ◦ β.1 + (U × β)) to the class of monads which form
monadic λc 2η -models.
◦

11

6

Separated Sums and Linearly Initial Algebras

We continue to show how we construct monads compatible with extensional
universal types. In this section we consider separated sums and linearly initial
algebras. For space reason, we give only a sketch.
6.1

Basic Ideas

First we describe basic ideas used in later, and also why we use separated sums
and linearly initial algebras instead of coproducts and initial algebras. Contrary
to the case of constants, for coproducts and initial algebras we have to use more
limited class of models with additional arrows. First let us see the reason forcoproducts in a syntactic way.
Naively thinking, to get the desired term of the type ∀α. (σ + τ ) → ∀α.σ +∀α.τ , we can think of a term likeλu: ∀α. (σ + τ ) . case u1 of
(2)
¡
¢
0
in0 a → in0 Λα.case uα of (in0 a → a) | (in1 b → “this case nothing”)¡¢|in1 b0 → in1 Λα.case uα of (in0 a → “this case nothing”) | (in1 b → b)
where “this case nothing”’s mean that the cases of the coproducts are not realized, if we assume parametricity. In fact, we can prove in the Plotkin-Abadi
logic that, for any term u of a type ∀α. (σ + τ ), every type instantiation of u has
the same index of the coproduct.
However, this is just a reasoning in logic, and there is no assurance to beable to construct such terms as “this case nothing”. In fact, there is no term of
the type ∀α. (σ + τ ) → ∀α.σ + ∀α.τ in System F for certain σ and τ : for thecase when σ is α and τ is α→0, the type ∀α. (α + (α→0)) → ∀α.α + ∀α. (α→0)
in System F corresponds to the proposition ∀α. (α ∨ ¬α) ⇒ ∀α.α ∨ ∀α.¬α insecond order intuitionistic logic, and the inhabitation contradicts the soundnessof second order classical logic. So we have to add more terms to realize the above“this case nothing”.
To solve this problem, we use non-termination effects, with which we canreplace “this case nothing”’s with bottoms.
In the next place, let us think about initial algebras. For e.g. the list monad,
we may think a desired term f of the type ∀α.µβ.1 + σ × β −→ µβ.1 + (∀α.σ) × β
as the following.
let f = λu: (∀α.µβ.1+σ×β) . case u1 of Nil → Nil | Cons(a0 , as0 ) →¡Cons Λα.case uα of (Nil → “this case nothing”) | (Cons(a, as) → a)¡¢¢
, f Λα.case uα of (Nil → “this case nothing”) | (Cons(a, as) → as)
The two “this case nothing”’s are the same as that in the case of coproducts, andthis is just because we use coproducts in the definition of lists. The essential hereis the occurrence of f in the definition of f . This is not induction which follows
from the universality of initial algebras, but recursion by fixed-point operators.

12

For fixed-point operators, we employ separated sums and linearly initial algebras instead of coproducts and initial algebras respectively. These cause no
problem to construct monads, as we use these in Haskell in fact, because these
also have universal property, though limited into a linear model. In the following
subsections, we show that separated sums and linearly initial algebras preserve
simple Ω-products in relevant parametric models with fixed-point operators.
6.2

Linear Parametric Models

From now on, we consider domain theoretic models. Let us begin with describing
what kind of models we use.
We consider a PILLY model [6] l having fibred products. PILLY models are
λ2-version of linear categories which can also model fixed-point operators, seeloc. cit. for details. The requirement on fibred products is not strong at all, since
they can be obtained for free if we assume linear parametricity [5], and in fact weassume a bit stronger one, i.e., relevant parametricity in the next subsection. For
the linear exponential fibred comonad ! on l, let U : l −→←− p : L be its coKleisli
fibred adjunction, where U is the right, so fiberwise identity-on-objects.
Then p is a λ2-fibration: It is well-known that the coKleisli category of alinear model with cartesian products is a CCC, see e.g. [3]. A generic object isshared with l, since U is fiberwise identity-on-objects and the base is shared.
Simple Ω-products are for free like fibred products.
We take this λ2-fibration p as the base fibration of monadic λc 2η -models.
Then, the fibred monads T on p studied below are what we described in Section
5.1.
Since U is a fibred right adjoint functor, it preserves simple Ω-products,
which follow from just the universal property, and irrelevant to the fact that Ω
is a generic object or that U preserves it.
On the other hand, we do assume that the left fibred adjoint functor L preserves simple Ω-products. The reason for assuming this is to show the compatibility of separated sums and of linearly initial algebras with simple Ω-products.
Thanks to this assumption, we can add the non-termination lifting monad to theclass of monads compatible with simple Ω-products, but this is just a (welcome)secondary product. This is a reasonable assumption, since lifting monads usually preserve simple Ω-products in a parametric setting, as opposed to powerset
monads.
6.3

Relevant Parametricity for Separated Sum

The use of fixed-point operators involves two matters, i.e., we have to use separated sums instead of coproducts in p, and have to use linear parametricity.
In fact, the use of separated sums is less problematic. Assuming linear parametricity, there are fibred coproducts in l, so we have also fibred separated sums
⊕ in p as U ◦ (+) ◦ L2 . Here, (+) ◦ L2 has the same kind of universal property
as Kleisli exponentials, and by this we can construct familiar monads like e.g.

13

exception monads, the list monad, and input monads. When we use separated
sums for exception monads, it can be viewed also in terms of linearly used effects[13].
Now we show that these separated sums commute with simple Ω-products.
We basically use the idea of the above term (2). After replacing “this case nothing”’s with bottoms, still there remain two problems. The first is, in (2), we use
weakening rules for a0 and b0 , and the second is the use of a contraction rule forthe two u’s in u1 and uα. (The two uα’s are essentially the same, since this isfrom the distributivity of monoidal products over coproducts in l.)
The problem of weakening is resolved as the following. To proveQ◦ that separated
sums
preserve
simpleΩ-products,
itsufficesto
prove(!A+!B) ∼
=
Q◦
Q◦
Q◦
!A+
!B in l, whereis simple Ω-products in l. This is because, we can
Q
Q◦
Q◦
def Q
∼
then ¡show
thatQ (A⊕B)= Q U (LA+LB)=U(!A+!B)= U Q (LA+LB)
¢
Q
Q
Q
◦
◦
∼
!A+
!B ∼
=U
= U (L U A+L U B) = A⊕ B, noting that U and
L preserve simple Ω-products, and U is identity-on-objects. So, we can use weakening rules by virtue of these two !’s.
On the other hand, to use a contraction rule, we need to strengthen a typetheory to allow contraction, i.e., to the “relevant” one. Fortunately, lifting monads are usually relevant monads as in [18]. Relevant lambda calculi are extensionof linear lambda calculi with contraction term formation rules. Then relevant
Plotkin-Abadi Logic is simply linear Plotkin-Abadi logic [5] on top of such thesecond order relevant lambda calculus. As a result of this extension of the classof linear terms, the class of admissible relations is also extended, for instance we
can use graph relations of such “relevant terms”.
Finally, we need one more rule for forming admissible relations: for an admissible relation ρ between σ and τ , and a term hf, gi : σ 0 × τ 0 ( σ × τ of linear
function type, the “inverse-image” relation (x : σ 0 , y : τ 0 ) .ρ (f hx, yi , g hx, yi) is
also an admissible relation between σ 0 and τ 0 . This is modeled with the intuition
that admissible relations between σ and τ are subalgebras of the product of σand τ . This rule is usedQ◦beQ◦ in the parametric reasoning to prove theQequality◦!B!A+(!A+!B)andthecompositetermthrough
tween the identity on
Q◦
Q◦
Q◦
!B.
!A+
(!A+!B) ∼involving the isomorphism=
We introduce some of models (l, p, ...) for such relevant parametricity which
satisfy the assumptions thus far: the models (PFam (AP (D)⊥ ), PFam (AP (D)),...) of linear Plotkin-Abadi logic constructed from domain theoretic PERs, which
is described in [8]. Hence,
Proposition 10 The separated sums in PFam (AP (D)) preserve simple Ω-products.¤
6.4

Linearly Initial Algebras

In this last subsection, we consider about linearly initial algebras.
Once we determine to use fixed-point operators, there is an easier way thanconsidering of such a complicate term as in Section 6.1. That is, we can use
the fact that if both initial algebras and final coalgebras exist for sufficiently
many endofunctors, then the initial algebras and final coalgebras are canonically14isomorphic for such endofunctors if and only if fixed-point operators exists [9,5].
Then Lemma 9 is applicable.
All the remaining matter is that we have to use linearly initial algebras
instead of initial algebras. Now let q be a fibration which has the same basecategory and generic object Ω as those of l and p, and has simple Ω-products.
Then for a fibred functor F : q × p −→ p preserving simple Ω-products, thecomposite fibred functor F 0 := L ◦ F ◦ (q × U ) : q × l −→ q × p −→ p −→ l alsopreserves simple Ω-products.
Now if F 0 has initial algebras with parameters and also final coalgebras withparameters in the sense of Section 5.2, then the µF 0 and νF 0 are naturally
isomorphic thanks to the fixed-point operators as mentioned above. So by Lemma
9, µF 0 preserves simple Ω-products. Hence the linearly initial algebras fibred
functor U ◦ µF 0 : q −→ l −→ p also preserves simple Ω-products.
n+1

Proposition 11 Let F : PFam (AP (D))−→ PFam (AP (D)) be a fibred
functor such that F 0 defined as above has initial algebras with parameters andfinal coalgebras with parameters. If F preserves simple Ω-products, then the linn
early initial algebras fibred functor U ◦ µF 0 : PFam (AP (D)) −→ PFam (AP (D))
also preserves simple Ω-products.
¤
Theorem 12 Let T be a fibred strong monad on PFam (AP (D)) satisfying theequalizing requirement. If the underlying fibred endofunctor of T is included in
the class (1) in Section 5.1, then T and the λ2-fibration PFam (AP (D)) form amonadic λc 2η -model.
¤

7

Concluding Remark

We have given the second order computational λ-calculus with extensional universal types, which is a call-by-value lambda calculus with universal types satisfying η-equality. Then we have formulated its sound and complete categoricalsemantics, and also reasonable characterization in terms of monadic metalanguages. Finally, we have seen concrete domain theoretic models, in a somewhat
general way with relevant parametricity. Such models can accommodate manyfamiliar effects constructed polynomially to extensional universal types.
In Section 6, we have taken the domain theoretic approach. On the other
hand, we can also take a dependent type theoretic approach, by which we can
avoid “this case nothing” in the term (2) in Section 6, using strong coproducts.
Moreover, by inductive initial algebras in the sense of [19], we can deal withsome kinds of initial algebras including the list monad and input monads. In
this way, we can see that the typical models for parametricity constructed fromrecursion theoretic PERs (see e.g. loc. cit.) also have a similar class of monads
which form λc 2η -models. These will be treated in a separate paper.
It is interesting to clarify whether we can include powerset monads and/or
continuations monads into the class of models, and whether all lifting monads
commute with parametric simple Ω-products.
Also, it is an interesting challenge to investigate principles of parametricpolymorphism in the two call-by-value calculi in the paper.

15

Acknowledgements
I would like to thank Masahito Hasegawa for many helpful discussions and comments on earlier drafts. I am also grateful to Shin-ya Katsumata, Ichiro Hasuo,
and Naohiko Hoshino for useful comments and discussions. Also I thank anonymous reviewers for helpful comments.

References
1. Martı́n Abadi, Luca Cardelli, and Pierre-Louis Curien. Formal parametric polymorphism. TCS: Theoretical Computer Science, 121, 1993.
2. Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In Gilles
Barthe, Peter Dybjer, Luı́s Pinto, and João Saraiva, editors, Advanced Lecturesfrom Int. Summer School on Applied Semantics, APPSEM 2000 (Caminha, Portugal, 9–15 Sept. 2000), volume 2395 of Lecture Notes in Computer Science, pages
42–122. Springer-Verlag, Berlin, 2002.
3. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models(extended abstract). In CSL, pages 121–135, 1994.
4. Gavin M. Bierman, Andrew M. Pitts, and Claudio V. Russo. Operational properties of lily, a polymorphic linear lambda calculus with recursion. Electr. Notes
Theor. Comput. Sci., 41(3), 2000.
5. Lars Birkedal, Rasmus E. Møgelberg, and Rasmus L. Petersen. Linear Abadi &Plotkin logic. Logical Methods in Computer Science, 2(5), November 2006.
6. Lars Birkedal, Rasmus E. Møgelberg, and Rasmus L. Petersen. Category-theoretic
models of linear Abadi and Plotkin logic. Theory and Applications of Categories,
20(7):116–151, 2008.
7. Lars Birkedal and Rasmus Ejlers Møgelberg. Categorical models for Abadi and
Plotkin’s logic for parametricity. Mathematical Structures in Computer Science,15(4):709–772, 2005.
8. Lars Birkedal, Rasmus Ejlers Møgelberg, and Rasmus Lerchedahl Petersen.
Domain-theoretical models of parametric polymorphism. Theor. Comput. Sci,
388(1-3):152–172, 2007.
9. Peter Freyd. Recursive types reduced to inductive types. In John Mitchell, editor,
Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, LICS
1990, pages 498–507. IEEE Computer Society Press, June 1990.
10. Carsten Führmann. Direct models of the computational lambda calculus. Electr.
Notes Theor. Comput. Sci, 20, 1999.
11. Jean-Yves Girard. Interpretation fonctionelle et elimination des coupures del’arithmetique d’ordre superieur. These D’Etat, Universite Paris VII, 1972.
12. Robert Harper and Mark Lillibridge. Operational interpretations of an extensionof Fω with control operators. J. Funct. Program., 6(3):393–417, 1996.
13. Masahito Hasegawa. Linearly used effects: Monadic and cps transformations into
the linear lambda calculus. In Zhenjiang Hu and Mario Rodrı́guez-Artalejo, editors, FLOPS, volume 2441 of Lecture Notes in Computer Science, pages 167–182.
Springer, 2002.
14. Masahito Hasegawa. Relational parametricity and control. Logical Methods in
Computer Science, 2(3), 2006.
15. Masahito Hasegawa and Yoshihiko Kakutani. Axioms for recursion in call-by-value.
Higher-Order and Symbolic Computation, 15(2-3):235–264, 2002.

16
16. Ryu Hasegawa. Categorical data types in parametric polymorphism. Mathematical
Structures in Computer Science, 4(1):71–109, 1994.
17. Claudio Alberto Hermida. Fibrations, Logical Predicates and Indeterminates. PhD
thesis, University of Edinburgh, 1993.
18. Bart Jacobs. Semantics of weakening and contraction. Ann. Pure Appl. Logic,
69(1):73–106, 1994.
19. Bart Jacobs. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. Elsevier, 1999.
20. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004.
21. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments incall-by-value programming languages. INFCTRL: Information and Computation(formerly Information and Control), 185, 2003.
22. Rasmus Ejlers Møgelberg. Interpreting polymorphic fpc into domain theoretic
models of parametric polymorphism. In Michele Bugliesi, Bart Preneel, Vladimiro
Sassone, and Ingo Wegener, editors, ICALP (2), volume 4052 of Lecture Notes in
Computer Science, pages 372–383. Springer, 2006.
23. Rasmus Ejlers Møgelberg and Alex Simpson. Relational parametricity for computational effects. In LICS, pages 346–355. IEEE Computer Society, 2007.
24. Rasmus Ejlers Møgelberg and Alex Simpson. Relational parametricity for control
considered as a computational effect. Electr. Notes Theor. Comput. Sci., 173:295–
312, 2007.
25. Eugenio Moggi. Computational lambda-calculus and monads. Technical Report
ECS-LFCS-88-66, Laboratory for Foundations of Computer Science, University of
Edinburgh, 1988.
26. Eugenio Moggi. Computational lambda-calculus and monads. In LICS, pages
14–23. IEEE Computer Society, 1989.
27. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991.
28. Gordon D. Plotkin. Type theory and recursion (extended abstract). In LICS, page374. IEEE Computer Society, 1993.
29. Gordon D. Plotkin and Martı́n Abadi. A logic for parametric polymorphism. In
Marc Bezem and Jan Friso Groote, editors, TLCA, volume 664 of Lecture Notes
in Computer Science, pages 361–375. Springer, 1993.
30. John C. Reynolds. Towards a theory of type structure. In Bernard Robinet, editor,
Symposium on Programming, volume 19 of Lecture Notes in Computer Science,
pages 408–423. Springer, 1974.
31. John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP
Congress, pages 513–523, 1983.
32. Alex K. Simpson and Gordon D. Plotkin. Complete axioms for categorical fixedpoint operators. In LICS, pages 30–41, 2000.
33. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra,
2:149–168, 1972.
34. Philip Wadler. Theorems for free! In Functional Programming Languages andComputer Architecture. Springer Verlag, 1989.

Erratum
In Section 4 we defined two kinds of categorical models called λc 2η -models andmonadic λc 2η -models, where the latter is stronger notion than the former; andin Theorem 4 we stated that the λc 2η -calculs is sound and complete for the
λc 2η -models. It turns out that this does not hold, and instead we have to assume
monadic λc 2η -models rather than λc 2η -models; this is necessary in the sense thatthe calculus is also complete for the monadic λc 2η -models, as the term model
becomes a monadic λc 2η -model. Thus a correct theorem instead of Theorem 4
is:Theorem The λc 2η -calculus is sound and complete with respect to the monadic
λc 2η -models.

What is overlooked in a proof of the soundness is the lemma that, for any
value V , its interpretation [[V ]] is a value (i.e., in the image of the Kleisli embedding); its proof itself is straightforward by induction on V (once we assume
monadic λc 2η -models).
All the parts except for Theorem 4 in the paper are correct—where first of
all we do not use the notion of λc 2η -models (but use the stronger notion ofmonadic λc 2η -models)—, especially including Sections 5 and 6 on constructionof concrete monadic λc 2η -models.
Remark Once we apply the above erratum, we use only the notion of monadic
λc 2η -models and do not use that of λc 2η -models at all; then it seems better to
use the terminology λc 2η -models for the notion of monadic λc 2η -models, (though
in this erratum we always use the terminology in the original paper to avoid
confusion).
