[Prev][Next][Index][Thread]

Extending Reynolds

		   AN EXTENSION OF REYNOLDS' RESULT
	  ON THE NON-EXISTENCE OF SET-MODELS OF POLYMORPHISM

			   Andrew M. Pitts
	     Mathematics Division, University of Sussex,
		      Brighton  BN1 9QH, England

		       andyp@cvaxa.sussex.ac.uk


Recall that Reynolds [Re] proved that there is no model of the
polymorphic typed lambda calculus in which types denote sets and the
function type (X->Y) denotes the set of all functions from X to Y.
Soon afterwards Plotkin generalized and clarified Reynolds' method of
proof, resulting in the joint paper [RP]. Reading that paper recently,
I realized that there is a simple but very pleasing extension of
Reynolds and Plotkin's results, and one that shows (maybe
surprisingly, in view of the results in [Pi]) that Reynolds'
non-existence result has nothing to do with the non-constructive
nature of set theory and everything to do with the fact that the
category of sets is cartesian closed and has a subobject classifier
(i.e. is an elementary topos). Let me explain...

Firstly, we consider models P of the polymorphic typed lambda calculus
as in [RP]. Part of the information specifying P is a cartesian closed
category (ccc) whose objects and arrows are used to denote the closed
types and terms of the calculus; I will denote this ccc by P(0).

(REMARK. Reynolds and Plotkin consider a weak notion of model, just
sufficient for their needs; that will do for us too, but my notation
is geared towards the categorical notion of model considered in [Se]
and [Pi] (and elsewhere)---where for each natural number there are
ccc's P(n) for denoting types and terms with at most n free type
variables, and functors connecting these ccc's to deal with
substitution and polymorphic product formation: see [Pi, Definition
2.2].)

Reynolds [Re] showed that there is no model P with P(0)=SET, the
category of sets and functions. SET is a (very special) example of a
topos, i.e. a ccc with a subobject classifier---see [LS, II.3].
(Toposes are the categories which model theories in constructive
higher order predicate logic---a kind of construcive set theory: see
[LS, PartII].) We cannot have P(0)=Set, but perhaps P(0) can still be
a topos? The answer is "no":

THEOREM. There is no non-degenerate model P of the polymorphic typed
lambda calculus with P(0) a topos.

(By definition, P is degenerate if P(0) is degenerate, i.e. is
equivalent to the one-object-one-arrow category. In the case that P is
actually one of the categorical models mentioned above, the degeneracy
of P(0) in fact implies the degeneracy of all the other ccc's P(n).)

Slightly more generally:

PROPOSITION. Let P be a model of the polymorphic typed lambda
calculus, and let I:P(0)--->E be a fully faithful functor from P(0)
into a topos E whose image is closed in E under taking finite limits
and exponentials. (This implies in particular that the ccc P(0) has
equalizers of all parallel pairs of arrows.) Then the subobject
classifier of the topos E is a subobject of an object in the image of
I only in the case that E (and hence also P) is degenerate.

(The theorem follows immediately from the proposition by taking E=P(0)
and I equal to the identity functor.)

This proposition should be contrasted with the results in [Pi], which
show that (categorical) models of the polymorphic typed lambda
calculus can always be fully embedded in toposes at the same time
preserving all the structure involved. The proposition shows that in
the case that P(0) has equalizers (which is certainly a very special
assumption), such full embeddings will sit the polymorphic types "well
away" from the type of propositions (the subobject classifier), in the
sense that the latter can't be a subtype of any of the former, except
in the degenerate case.

I will now sketch the proof of the proposition, building upon the
methods of [RP]:

Firstly, there is Plotkin's key observation [RP, Proposition 3] that
if a functor T:P(0)--->P(0) is expressible in the model P (i.e.
definable by expressions in the polymorphic lambda calculus), then
there is a weakly initial T-algebra, i.e. there is w:T(W)--->W with
the property that for any other a:T(A)--->A, there is some (not
necessarily unique) f:W--->A with

			     T(f);a = w;f .

It is important to note that one can allow T to be definable by
polymorphic expressions over some language with type and individual
constants. (I.e. we don't have to limit ourselves to definability in
the pure calculus.) In particular if B is an object in P(0), then 

			   T( )=(( )->B)->B

is definable by expressions in the polymorphic lambda calculus over
the language with a single type constant standing for B; so we can
apply the observation to this functor and conclude that it has a weak
initial algebra.

Secondly, we need a way of manufacturing an actually initial T-algebra
>from a weakly initial one, w:T(W)--->W. In [RP] the method at the
heart of the Adjoint Functor Theorems is used: take the joint
equalizer of all the T-algebra endomorphisms of W and show that the
resulting T-algebra is initial. This is fine if P(0) has equalizers of
all sets of parallel arrows (as it does if we are assuming P(0)=SET);
but the hypotheses of the proposition only provide us with equalizers
of parallel pairs. The resolution of this problem is to internalize
the argument, using the fact that T is defined "internally" (the
precise requirement on T is given below). Specifically, the following
technical lemma is the key result we need:

LEMMA. Let C be a ccc with equalizers of all parallel pairs of arrows
and suppose that T:C--->C is a C-enriched functor. (See below for a
definition of being enriched). Then an initial T-algebra exists if a
weakly initial one does.

(DEFINITION. T is C-enriched if for all objects A and B in C, there
are arrows
		       tAB:(A->B)---->(TA->TB)

satisfying              tAA(id(A)) = id(TA)     for all A in C,
and		     tAB(f);tBC(g) = tAC(f;g)   for all f:A---->B and
                                                g:B---->C in C.)

This is a standard notion of "enriched" category theory (see [Ke]),
which is applicable here since C is a monoidal closed category via the
binary products and exponentials it possesses.)

