Types have a cardinality

In type theory a type has a cardinality. The cardinality for a given type is the number of possible values. A cardinality can be finite or infinite. A pair of types with the same cardinality will always be isomorphic.

Cardinality for a type $T$ is expressed $|T|$. For example for the type

data Boolean = True | False

Then $|Boolean| = 2$ should be read as the cardinality of Boolean is equal to 2

References

• Book: Thinking with types

Backlinks

• Void Type
  • In type theory, the void type is a type with a cardinality of $0$. It is therefore impossible to construct. It's dual is the unit type. It corresponds to the empty set from set theory.
• Type Theory
  • Types have a cardinality, which is the number of possible values within that type.
• 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.
• Function types are like exponentiation for cardinality
  • The cardinality of a function type is the second argument to the power of the first.
• Product Type
  • A product type is the result of the product operation on algebraic types. The cardinality of a product type is the product of it's fields. For example
• Sum Type
  • The cardinality of a sum type is the sum of all the cardinailities of it's constructors. $|Boolean| = 2$