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

[kahl at cas.mcmaster.ca]

Norman,

 > Haskell permits recursive definitions at both the type level and the
 > term level.  Here's an example definition at the type level:
 > 
 >   data Intlist = Nil | Cons Integer Intlist
 > 
 > If my understanding is correct, Haskell takes as the definition of
 > `Intlist` the *greatest* solution to this recursion equation.
 > That is, in a vaguely domain-theoretic way, Intlist is the greatest
 > fixed point of the function
 > 
 >    f(S) = {Nil} union {Cons n ns | n in Integer, ns in S}
 > 
 > It's this 'greatest fixed point' or coinductive definition that admits
 > of infinite lists in the `Intlist` type.  Right?

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.

Haskell uses non-coalesced sum, that is,

  Left undefined /= undefined /= Right undefined,

and non-strict product, that is,

  (undefined, undefined) /= undefined,

which make these chains non-trivial.

(OCa)ML has strict constructors,
so effectively uses coalesced sum and strict product,
which makes all chains resulting from polynomial functors finite.

Therefore it is not the CPO semantics alone that creates infinite lists,
but rather the presence of non-strict data constructors.


Wolfram