[Haskell-cafe] Functional progr., images, laziness and all therest

[Ross Paterson]

On Thu, Jun 22, 2006 at 11:06:38AM -0400, Robert Dockins wrote:
> <aside>
> Every few months a discussion arises about induction and Haskell  
> datatypes, and I feel compelled to trot out this oft-misunderstood  
> fact about Haskell: 'data' declarations in Haskell introduce co- 
> inductive definitions, NOT inductive ones.  Induction, in general,  
> does not apply to ADTs defined in Haskell; this is in contrast to  
> similar-looking definitions in, eg, ML.  This is a common source of  
> confusion, especially for mathematically-inclined persons new to  
> Haskell.  Does anyone know of a good reference which clearly explains  
> the difference and its ramifications?  I've never been able to find a  
> paper on the topic that doesn't dive head-first into complicated  
> category theory (which I usually can't follow) ...
> </aside>

I think that's untrue, from a certain point of view.

A convenient semantics for Haskell data types includes values for
non-termination (_|_, or "bottom"), partial values (containing _|_) and
infinite values, with a termination ordering -- a complete partial order
(cpo for short).  The infinite values are needed for the "complete"
part: they arise as the limits of ascending chains of partial values.
(The semantics of ML types has extra values too, but in a different
place: the partial functions in the -> type.)

You can do induction over Haskell data types, as long as your predicate
is well-behaved on limits (which conjunctions of equations are), and
also satisfied by _|_.  There's a good introduction to this sort of
reasoning in "Introduction to Functional Programming using Haskell"
by Bird (or the first edition by Bird and Wadler).

It works because Haskell 'data' definitions yield both an initial fixed
point (with respect to strict functions) and a terminal fixed point (with
respect to arbitrary functions), and moreover these are usually the same.
The former is inductive, the latter co-inductive.  They differ only when
the definition is strict in the recursive type, as in

	data Nat = Zero | Succ !Nat

The initial fixed point is the natural numbers plus _|_.
The terminal fixed point has those elements plus an infinity.
The former corresponds to what Haskell provides.

So actually Haskell data types are always inductive, and usually also
co-inductive.