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
