In Haskell, every type has at least one value – ⊥. The empty type is not actually empty – it has ⊥ in it, sum types contain the sum of the two types plus one extra element – ⊥, etc.
But we don’t always need to do this. The ⊥ value of a type has one important feature, it’s the least defined value in the type. So let’s investigate the four primitive types:
Empty – as this type has no values, there’s obviously no least defined one, so we definitely need to add an extra value.
() – this type has only one value, so that value clearly is the least defined. Thus (⊥ :: ()) can be defined safely to be ().
Sum types – any value we chose in (A + B) must carry a tag to determine which of type A or B it’s in, and so cannot be the least defined value – if we chose a value in A, it carries enough information to say it’s not in B, and vice-versa. Thus for sum types, we must add an extra ⊥.
Product types – assuming that we have bottom values in types A and B, we can define ⊥ for (A × B) as being (⊥ :: A, ⊥ :: B).
One can clearly make at least two choices here, either the choice Haskell makes – add bottom values everywhere, or add bottom values only where they are needed. One could argue convincingly that what Haskell does is very consistent and predictable, but interestingly, the other choice has some nice results.
The functor laws demand that fmap id x = x. A special case of this is that fmap id ⊥ = ⊥. Lets look at this for pairs – that means that fmap id undefined = undefined, but this isn’t as lazy as we could be – we’d like to be able to return a tuple straight away, without looking at any of the tuple we’re given.
If however we chose to only add a bottom value to a type when needed, then bottom for tuples really is (⊥, ⊥), and we’re able to define fmap for tuples as fmap f x = (fst x, f $ snd x) and not break the Functor laws.
Any more comments about this are appreciated. What other consequences does this decision have?
No Ordering 
Correct me if I’m wrong, but wouldn’t this zap the reason why fail got put in Monad? See http://www.cse.unsw.edu.au/~dons/haskell-1990-2000/msg03267.html
It looks very much like it should, yes. I guess this is like option 3++ – don’t make tuples special, but make anything where we can find a bottom already in the type “special”. I’m not sure I think they’re very special though – we’re consistently only adding values where we need to.
So what you’re arguing for is unlifted tuples.
Empty (the empty sum) and the other sum types gets a bottom stuck underneath, whereas products do not (where () is the empty product).
This is a perfectly OK decisions to make, but you have to be aware of the consequences. In the presense of seq it get’s a bit tricky. For seq we know
seq _|_ a = _|_
so that means that
seq (x, y) a
should be _|_ exactly when both x and y are _|_, but not otherwise. The means we can’t evaluate x first nor y first, because either of them might not terminate, but the other one will. So we have to evaluate both of them in parallel, and if either terminates then seq proceeds with the second argument.
So unlifted products and seq implies that the evaluator must be parallel. There’s nothing wrong with that, just a complication to be aware of.
Unlifted products are also less efficient in general.
Is that rule necessary for seq to do its thing though? i.e. is there a very similar operation to seq with margionally different semantics that fits quite happily here? It seems to me that
seq (_|_, _|_) acould quite happily still bea– we have still reduced the left argument to WHNF, it just happened that there was only one choice for that WHNF, not two.Can you give an example where unlifted products are less efficient, I’m not sure I see why. Certianly the fact that we get to have lazy fmap would suggest that in certain circumstances they’re more efficient.
You can’t have it both ways. Either (_|_,_|_) is equal to _|_ or it’s not. If they are equal, that means that they are indistinguishable in all contexts, including seq. If seq can distinguish them, then they are not equal, and by monotonicity we know that _|_ is less than (_|_,_|_).
Now, if seq was a method in a class, then we could make seq unavailable for products. But seq is no longer in a class (as it should be).
As for efficiency, consider (with unlifted products)
case e of (x, y) -> [x, y]
this must return a list with two elements even when e is _|_, and not _|_. This means that the case cannot evaluate the scrutinee, nor can x and y directly refer to the subfields of the pair. Instead it has to be compiled as
let p = e in [fst p, snd p]
So we need to build a suspension for e, fst p, and snd p. This is much less efficient than evaluating e and grabbing x and y out of the pair.
Products in Haskell are not lifted by accident. The choice between lifted and unlifted were carefully considered when the language was designed. There are good arguments both ways, but in my opinion Haskell has the simpler and more consistent design.
I wasn’t suggesting having it both ways, I was suggesting that seq _|_ a = _|_ is not necessarily something that needs to be part of seq’s semantics, merely instead that seq reduces its left hand argument to WHNF, and then returns its right argument.
I’m not sure I follow your argument about inefficiency. the compiler actually knows *much* more in the unlifted case – it knows that e will be a pair, it doesn’t have to insert a branch to check for bottom, and it knows it will always return a list. In general, it would seem, any case expression on a product type can actually be reduced to a let (because we need do no comparison any more) – in this case let (x,y) = e in [x,y].
Bob
So explain to me how you make
seq undefined a
and
seq (undefined, undefined) a
do the same thing. What is the WHNF for your pairs, and how do you compute it?
The compiler doesn’t know any more about the unlifted case. And there is never a test for _|_ in the lifted case, in fact, you can’t test for _|_; it just happens. If you are going to convince anyone about efficiency you need to explain in detail how you will compile your unlifted pairs. Perhaps there’s a marvelous way of doing it, but I sure don’t know what it is.
Tell me how you translate ‘let (x,y)=e in [x,y]’ to machine code and I will listen.
For clarity I’ll use (# #) to represent unlifted products, as opposed to the lifted products in Haskell currently.
You can represent objects of an unlifted product type as expressions with multiple return values. So, “undefined :: (# Int, Char #)” is really “(# undefined, undefined #)”, and “undefined :: (# #)” is really “(# #)”. (In the latter case, there’s no way to force evaluation of an unlifted unit; it never executes any code at all!). So, “let (#x,y#) = e in [x,y]” would translate to [ point to the first field of e, point to the second field of e ]; e is guaranteed to have both of these fields because it is an unlifted tuple.
The magic would happen in code that builds objects of these types; “bottom :: (# Int, Bool #); bottom = bottom” would translate to “bottom1 :: Int; bottom1 = bottom1; bottom2 :: Bool; bottom2 = bottom2; bottom = (# bottom1, bottom2 #)”