On Fri, 26 Sep 2003, Derek Elkins wrote:

On Thu, 25 Sep 2003 12:59:37 -0700 Mark Tullsen <tullsen@galois.com> wrote:

...

Haskell has lazy/lifted products and not true products.

Aren't lazy products true products? What makes something a product is: fst (x,y) = x snd (x,y) = y for all x and y. This holds with lazy products but not eager ones fst (3,_|_) = _|_ /= 3

Right, strict languages do not have true products either. A strict language without side-effects, and in which no expression can loop infinitely or cause an error (because these are side-effects of a sort), COULD have true products. The reason Haskell doesn't is that true categorical products have to satisfy an additional law, (fst x, snd x) = x and Haskell's products don't, since (_|_, _|_) /= _|_ The key question is: can we write a program which distinguishes these two values? And we certainly can, for example seq (_|_,_|_) 0 = 0 seq _|_ 0 = _|_ or case (_|_,_|_) of (_,_) -> 0 = 0 case _|_ of (_,_) -> 0 = _|_ But of course, *fst and snd* can't distinguish the two! So if we only operated on products using fst and snd, then we could pretend that these two values *were* equal, even though they're not in the implementation, and thus say that Haskell had true products. This leads some people to suggest that the behaviour of seq and pattern matching be changed, so as not to distinguish these two values either. A possible change would be to make both seq and case lazy for product types, so that if x were a pair, then seq x y would NOT force the evaluation of x, and case x of (a,b) -> e would behave as case x of ~(a,b) -> e, i.e. x would be demanded only when one of a or b was needed. This would be a good thing, in that Haskell would have a nicer algebra, but a bad thing, in that it would conceal a difference which is really present in the implementation, thus denying the programmer a degree of control over what the implementation does. Namely, a programmer would no longer be able to move the evaluation of a pair earlier than its components are needed, by using a seq or a case (or in any other way). Unfortunately, that control may sometimes be vitally important. Anyone who has removed space leaks from Haskell programs knows the importance of controlling evaluation order, so as, for example to drop pointers to garbage earlier. Consider an expression such as if ...condition containing the last pointer to a very large datastructure... then (a,b) else (c,d) where a, b, c and d are perhaps expressions which *build* a very large data-structure. Evaluating this expression early enables a lot of garbage to be collected, but evaluating a component early allocates a lot of memory before it is needed. Thus it's important to be able to force just the pair structure, without forcing components, and this distinguishes _|_ from (_|_,_|_), however it is done. Space debugging does, to quite a large extent, involve inserting seq in judiciously chosen places. These places are hard to predict in advance (before seeing the heap profile). If Haskell had true products, and it turned out that the place needing a seq happened to have a pair type, then that simple fix would not be applicable. The programmer would need to refactor the program, replacing the pair by another type representing a lifted product, before the space leak could be fixed. That might require changing an arbitrarily large part of the program, which is clearly not desirable. So there are good arguments both for and against having "true products". The debate has raged many times during the Haskell design process. In the end, the argument that Haskell's designers should not make finding and fixing space leaks any harder than it already is won, and I think that was the right decision -- but it is a trade-off, and one must recognise that. Incidentally, exactly the same problem arises for functions: Haskell does not have "true functions" either, because _|_ and \x -> _|_ are not equal. John Hughes