Response to Wadler: Greatest fixpoints have existential types

• To: types
• Subject: Response to Wadler: Greatest fixpoints have existential types
• From: ryu@kurims.kurims.kyoto-u.ac.jp (Ryu Hasegawa)
• Date: Tue, 17 Jul 90 11:21:29 EDT
• Sender: meyer@theory.lcs.mit.edu

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.

• Prev: Greatest fixpoints have existential types
• Next: Call for papers: MFPS91
• Index(es):
  • Main
  • Thread