Strictness annotations do not completely remove the need for unlifted
products. (However, on balance I am inclined to stay with lifted
products only, rather than add a new language feature.)
In a lifted product, bottom /= (bottom, bottom). That is, a new bottom
is added onto the produce, so the product is lifted above these. In an
unlifted product, bottom = (bottom,bottom). Miranda claims to use
unlifted products for tuples while Haskell uses lifted products.
Consider the function:
f(x,y) = 5
In either either Haskell or Miranda, f(bottom, bottom) = 5. In Miranda,
since (bottom, bottom) = bottom, it must be the case that f bottom = 5,
and it is. In Haskell, on the other hand, f bottom = bottom. Pattern
matching always forces evaluation at least to the point where the
constructor is applied, even in the case where there is only one
constructor. If we define
g [] = 5
g (x:xs) = 5
you would expect g bottom = bottom, and Haskell treats f in a similar
manner even though there is only one constructor for an ordered pair.
If we make the pairing operator, (_,_), strict in both arguments, then
f (bottom, bottom) = f bottom = bottom
On the other hand, if we make products unlifted, then
f (bottom, bottom) = f bottom = 5
In either case, (bottom, bottom) = bottom, but stirctness annotations
also make (bottom, x) = (x, bottom) = bottom for all x, which is not the
case with unlifted products.
As Phil Wadler pointed out, with lifted tuples the types
(a,b) -> c and a -> b -> c
are not isomorphic because the domain for (a,b) contains an extra bottom
element. That is, there isn't a one-to-one correspondence between
curried and uncurried functions! Strictness annotations do not solve
this problem.
Miranda has both a mechanism for forcing strictness and unlifted
products. In Miranda
seq x y = y, if x \= bottom
= bottom, if x = bottom
For example,
seq bottom 5 = bottom
Since Miranda uses unlifted products, it must be the case that
seq (bottom, bottom) 5 = seq bottom 5 = 5
but is isn't! Miranda incorrectly (according to the language
definition) gives
seq (bottom, bottom) 5 = 5
To correctly evaluate seq (x, y) 5 it would be necessary to concurrently
evaluate x and y, since (x, y) is bottom if and only if both x and y are
bottom. (I enjoy finding a flaw in Miranda because there are so few to
be found!)
Warren Burton
Simon Fraser University