I think it's important to realize that laws aren't being entirely
lost -- they're just being weakened a (wee) bit, in the form of
carrying an extra constraint. For example, eta conversion:
\x -> f x = f
must simply be modified slightly:
\x -> f x = f if f /= _|_
(I should also point out that even the first equation comes with an
implicit constraint: it only holds if \x -> f x is type correct!
E.g. 5 /= \x -> 5 x, even in an untyped system, reflecting the fact
that eta conversion holds for pure lambda calculus, but not pure lambda
calculus plus constants. Maybe this is even more reason to put
strictness into the type system! :-)
Similarly, given an equation:
f (Foo x y) = y
If Foo is strict in its first component then I can't use this equation
at will; I need to qualify it:
f (Foo x y) = y if x /= _|_
(And again, the first equation actually comes with an extra implicit
constraint: it only holds if we know all the other equations for f
that lexically preceed it don't hold.) The same situation arises, of
course, if we can define strict functions.
We simply need to decide whether this extra complexity is worth having
the extra "expressiveness" of strict functions and constructors. I think
it probably is.
-Paul
