Cardinality can be used to express maths concepts

Each type has a cardinality. This allows us to express equations and ideas from maths using only types because of the Curry-Howard isomorphism.

For example

$$(a, ()) \cong a \because |(a, ())| = |a| * |()| = |a| * 1 = |a|$$

We can even provide functions for this isomorphism to further prove it

to :: (a, ()) -> a
to (a, _) = a

from :: a -> (a, ())
from a = (a, ())

References

• thinking with types