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

[Jonathan Cast]

On Tue, 2010-02-02 at 23:43 +0000, kahl at cas.mcmaster.ca wrote:
> 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.

To clarify, strict product not only means

    (undefined, undefined) == undefined

(as above), but also

    (undefined, y) == undefined == (x, undefined)

for all x, y.  This is the property that forces infinite lists, say:

    x : undefined /= undefined

and so

    undefined, x0 : undefined, x0 : x1 : undefined, ...

is a *strictly* increasing sequence, which must have an (infinite)
supremum.

jcc