If you want to make money online : Register now

# [Solved]: Uses of the type Unit

, ,
Problem Detail:

The `Unit` type is a singleton type containing the constant `unit`. In functional languages with side effects, `unit` is used in functions that perform side effects. For example `print` is a function from `string` to `Unit`.

`Unit` also corresponds to truth. If you view the type of the expression as a proposition and the program as a proof, `Unit` corresponds to truth since you can always prove `Unit` by using the constant `unit`.

My question is aside from these two uses, is there any other uses of `Unit`?

#### Answered By : Anton Trunov

Some other usages of the type `Unit` (I'm sure the list is not exhaustive):

(1) The value of type `Unit` is used to simulate functions of arity 0 in strict languages that don't have zero-argument functions, like in OCaml: `f ()`. Essentially this is just for deferring computations.

(2) It also can be used to instantiate some parametrically polymorphic type when the actual "payload" is not some data, but the shape of a data structure, like when it's only the length of a list is of interest to us.

(3) `Unit` is used in dependently typed languages, for instance as a type-level analogue of the empty list or a dummy value. A simple example in Coq:

``Fixpoint nat_to_tuple (n : nat) : Set := match n with   | O => unit                 (* ! *)   | S n' => nat * nat_to_tuple n' end % type.  Eval compute in (nat_to_tuple 3).  (* Evaluates to (nat * (nat * (nat * unit)))    Note: unit in Coq corresponds to Unit in the question;          nat is the type of natural numbers;          Set is the type of types of programs.  *) ``

You might want to take a look at a more educational (but longer) example on implementing the head function(`hd`) for length-indexed lists in the Certified Programming with Dependent Types book by A. Chlipala.