Norman Ramsey nr at cs.tufts.edu
Tue Feb 2 18:27:05 EST 2010

```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

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).