[Haskell] recursive definitions in Haskell (inductive and
coinductive)
Jonathan Cast
jonathanccast at fastmail.fm
Tue Feb 2 21:25:23 EST 2010
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
More information about the Haskell
mailing list