Exponentiation Types

A pair colleagues of mine and I have been staring at an interesting riddle, which I’m guessing exists in the literature somewhere. He pointed out that we have sum types where a+b is the type containing all the values in a, and all the values in b, we have product types where a*b is the type containing all the values which contain an a, and a b. What we don’t have though is exponentiation types. The riddle then – what is the type ab?

Bart realised that this type is b -> a. The type contains all functions that map bs onto as. This has some rather nice mathematical properties. We know from our early maths a couple of rules about exponents:

ab * ac = ab+c

This gives us a rather nice isomorphism: (b -> a, c -> a) is equivalent to (b + c) -> a. That is, if we have one function that produces an a from bs, another that gives us an a from cs, we can write a function that gives us as, given either a b or a c, and vice versa.

Secondly, and perhaps even nicer
(ab)c = ab*c

This gives us a different isomorphism: c -> b -> a is equivalent to (b,c) -> a. Woohoo, we have currying!

This seems very close to the curry-howard isomorphism, but not quite there. Does anyone know who’s discovered this already?

Bottoms

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?