The unit type is the canonical type with exactly one element, named unit and represented by the empty tuple ().
It describes only a single value, which consists of said constructor applied to no arguments whatsoever.
Unit is analogous to void in languages derived from C: even though void has no elements that can be named, it represents the return of control flow from a function with no additional information.
In functional programming, Unit is the return type of things that “return nothing”.
Mathematically, this is represented by a single completely uninformative value, as opposed to an empty type such as Empty, which represents unreachable code.
When programming with monads, Unit is especially useful.
For any type α, m α represents an action that has side effects and returns a value of type α.
The type m Unit represents an action that has some side effects but does not return a value.
There are two variants of the unit type:
Unit is a Type that exists in the smallest non-propositional universe.
PUnit is universe polymorphic and can be used in any non-propositional universe.
Behind the scenes, Unit is actually defined as PUnit.{1}.
Unit should be preferred over PUnit when possible to avoid unnecessary universe parameters.
If in doubt, use Unit until universe errors occur.
The canonical type with one element. This element is written ().
Unit has a number of uses:
It can be used to model control flow that returns from a function call without providing other information.
Monadic actions that return Unit have side effects without computing values.
In polymorphic types, it can be used to indicate that no data is to be stored in a particular field.
The only element of the unit type.
It can be written as an empty tuple: ().
The canonical universe-polymorphic type with just one element.
It should be used in contexts that require a type to be universe polymorphic, thus disallowing
Unit.
Constructors
PUnit.unit.{u} : PUnit
The only element of the universe-polymorphic unit type.
Unit-like types are types that have exactly one element.
In particular, a non-recursive inductive types with a single constructor in which each parameter's type is either unit-like or a proposition is unit-like, as is a function type whose codomain is unit-like.
PUnit is one such type.
Nat → PUnit is another.
All elements of unit-like types are definitionally equal to all other elements.
Types with parameters may be unit-like only for some instantiations of the parameters.
UnitBoth CustomUnit and AlsoUnit are unit-like types, with a single constructor that takes no parameters.
Every pair of terms with either type is definitionally equal.
inductive CustomUnit where
| customUnit
example (e1 e2 : CustomUnit) : e1 = e2 := rfl
structure AlsoUnit where
example (e1 e2 : AlsoUnit) : e1 = e2 := rfl
Inductive types with parameters, such as WithParam, are also unit-like if all their fields' types are unit-like or proofs.
This check is performed after the parameters are instantiated.
structure WithParam (α : Type) where
a : α
a_eq_a : a = a
example (x y : WithParam Unit) : x = y := rfl
Note that in this example, WithParam α is only unit-like if α is unit-like. The following fails.
example (e1 e2 : WithParam Nat) : e1 = e2 := rfl