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?
Uses of the type Unit
lambda calculus;curry howard
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.