Counterexamples of functors that do notpreserve parametric simple Ω-products
Kazuyuki Asada1Introduction

In [1], it is shown that all the polynomial functors—including (linearly-)initial
algebra and final coalgebra construction—in a suitable model of parametric polymorphic lambda calculus preserve simple Ω-products. (Simple Ω-products aresemantical counterparts of universal types ∀α.σ.) In this manuscript, we give
examples of functors that do not preserve simple Ω-products even in parametric setting. Especially, the continuation monad in Section 2 forms an exampleof models that are not models of λc 2η -calculus [1]. Below, see ibid. for relatednotions.

2Continuation MonadThe next example is given in a syntactic way (or, in term models).
Proposition 1 Let R be the type 1 + 1 in System F.
Then the canonical termfrom ((∀α.α → α + R) → R) → R
to∀α. ((α → α + R) → R) → Ris not an isomorphism (regardless of assuming parametricity).

Proof. Let c be the canonical term from((∀α.α → α + R) → R) → Rto∀α. ((α → α + R) → R) → R.
Suppose that there is a term c–1 such that c is isomorphic up to parametricity
with c–1 as the inverse. (Note that if c is isomorphic up-to-βη then trivially isisomorphic up to parametricity.) Then our aim is to show absurdity.
((∀α.α → α + R) → R) → R oOd ∼= d–1

((1 + R) → R) → Rc∼=?

/

∀α. ((α → α + R) → R) → R

c–1
(−)Rf


/ ((R → R + R) → R) → R

2

By usual parametric reasoning, ∀α.α → α + R is isomorphic to 1 + R, so
there is the canonical term d and d–1 as above, and they are isomorphic up toparametricity. Then let f be the composition ((−) R) ◦ c ◦ d.
Let 10 be the term
Λα.λk : ((α → α + R) → R) .k (λx0 : α.in1 (k (λx1 : α.in0 (x0 ))))in ∀α. ((α → α + R) → R) → R. (On the naming of “10 ”, note that we can define
the Church numeral of 1 in ((1 + R) → R) → R, and its image by c ◦ d is equal
to the term
Λα.λk : ((α → α + R) → R) .k (λx0 : α.in1 (k (λx1 : α.in0 (x1 ))))and not equal-up-to-parametricity to 10 ; the last fact follows from the remaining
part of the proof.)
Now f d–1 c–1 (10 ) is equal to 10 R up to parametricity; hence, 10 R is in
the image of f . (Here “in image” is up to equations under parametricity.) On
the other hand, in the types ((1 + R) → R) → R and ((R → R + R) → R) → R
16
there are only finite number (respectively 28 and 2(2 ) ) of closed terms up toparametricity, so the extensional equality in the types are decidable, and we cancompute—by programming—whether 10 R is in the image of f . Then the answer
becomes false, hence we could show contradiction.
As above, the proof is given using computation by computer; a direct proof
should be given.
Though the example in Section 3 comes from shortage of parametricity, theabove example is a counterexample even under full-parametricity.
The above example denies the isomorphism in the term model with parametricity, but does not directly deny the isomorphism in other models of System
F with parametricity. If we have some parametric models for which the isomorphism holds, it means that the logic of parametricity is not complete for suchthe models. Conversely thinking, if—as in the case of simply typed lambda calculus [2]—every “non-trivial” parametric model of System F forms a (singleton)class of models for which the logic of parametricity is complete, then the above
counterexample works also for all such non-trivial models.

3Tensor Products

Proposition 2 The fibred endofunctor (−) ⊗ (−) on PFam (AP (D)⊥ ) does notpreserve simple Ω-products.
Proof. We here represent a per by the set of equivalent classes. Note that if
the domains of considered pers are finite sets, then a relation, i.e., a regularsubobject of the product of such two pers is just a relation between such twosets of equivalent classes such that the bottom class must be related to thebottom class.

3

Let us define an object f = (f p , f r ) over the generic object 1 in PFam (AP (D)⊥ )as the following:f p(1) := {true, ⊥}, {false}
f p(R) := {true}, {⊥, false}(for R 6= 1)
def[d] f r(A) [e] ⇐⇒ ∃x ∈ {⊥, true, false}. x ∈ [d] ∧ x ∈ [e](for R, S ∈ |AP (D)⊥ |, and for regular subobject A  R × S in AP (D)⊥ ) .
QNow note that the fiber over 0—where f belongs—is nothing but AP (D)⊥(up-to-iso), and also that the per part of a tensor product is determined by only
the two per parts. ThenQf = {{⊥}, {true}, {false}},and soQQf⊗ f
= {h⊥, ⊥i , ...}, {htrue, truei}, {htrue, falsei}, {hfalse, truei}, {hfalse, falsei} .
On the other hand, it can be easily checked by definition thatQhtrue, falsei ( (f ⊗f )) h⊥, ⊥i andQhfalse, truei ( (f ⊗f )) h⊥, ⊥i ,henceQ(f ⊗f )= {{h⊥, ⊥i , htrue, falsei , hfalse, truei , ...}, {htrue, truei}, {hfalse, falsei}}.
QQ
QThus f ⊗ f and (f ⊗f ) are not isomorphic.
Note that the above counterexample comes from (probably inevitable) shortage of parametricity of PFam (AP (D)⊥ ) in the sense that a term of a universal
quantified type in PFam (AP (D)⊥ ) may be ⊥ or else dependently on type instantiation.

Acknowledgements
I would like to thank Masahito Hasegawa and Shin-ya Katsumata for conjecturing the counterexample on continuation monads.

References
1. Kazuyuki Asada. Extensional universal types for call-by-value. In G. Ramalingam,editor, Programming Languages and Systems, volume 5356 of Lecture Notes in Computer Science, pages 122–137. Springer Berlin Heidelberg, 2008.
2. Alex K. Simpson. Categorical completeness results for the simply-typed lambdacalculus. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, TypedLambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science,
pages 414–427. Springer Berlin Heidelberg, 1995.