5
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ I just thought of another use. For inductively defined datatypes unit is used as the argument for the constructors in the base case. For example data 'a list = [] of Unit | (::) of 'a * 'a list. $\endgroup$ – Justin Raymond Apr 3 '16 at 2:36
  • $\begingroup$ I'm not sure I follow this example. Most languages just let you write your base cases without using dummy values/types. What's the purpose of using Unit here? Why not just data 'a list = [] | (::) of 'a * 'a list? $\endgroup$ – Anton Trunov Apr 3 '16 at 8:28
  • $\begingroup$ Yes, but formally we need a dummy type for the [] case. To formally define the type of a list we move the "loop" over to the right hand side of =, and introduce an explicit recursion operator u (Greek lowercase mew). So the formal definition of a list is list = u T . Unit + 'a x T. In "real" languages Unit is dropped because it not needed, but in research papers or textbooks it is sometimes included for formal reasons. $\endgroup$ – Justin Raymond Apr 3 '16 at 15:41
  • $\begingroup$ In "Types and Programming Languages" by Pierce there is a complete explanation of the formalization of recursive types in the chapter "Recursive Types". If you don't have access to the book here is a pdf that is basically notes on that chapter. $\endgroup$ – Justin Raymond Apr 3 '16 at 16:04
  • 1
    $\begingroup$ "Practical Foundations for Programming Languages" by Harper has a chapter on recursive types and Mitchell also talks about them in "Foundations for Programming Languages" in the chapter on variations and extensions of PCF $\endgroup$ – Justin Raymond Apr 3 '16 at 16:21
2
$\begingroup$

I can think of a couple:

  1. If a language makes a distinction between functions that return a value, and those that don't, it becomes difficult to stitch functions together. You have one set of functions that do return a value, and one set that doesn't. You end up having to write somewhat duplicated higher order functions. One set of higher order functions that work on a function that returns a value, and one set that doesn't. Or you say "just wrap your function that returns a value in one that doesn't", incurring an extra function call overhead.

  2. Sometimes you have a function that is interesting only if it succeeds. If you have a type like Haskell's Either (returns either A or B, but never both), you can pair it with a unit. You can get a function that returns unit on success, and some sort of error class/enum/monad/what have you on failure. That means that when there's an error, you have something you can poke to get more information from (instead of, say, a status code). Granted, you don't necessarily need a unit, but having unit makes it absolutely clear that the value is uninteresting.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.