Remember when you were in school, and your mathematics teacher told you that 00 = 1, and you got very confused? This is the type theory equivalent of that.
So what’s this all about?
It’s about three type constructors:
0 is an “empty” type. It has no values.
1 is a “unit” type. It has one value.
A → B is the type of maps from A to B, where A and B are types.
“An” empty type?
Sure, there might be more than one empty type, and more than one unit type. But in each case they’re all isomorphic (formal way of saying “basically the same”) so we’ll treat them as one empty type and one unit type.
How would you store the unit type?
The unit type has one value, so it needs zero storage space. Any more than that would be wasting space.
How would you store the empty type?
The empty type has no values, so it doesn’t matter how much storage space it requires, as you’ll never have a value of it to store. You could decide to allocate 5G for the type, if you want, and it wouldn’t cause any problems, because those allocations would never actually happen. (Although, it might cause problems with the way you allocate non-empty types constructed with the empty type.)
What about the void type?
In some languages, “Void” is used to refer to an empty type, or some approximation thereof.
In C, C++, Java, C#, etc., the keyword void refers to the zero-byte function return structure. As such it has 2560 = 1 value, so it’s a unit type. You can think of void functions as returning only one possible “value” and therefore no information. (Functions in these languages are not maps, by the way.)
By “map”, you mean function, right?
Well, a pure function that always terminates and doesn’t do anything else. A → B just means assigning a B for every A. Two values of this type are the same if they assign the same B to each A. This kind of equality is called “extensional”, basically meaning that the things look the same from the outside.
How many values do maps have?
We’ll use |A| to indicate the number of values in type A. Then we have:
|0| = 0
|1| = 1
|A → B| = |B||A|.
So for example, |1 → A| = |A|. And |0 → A| = 1.
Wait, there’s a value of 0 → A ?
Yes. While 0 has no values, 0 → A has one value. That value is called the absurd map, and it exists but never gets looked up, or called, or whatever.
How is that possible?
Supposing I told you I could give you a value of 0. Then I’d be lying, because there are no values of 0.
But what if I told you that if you give me a value of 0, I could give you anything? Then I’d be telling the truth, because you can’t give me a value of 0. That promise is the absurd map.
“If you give me a value of 0, I’ll eat my hat.” Clearly I’m not going to break this promise.
Could there be more than one value of 0 → A ?
If you have two of these absurd maps, you have nothing you can do with them, so you have no way of telling them apart from the outside. So they’re the same map.
Doesn’t that mean 0 → A is itself a unit type?
I guess?? Sure, whatever.
How would you implement the absurd map as a function?
It doesn’t matter, since such a function will never get called. You could just make it the null pointer if that’s how you represent functions, or whatever you want.
What about the type A → 0 ?
If A has any values, then A → 0 has no values. But if A has no values, then A is basically the same as 0, and A → 0 has one value, the absurd map.
What’s this in category theory?
There’s a category where the objects are types, and the morphisms are maps. 0 is the initial object, and 1 is the final object. A → B is the exponential object BA.
How is all this done in Haskell?
Haskell does not have any of these types. It has a type of pure functions, but they are not guaranteed to terminate. It does not have an empty type or a unit type, because non-termination and other “bottom” values are included in all types, but it does have approximations of these types.
— Ashley Yakeley