Unit Type

In type theory, the unit type can always be constructed. It has a single value, unit.

It is related to the singleton set from set theory and dual to the void type

In Haskell, unit is represented with the empty list ().

It's possible to construct the function f :: a -> () easily, as unit can always be constructed.

Similarly, f :: () -> Int or to any other concrete type in a pure language acts as a constant for a specific value. When corresponding this idea into category theory it's possible to use this to define all objects within the category - this is the initial object. Not every category has an initial object.

Backlinks

• The singleton set and the unit type
  • The singleton set from set theory corresponds to the Unit type from type theory. Also to true in logic, and to a 1-category in category theory.
• 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.
• Dual
  • It's dual is the unit type. It corresponds to the empty set from set theory.
• Void and Unit form the basis for all types
  • In type theory, void and unit form the basis for all other types.
• Product Type
  • Product types have a monoidal identity of Unit. $|Unit| = 1$.