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?