[Haskell] recursive definitions in Haskell (inductive and coinductive)

[kahl at cas.mcmaster.ca]

Norman,
 > 
 >  > AFAIK, the normal understanding is that recursive types
 >  > are the least fixed points of endofunctors on the category of CPOs,
 >  > and it is the CPO property that least upper bounds of chains exist
 >  > that forces the existence of infinite lists.
 > 
 > But ML has CPOs and infinite chains too!  The situation is simpler
 > because the only *interesting* infinite ascending chains are in
 > function domains.

That's why I (later) said ``polynomial functors'' ---
in ML, infinite chains do not arise in simple recursive datatypes like

  List A = 1 + A \times List A
.

 > To paraphrase, is what you're saying that the definition of a Haskell
 > type is the smallest fixed point that contains the bottom element
 > (divergent computation) as a member?

Standard Haskell types are interpreted as objects in the category of CPOs
that have a least element --- bottom.
(We are not talking about unboxed types here.)
Morphisms do not need to preserve the least element ---
non-strict functions are allowed.
Then + is interpreted as non-coalesced sum with non-strict injections,
and $\times$ is interpreted via non-strict pair construction,
i.e., the function (curry (id :: (a,b) -> (a,b))) is non-strict,
which gives rise to the property just emphasised by Jonathan:

    (undefined, y) /= undefined

(This hold even if  y = undefined.)

So both + and \times produce non-flat CPOs even from flat CPOs,
introducing infinite ascending chains in the recursive case.


Anyway, the bottom does not come in through the fixed point construction,
i.e., the semantics of recursion,
but rather through the initial choice of semantic domains.

 > To paraphrase, is what you're saying that the definition of a Haskell
 > type is the smallest fixed point

Technically, that fixpoint is contructed as a colimit (``inverse limit'')
of an inifinite diagram resulting from a chain of functor applications
starting from the trivial CPO with least element: {bottom}.
(The fact that it is a colimit is a generalisation of the ``smallest''
 aspect and is shared with initial algebras.)


Wolfram