23 Jun
2006
23 Jun
'06
12:53 p.m.
On Thu, Jun 22, 2006 at 05:44:58PM +0100, I wrote:
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
On second thoughts, I think the fixed points coincide in these cases too.