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

[Norman Ramsey]

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