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?
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 (, ).
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 .
 R. Hasegawa (89) Parametric polymorphism and recursive type
definitions, Master Thesis, RIMS, Kyoto University.
 R. Hasegawa (90) Categorical data types in parametric
polymorphism, in preparation.
 G.C. Wraith (89) A note on categorical datatypes, LNCS 389.