[PRL] isomorphic fixed points

[peter douglass]

Hi,
   During my talk yesterday, the question was raised of whether the 
fixed   points of a given (algebraic) type constructors were all 
isomorphic, or whether we needed to choose a "least" fixed point.  I'm 
glad we did not stray too long on this question during the talk, but I 
would like to address it now.

   Isomorphisms constitute a very undiscriminating equivalence 
relationship.  In the category of sets, all pairs of sets with the same 
cardinality are isomorphic.

   We can use cardinality to argue that all fixed points of the Maybe 
functor (in the category of sets) are isomorphic.  There are no set with 
a finite number of elements is a fixed point of the Maybe functor.  Sets 
with the cardinality of the natural numbers are all fixed points, but 
they are all isomorphic.  Finally, if we assume the continuum 
hypothesis, there are no sets with cardinality greater than the 
cardinality of the natural numbers, but less than the cardinality of the 
reals (or the powerset of the naturals).  The set of all reals is not a 
fixed point of the Maybe functor, and ... well I'm going to stop at the 
reals.

   With regard to Haskell lists having "more" elements than the finite 
lists, I'm not sure that is true.  The cardinality of the set of 
infinite lists of naturals is the cardinality of the powerset of 
naturals, or the cardinality of the reals.  However, the set of all 
Haskell lists of nats does not include the set of all infinite lists of 
nats, but only those that can be finitely represented.  So, I would 
argue that the set of Haskell lists of nats is isomorphic to the set of 
finite lists of nats.  Haskell lists might be a "greatest" fixed point 
in some sense, as someone at PL-jr claimed was claimed by third parties. 
      But if we choose "isomorphism" to be our equivalence relationship, 
Haskell lists are "equivalent" to finite lists.

   Once one accepts that isomorphism is a poor notion of equivalence, 
one might find this very troubling for category theory.  If objects are 
so frequently isomorphic, are not the results of category theory 
somewhat vacuous?  We are talk about lists, and Nats etc as if they were 
different "objects", but in the end, they all seem to be isomorphic!  I 
think the answer to this is to remember that what are important are the 
arrows and not the objects.

--PeterD