Response to Wadler: Greatest fixpoints have existential types

Date: Mon, 16 Jul 90 20:27:07 JST

> Similarly, we can make the coding
> 	Gfix X. T(X)  =  Exists X. (X -> T(X)) * X
> where Gfix is the greatest fixpoint and T is still a covariant
> functor.  Is this known?

See [1][3].

In fact, in the models satisfying Reynolds' parametricity, Gfix X. T(X) is
a terminal fixed point of T, i.e., a terminal object of the category of
T-coalgebras, as well as Lfix X. T(X) is an initial fixed point ([1], [2]).
Moreover, parametricity is partially a necessary condition for the
existence of such fixed points.  These results are used to show that in
the category of pers, every realizable endofunctor has initial and
terminal fixed points [2].

R. Hasegawa

[1] R. Hasegawa (89) Parametric polymorphism and recursive type
 definitions, Master Thesis, RIMS, Kyoto University.
[2] R. Hasegawa (90) Categorical data types in parametric
 polymorphism, in preparation.
[3] G.C. Wraith (89) A note on categorical datatypes, LNCS 389.