[Prev][Next][Index][Thread]
set-models of polymorphism
Date: Tue, 7 Feb 89 15:24:49 -0100
To: types@theory.LCS.MIT.EDU
A TYPE-THEORETIC VERSION OF REYNOLD'S RESULT
ON THE NON-EXISTENCE OF SET-MODELS OF POLYMORPHISM
This message can be seen as a sequel of one previous message of A. Pitts
entitled ``An extension of Reynolds' result on the non-existence of
set-models of poymorphism'' of which I refer for precisions and
bibliography (in particular, notice that the following argument is
really intuitionistic, and even minimal).
We describe a type-theoretic counterpart of Reynolds' result
which is used to produce a new paradox for Type:Type.
------------------------------------
The idea is to translate Reynolds' argument in the system U, which is the
extension of simple type theory to the second-order lambda-calculus.
Sketch of a definition of the system U:
extend the system F with a primitive type Prop, and logical
constants =>:Prop->Prop->Prop, forall:(X:Type)(X->Prop)->Prop
and Forall:((X:Type)Prop)->Prop, and define what are the true propositions
as usual (for instance, B finite set of propositions
B |- phi(X)
============================ X not free in B
B |- Forall X:Type.phi(X)
B |- Forall X:Type.phi(X)
========================== T arbitrary types
B |- phi[X/T]
B, phi |- psi
=============
B |- phi => psi
etc...)
In this system we can define PHI(X) = (X->Prop)->Prop, which
extends fonctorially on terms: if f:X->Y, PHI(f):PHI(X)->PHI(Y).
We build A0 = (X:Type)((PHI X)->X)->X (as in Reynolds' paper)
which is a "weak initial object", so that we have a term
intro: (PHI A0)->A0 and for any f : (PHI X)->X
a term (iter X f): A0 ->X, such that
iter X f (intro z) = f (PHI(iter X f) z) [z:PHI(A0)]
In particular, we can define
match: A0->PHI(A0)
by match = (iter PHI(A0) PHI(intro)).
ASIDE REMARK: we expect to have (match (intro z)) = z for z:PHI(A0), but
this is not true for the conversion of the lambda-calculus (this is a general
problem with the coding of primitive recursion in the system F).
The problem is now what becomes in this setting the "method at the
heart of the Adjoint Functor Theorem" used for getting a true initial
T-algebra.
If we remember that a set becomes a p.e.r. in type theory (see Lambek-Scott
for instance) the answer has to be: it becomes the construction of a
special p.e.r. E0 on the type A0, so that (A0,E0) is now an initial
T-algebra in the category of "sets". This E0 can be seen as an induction
principle on A0.
The construction of E0 (the type-theoretic counterpart of the
"big equalisers") runs as follows: PHI can be extended to relations
so that
PHI2(R) : PHI(X)->PHI(X)->Prop if R:X->X->Prop,
in such a way that PHI2(R) is a p.e.r. if R is a p.e.r.
(we take (cf. logical relations)
PHI2(R)(z1,z2) = (u1,u2:X->Prop)((x1,x2:A)(R x1 x2)->(equiv (u1 x1) (u2 x2)))
->(equiv (z1 u1) (z2 u2))
where equiv is the equivalence between propositions, which is the canonical
p.e.r. on Prop)
The p.e.r. E0 on A0 is:
E0(x,y) = (R:A0->A0->Prop)(p.e.r. R)->
[(z1,z2:(PHI A0))(PHI2(R) z1 z2)->(R (intro z1) (intro z2))]->
R(x,y).
It is then possible to show that (intro,match) defines an isomorphism
between (PHI(A0),PHI2(A0)) and (A0,E0), that is, we have
(x:A0)(E0 x x)->(E0 x (intro (match x)) (1)
and
(z:PHI(A0))(PHI2(E0) z z)->(PHI2(E0) z (match (intro z)) (2)
From this we derive a paradox (and actually only (2) is used).
For we have that for the p.e.r. (cf. logical relations)
F0(f1,f2) = (x1,x2:A0)(E0 x1 x2)->(equiv (f1 x1) (f2 x2))
on A0->Prop, the set (A0->Prop,F0) is embedded in the set (A0,E0)
(via the set (PHI(A0),PHI2(E0))), and we can then apply the
usual Cantor's argument.
Finally, we notice that we can interpret all this argument
in Type:Type, by replacing everywhere Prop by Type.
A precise study of the computational behaviour of this paradox
(similar to the one of Howe LICS 87) is still to be done.
Experimentally, the term doesn't seem to loop (it is still too big for doing
computations by hand) , and thus it's likely that it will yet not provide a
fixpoint combinator for Type:Type.
Questions:
1. can this argument be seen as A. Pitts' argument expressed in
internal logic?
2. is there a simple categorical version of this argument for Type:Type?
3. can the Burali-Forti argument be used also to give the result that there
is no set-theoretic model of polymorphism?