FOM: Re: polymorphic type theory

[Till Mossakowski]

Steve Simpson wrote:

>Polymorphic type theory:
>
>Till Mossakowski called our attention to Pitts' work (LNCS 283, pages
>12-39) in which an appropriately chosen topos provides a semantics for
>polymorphic type theory.  That's a good point!  At the very least,
>it's an interesting connection between topos theory and polymorphic
>type theory.  I don't remember the details of Pitts' paper; I may have
>read it years ago.  Does Pitts actually refer to toposes or use any
>results of topos theory?  His title refers instead to "constructive
>set theory", so once again it appears that topos theory is slavishly
>imitating set theory.

Pitts actually shows that any topos with some suitable properties
gives rise to a model of polymorphic lambda calculus.

>In any case, I'm familiar with the PER model of
>polymorphic type theory; I think this is essentially the same thing as
>what Hyland calls the effective topos.  In this model, the types are
>partial equivalence relations, i.e. PERs, on N, and the functions from
>one type to another are given by equivalence-preserving partial
>recursive functions.  A very nice model!  You could explain this model
>to anybody who is familiar with the rudiments of recursive function
>theory.

True. But the point is that if you want to interpret polymorphic lambda calculus
in a standard way, i.e. products are interpreted as products,
and function spaces are interpreted as full function spaces,
then you have to consider the PER model to be a topos.

>But now let's ask, what does polymorphic type theory have to do with
>f.o.m.?  Is polymorphic type theory viable as a foundational setup for
>mathematics? 

I only claimed that topos theory could serve as a foundation of mathematics
with an unlimited comprehension principle for sets. This cannot work
in ZFC by Russell's Paradox. But I think there is a chance to identify
suitable axioms that, when added to the topos axioms, give you an unlimited 
comprehension principle. (I am not sure how far this has been worked out.)
Then topos theory would be the least common denominator of

	set theory with limited comprehension, and excluded middle
and
	set theory with unlimited comprehension, without excluded middle

I merely cited polymorphism as an application of unlimited comprehension,
not as a foundation in itself.
I think that unlimited comprehension also has other applications:
for example, category theory. In category theory, all concepts (like 
category, functor, natural transformation) have a "large" and a "small" 
version, and many theorems work differently, depending on "large" or "small"
(meaning: "class" or "set"). I think that this distinction
has not to do with the essence of category theory, but is more about the
interplay between category theory and its foundation (ZFC + universe).
Nevertheless, a considerable part of category theory deals with 
smallness properties.
Now if you worked with an internal category object in a topos with unlimited
comprehension, you would not need this distinction any more.


Till