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

[Janis Voigtländer]

Norman Ramsey schrieb:
> 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?

My understanding has always been that the above equation should be

   f(S) = {_|_, Nil} union {Cons n ns | n in Integer, ns in S}

and that then it depends on whether one is asking for a fixpoint *set*
or a fixpoint *cpo*, what makes or does not make for a difference
between least and greatest fixpoint.

If one asks for a set S that satisifies above equation, then the least
solution will be one with only finite and partial lists, while the
greatest solution will contain infinite lists as well.

If one asks for a cpo S that satisifies above equation, then the
difference vanishes. The least such cpo S is identical to the greatest
such cpo, because the "complete" aspect forces even the least cpo
fixpoint to contain infinite list.

Ciao,
Janis.

-- 
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:jv at iai.uni-bonn.de