[Prev][Next][Index][Thread]
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.