Completing the proof of the proposition, we know from Reynolds and
Plotkin's results that for any B in P(0), T( )=(( )->B)->B has a weak
initial algebra; and since (( )->B)->B is always an enriched functor,
the lemma implies that it has an initial algebra, i:((I)->B)->B--->I,
say. As is well known, the structure morphism i is an isomorphism. Now
if B contains the subobject classifier as a subobject, we can carry
out a version of Cantor's diagonal argument in the internal logic of
the topos E to conclude that it is degenerate.

REMARK. In SET, the subobject classifier coincides with the coproduct,
1+1, of the terminal object with itself; but in a general topos these
two objects are very different. In particular, it is possible to have
((I)->1+1)->1+1 isomorphic to I for some I in a non-degenerate
topos---Hyland's effective topos [Hy, 3.1] furnishes an example.

REMARK. Note that the "modest sets" model of polymorphism [Hy] shows
that even though P(0) cannot have a subobject classifier, it can have
many of the properties which are consequences of being a topos (such
as being locally cartesian closed, having a natural number object and
being finitely cocomplete).


			      REFERENCES

[Hy] Hyland,J.M.E. "A small complete category". In: Proc. Conference
on Church's Thesis after 50 years, Ann. Pure Applied Logic, to appear.

[Ke] Kelly,G.M. "Basic Concepts of Enriched Category Theory", London
Mathematical Society Lecture Note Series No.64 (C.U.P., 1982).

[LS] Lambek,J. and Scott,P.J. "Introduction to Higher Order
Categorical Logic", Cambridge Studies in Advanced Mathematics 7
(C.U.P., 1986).

[Pi] Pitts,A.M.  "Polymorphism is set theoretic, constructively". In:
Pitt,D.H. et al (eds), "Category Theory and Computer Science", Lecture
Notes in Computer Science No.283 (Springer, Berlin, 1987), pp12--39.

[Re] Reynolds,J.C. "Polymorphism is not Set-Theoretic." In: Kahn,G.
et al (eds), "Semantics of Data Types", Lecture Notes in Computer
Science No.173 (Springer, Berlin, 1984), pp145--156.

[RP] Reynolds,J.C. and Plotkin,G.D. "On functors expressible in the
polymorphic typed lambda calculus". In: Huet,G. (ed.), "Logical
Foundations of Functional Programming" (Addison Wesley), to appear.

[Se] Seely,R.A.G. "Categorical semantics for higher order polymorphic
lambda calculus", Jour. Symbolic Logic 52(1987) 969--989.