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.