0
$\begingroup$

I have a doubt about the Unit Type in the context of Type Theory and its use in different case scenarios.

To start with, a Unit Type can be seen as a nullary Product Type, namely Unit, with one only value term which is the empty tuple, (). Also, there exist a unique map from any type to the Unit.

Now, it happens that the use of the Unit Type goes beyond such trivial definition, and is in fact used in the definition of Algebraic Data Types, which are Sums of Product Types. Specifically, it is possible to represent the concept of an Enumerated Type using a Sum of Unit Types, e.g. in StandardML we might have:

datatype suit = HEARTS | CLUBS | DIAMONDS | SPADES

where HEARTS, CLUBS, DIAMONDS and SPADES are nullary Product Types and therefore all isomorphic to the Unit.

My doubt is the following: if there exist only one element of Unit, how can the type system distinguish between the four distinct instances used in the Sum Type above (five instances if we also consider the empty tuple...)? I understand that they can be considered all equal to each other up to isomorphism, but they are extensionally different and in fact, even by considering only the suit we are supposed to pattern-match on them...

$\endgroup$
2
$\begingroup$

The short answer is that isomorphic types are not equal, despite behaving identically, and so the type system can distinguish between them. In a nominal type system, like the one you describe, types are essentially identified by their names, even if they are structurally equivalent. This is the case for the five unit types you describe: they are structurally equivalent, but nominally unequal, and so they are treated as distinct.

Note that the pattern matching aspect is orthogonal: you can think of the five unit types as existing in isolation. In most type theories, you can take the sum of any two types, even two that are (nominally) equal, e.g. Unit + Unit. You will still be required to pattern match, and will have two cases: the left Unit and the right Unit. The nominal aspect is unimportant, although many programming languages will use the names to distinguish between the different cases like this, instead of the indices of the summands (in particular, in languages where you are only allowed to take sums of distinct nominal types, like Standard ML).

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks, now it's definitely clearer! The problem I mentioned, then, arises only if the 4 Unit types were created aliasing the ()... Am I correct? $\endgroup$ – gifa May 5 at 11:49
  • 2
    $\begingroup$ If you instead create aliases to () with different names, you won't be able to distinguish between them, yes. However, it would still be possible to pattern match on a sum: you'd just have to have a type system where you case split on the indices of the sum, rather than the names of the summands (using indices rather than names is standard in type theories, like the simply-typed $\lambda$-calculus, but not so much in programming languages). $\endgroup$ – varkor May 5 at 12:15
  • $\begingroup$ Indeed, I faced the problem when trying to materialize type theory constructs in a programming language. Thanks for the clarifications! $\endgroup$ – gifa May 5 at 13:39

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.