In type theory, the unit type can always be constructed. It has a single value,
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.
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.
- The singleton set and the unit type
- Void Type
- Void and Unit form the basis for all types
- Product Type