Unit type

In the area of mathematical logic and computer science known as type theory, a unit type is a type that allows only one value (and thus can hold no information). The carrier (underlying set) associated with a unit type can be any singleton set. There is an isomorphism between any two such sets, so it is customary to talk about the unit type and ignore the details of its value. One may also regard the unit type as the type of 0-tuples, i.e. the product of no types. In the area of mathematical logic and computer science known as type theory, a unit type is a type that allows only one value (and thus can hold no information). The carrier (underlying set) associated with a unit type can be any singleton set. There is an isomorphism between any two such sets, so it is customary to talk about the unit type and ignore the details of its value. One may also regard the unit type as the type of 0-tuples, i.e. the product of no types. The unit type is the terminal object in the category of types and typed functions. It should not be confused with the zero or bottom type, which allows no values and is the initial object in this category. Similarly, the Boolean is the type with two values. The unit type is implemented in most functional programming languages. The void type that is used in some imperative programming languages serves some of its functions, but because its carrier set is empty, it has some limitations (as detailed below). Several computer programming languages provide a unit type to specify the result type of a function with the sole purpose of causing a side effect, and the argument type of a function that does not require arguments. In C, C++, C#, D and Java, void is used to designate a function that does not return anything useful, or a function that accepts no arguments. The unit type in C is conceptually similar to an empty struct, but a struct without members is not allowed in the C language specification. Instead, 'void' is used in a manner that simulates some, but not all, of the properties of the unit type, as detailed below. Like most imperative languages, C allows functions that do not return a value; these are specified as having the void return type. Such functions are called procedures in other imperative languages like Pascal, where a syntactic distinction, instead of type-system distinction, is made between functions and procedures.