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