Following up this discussion on which laws are there in the presence of lifting, which are not, and which one do we actually care about, here is another observation. On most occasions when you (well, I actually) write a datatype, you think about it inductively. In a lazy language however, you get a few more values than you bargained for. This has some nasty effects on program verification. Example: data Nat = Zero | Succ Nat add Zero x = x add (Succ x) y = add x (Succ y) An apparently perfectly reasonable definition of natural numbers and addition. However, the type Nat also contains the fixpoint of Succ and all its approximations. As a consequence, the law add x y = add y x doesn't hold, neither does add x Zero = x because x could be the fixpoint of Succ, or Succ(_|_), etc. (For similar reasons reverse(reverse xs)=xs isn't true for lists.) A different definition for add can do the trick in the example, but this is beside the point, i.e. that each datatype definition gives us these extra values we are usually not interested in. This is quite awkkward when it comes to teaching first-year students inductive proofs if the language they work with is lazy. It is very tempting then to cheat and not to reveal the full truth about the set of values defined by a datatype definition. I don't like to cheat. But I don't like strictness annotations either. They mess up the syntax and are just ugly. Perhaps it would be nice to have two notions of datatypes, one inductive (with all constructors being strict) and the usual lazy datatypes. The appropriate notion of strictness is probably to compute the WHNF (rather than the NF) of all arguments when applied. -- Stefan Kahrs