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@iai.uni-bonn.de