recursive definitions in Haskell (inductive and coinductive)
I'd appreciate a word from the experts to see if my understanding of recursive definitions in Haskell is correct---I would hate to be telling my students pernicious lies. 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? Contrast this situation with recursion at the term level. Suppose I define evens :: Intlist evens = 0 `Cons` intmap (2+) evens where intmap f Nil = Nil intmap f (Cons n ns) = Cons (f n) (intmap f ns) Here the solution to the recursion equation is totally different---at the term level, the definition of `evens` is taken to mean the *least* fixed point of the function \e -> 0 `Cons` intmap (2+) e. In this case its not obvious that there's any difference, but if we consider strange :: Intlist strange = intmap (2*) strange then Haskell is very definitely going to make `strange` the least defined solution to this equation, which means `undefined` and not, for example, `Nil` or `Cons 0 Nil`, both of which also solve the recursion equation. Is this the right story? One of my difficulties is that I'm having trouble grasping what coinduction might mean for terms. For types/sets/domains, I've found Andy Gordon's very nice tutorial at http://research.microsoft.com/en-us/um/people/adg/publications/fp94.ps But I'm not sure what a greatest solution to an equation involving values might be, or even if such a thing exists (aside from adding an arbitrary top element to form a lattice of values, which seems most unsatisfying). Comments, corrections, and cues about good papers are all cheerfully solicited! Norman
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
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.
But ML has CPOs and infinite chains too! The situation is simpler because the only *interesting* infinite ascending chains are in function domains. To paraphrase, is what you're saying that the definition of a Haskell type is the smallest fixed point that contains the bottom element (divergent computation) as a member? Norman
Norman,
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.
But ML has CPOs and infinite chains too! The situation is simpler because the only *interesting* infinite ascending chains are in function domains.
That's why I (later) said ``polynomial functors'' --- in ML, infinite chains do not arise in simple recursive datatypes like List A = 1 + A \times List A .
To paraphrase, is what you're saying that the definition of a Haskell type is the smallest fixed point that contains the bottom element (divergent computation) as a member?
Standard Haskell types are interpreted as objects in the category of CPOs that have a least element --- bottom. (We are not talking about unboxed types here.) Morphisms do not need to preserve the least element --- non-strict functions are allowed. Then + is interpreted as non-coalesced sum with non-strict injections, and $\times$ is interpreted via non-strict pair construction, i.e., the function (curry (id :: (a,b) -> (a,b))) is non-strict, which gives rise to the property just emphasised by Jonathan: (undefined, y) /= undefined (This hold even if y = undefined.) So both + and \times produce non-flat CPOs even from flat CPOs, introducing infinite ascending chains in the recursive case. Anyway, the bottom does not come in through the fixed point construction, i.e., the semantics of recursion, but rather through the initial choice of semantic domains.
To paraphrase, is what you're saying that the definition of a Haskell type is the smallest fixed point
Technically, that fixpoint is contructed as a colimit (``inverse limit'') of an inifinite diagram resulting from a chain of functor applications starting from the trivial CPO with least element: {bottom}. (The fact that it is a colimit is a generalisation of the ``smallest'' aspect and is shared with initial algebras.) Wolfram
On Tue, 2010-02-02 at 23:43 +0000, kahl@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
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
participants (5)
-
Janis Voigtländer -
Jonathan Cast -
kahl＠cas.mcmaster.ca -
Norman Ramsey -
nr＠cs.tufts.edu