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