Haskell Language Type algebra Natural numbers in type algebra
Example
We can draw a connection between the Haskell types and the natural numbers. This connection can be made assigning to every type the number of inhabitants it has.
Finite union types
For finite types, it suffices to see that we can assign a natural type to every number, based in the number of constructors. For example:
type Color = Red | Yellow | Green
would be 3. And the Bool type would be 2.
type Bool = True | False
Uniqueness up to isomorphism
We have seen that multiple types would correspond to a single number, but in this case, they would be isomorphic. This is to say that there would be a pair of morphisms f and g, whose composition would be the identity, connecting the two types.
f :: a -> b
g :: b -> a
f . g == id == g . f
In this case, we would say that the types are isomorphic. We will consider two types equal in our algebra as long as they are isomorphic.
For example, two different representations of the number two are trivally isomorphic:
type Bit = I | O
type Bool = True | False
bitValue :: Bit -> Bool
bitValue I = True
bitValue O = False
booleanBit :: Bool -> Bit
booleanBit True = I
booleanBit False = O
Because we can see bitValue . booleanBit == id == booleanBit . bitValue
One and Zero
The representation of the number 1 is obviously a type with only one constructor. In Haskell, this type is canonically the type (), called Unit. Every other type with only one constructor is isomorphic to ().
And our representation of 0 will be a type without constructors. This is the Void type in Haskell, as defined in Data.Void. This would be equivalent to a unhabited type, wihtout data constructors:
data Void
