<p>You are looking at this the wrong way. Almost any object can be encoded into a natural number, so it would be possible to have a programming language with a single type. But the goal is to have <em>more</em> types. You want to distinguish semantically distinct operations, even if they are encoded the same way as integers.</p>

<p>For example, you might have Boolean conjunction and integer multiplication. They encode in the same way. However, multiplying a boolean by an integer is a type error. By forcing distinct encodings, this type error is harmlessly detected at compile-time. By merging into the same encoding, this error leads to undefined semantics (even if, by the good fortune of the encoding scheme, it will be interpreted harmlessly).</p>

CC BY-SA 3.0
2011-12-03T15:24:38.833Z
2011-12-03T15:24:38.833Z
David Harris
<p>BTW, I heard “disjoint union” and <a href="http://en.wikipedia.org/wiki/Sum_type" rel="nofollow">“sum type”</a>, but not “disjoint type.”</p>

<p>Natural numbers ($\mathbb{N}$) are constructed with the help of sum types: $\mu(\lambda A. 1+A)$, where $+$ makes a sum type. What is the best approach now? ;)</p>

<p>A little offtopic. IMHO comparing approaches is a common trap. You can waste a lot of time thinking of it with a little reward and even get banned for arguing about the “best approach.” There is no right opinion.</p>

<p>Talking about the hierarchy of numbers, I'd use <a href="http://en.wikipedia.org/wiki/Structure_%28mathematical_logic%29" rel="nofollow">structures</a>. I.e., consider not only sets (types), but also algebraic operations on them. The canonical injection $\mathbb{N}\to \mathbb{Z}$ is a monomorphism of usual monoids, and this allows us to include $\mathbb{N}$ into $\mathbb{Z}$.</p>

<p>You can check that the only homomorphism of semigroups from $(2, \lor)$ to $(\mathbb{N}, +)$ is a homomorphism $\lambda x. 0$. Then the “natural” injection from $2$ to $\mathbb{N}$ is not a homomorphism. No inclusion. Although, you can try other structures on $2$, and try, and try until you find a structure with some formal properties, and then you may say that you've found a new approach (just new, not the best).</p>

<p>Of course, if you are not concerned about reasoning, you can forget structures and homomorphisms and organize types into any diagram which <strong>feels</strong> solid and neat and defend it as “the best.” Then you step directly into the aforementioned trap.</p>

CC BY-SA 3.0
2011-12-21T11:05:26.260Z
2011-12-21T11:05:26.260Z
beroal
<p>If you only think of Booleans as 0 and 1, then it is natural to include them as subtypes of natural numbers and integers. But as soon as you start applying operations to them, then things start to fall apart. </p>

<p>Consider what happens when you define the + operation on Booleans. You have two choices:</p>

<ul>
<li><p>Make + the same as <em>OR</em>, so 1+1=1. But then you have the problem that + on Booleans is no longer the same as + on Integers, which it should be.  More precisely, we have the following $(Integer)1_{Bool}+ (Integer)1_{Bool}\neq (Integer)(1_{Bool}+1_{Bool})$, where $1_{Bool}$ is true and $(Integer)\_$ is performing a cast from Bools to Integers. This means that there is a problem with <em>coherence</em> in the subtyping relation is we make this choice.</p></li>
<li><p>The second choice is to define + on Booleans so that 1+1=2. But now the operation takes you out of the world of Booleans. Semantically, this is not problematic ($\sqrt{-1}$ takes you out of the world of Real numbers), but it does suggest that you do not gain much by treating Booleans as numbers.</p></li>
</ul>

<p>Generally, the way Booleans/Integers are treated in languages like C is that Integers can be used in places where Booleans are expected, which does not really follow the usual subtyping rules. </p>

<p>Ultimately, the operations you apply to Booleans are not the same as the ones you apply to Naturals and Integers, so, from the perspective of coherence, you should not really consider them to be related by subtyping.</p>

<p><strong>Edit</strong>: 
A third alternative, suggested by <a href="https://cstheory.stackexchange.com/users/3131/peter-taylor">Peter Taylor</a> in comments, is to make + be XOR. This results in the subtype relation boolean &lt; short &lt; integer &lt; long, where + is addition-modulo-overflow. That's fairly natural, programmatically. </p>

CC BY-SA 3.0
2011-12-03T08:55:27.680Z
Surely there's a third option of making + be XOR, which is the most natural one by analogy with larger integer types. (Of course, in twos complement by the standard convention your two Boolean values are 0 and -1, but that's largely irrelevant).
Peter Taylor
CC BY-SA 3.0
2011-12-03T09:48:49.037Z
This is another option. And then you have subtype relation boolean < short < integer < long. Where + is addition-modulo-overflow. That's fairly natural, programmatically.
Dave Clarke
CC BY-SA 3.0
2011-12-03T10:14:44.950Z
I've incorporated your comment (and mine) into the answer.
Dave Clarke
CC BY-SA 3.0
2011-12-03T14:37:36.617Z
Good answer, thanks! Typo, 'should really', you mean 'should not really'?
rwallace
CC BY-SA 3.0
2011-12-03T07:35:17.087Z
2011-12-03T14:43:20.400Z
2017-04-13T12:32:28.117Z
Dave Clarke
<p>In languages oriented towards systems programming, digital logic and hardware design, it's common to treat boolean as a subtype of integer. In languages oriented towards mathematics and type theory, it's more usual to treat them as disjoint types.</p>

<p>Being from more of a systems programming background, it has always seemed to me appropriate to take the former approach. I would have thought it appropriate even from a mathematical viewpoint, since we already have a hierarchy of numeric types (natural numbers are a subtype of integer which is a subtype of rational etc.) so it would fit neatly at the start of that hierarchy; but then I'm not a real mathematician, so I may be missing something.</p>

<p>Apart from a little bit of extra error checking (catching the mistake if you pass a boolean to a function expecting an integer and you didn't mean to), is there any advantage to having them be disjoint types?</p>

CC BY-SA 3.0
2011-12-03T05:49:47.620Z
You might get a better answer on StackOverflow/Programmers SE, but it seems like you mostly answered your own question.
Huck Bennett
<pl.programming-languages><type-theory><language-design>
Boolean as subtype of integer
rwallace
# Boolean as subtype of integer

(Asked by: username_0 on 2011-12-03)

In languages oriented towards systems programming, digital logic and hardware design, it's common to treat boolean as a subtype of integer. In languages oriented towards mathematics and type theory, it's more usual to treat them as disjoint types.

Being from more of a systems programming background, it has always seemed to me appropriate to take the former approach. I would have thought it appropriate even from a mathematical viewpoint, since we already have a hierarchy of numeric types (natural numbers are a subtype of integer which is a subtype of rational etc.) so it would fit neatly at the start of that hierarchy; but then I'm not a real mathematician, so I may be missing something.

Apart from a little bit of extra error checking (catching the mistake if you pass a boolean to a function expecting an integer and you didn't mean to), is there any advantage to having them be disjoint types?

**Tags:** pl.programming-languages, type-theory, language-design

> **Comments:**
> **username_1**: You might get a better answer on StackOverflow/Programmers SE, but it seems like you mostly answered your own question.  

---

## 3 answers

### Answer by username_4 on 2011-12-03. Score: 16 | Accepted answer

If you only think of Booleans as 0 and 1, then it is natural to include them as subtypes of natural numbers and integers. But as soon as you start applying operations to them, then things start to fall apart.

Consider what happens when you define the + operation on Booleans. You have two choices:

* Make + the same as *OR*, so 1+1=1. But then you have the problem that + on Booleans is no longer the same as + on Integers, which it should be. More precisely, we have the following $(Integer)1\_{Bool}+ (Integer)1\_{Bool}\neq (Integer)(1\_{Bool}+1\_{Bool})$, where $1\_{Bool}$ is true and $(Integer)\\_$ is performing a cast from Bools to Integers. This means that there is a problem with *coherence* in the subtyping relation is we make this choice.
* The second choice is to define + on Booleans so that 1+1=2. But now the operation takes you out of the world of Booleans. Semantically, this is not problematic ($\sqrt{-1}$ takes you out of the world of Real numbers), but it does suggest that you do not gain much by treating Booleans as numbers.

Generally, the way Booleans/Integers are treated in languages like C is that Integers can be used in places where Booleans are expected, which does not really follow the usual subtyping rules.

Ultimately, the operations you apply to Booleans are not the same as the ones you apply to Naturals and Integers, so, from the perspective of coherence, you should not really consider them to be related by subtyping.

**Edit**:
A third alternative, suggested by [username_5](https://cstheory.stackexchange.com/users/3131/peter-taylor) in comments, is to make + be XOR. This results in the subtype relation boolean < short < integer < long, where + is addition-modulo-overflow. That's fairly natural, programmatically.

> **Comments:**
> **username_5**: Surely there's a third option of making + be XOR, which is the most natural one by analogy with larger integer types. (Of course, in twos complement by the standard convention your two Boolean values are 0 and -1, but that's largely irrelevant).  
> **username_4**: This is another option. And then you have subtype relation boolean < short < integer < long. Where + is addition-modulo-overflow. That's fairly natural, programmatically.  
> **username_4**: I've incorporated your comment (and mine) into the answer.  
> **username_0**: Good answer, thanks! Typo, 'should really', you mean 'should not really'?  

---

### Answer by username_2 on 2011-12-03. Score: 10

You are looking at this the wrong way. Almost any object can be encoded into a natural number, so it would be possible to have a programming language with a single type. But the goal is to have *more* types. You want to distinguish semantically distinct operations, even if they are encoded the same way as integers.

For example, you might have Boolean conjunction and integer multiplication. They encode in the same way. However, multiplying a boolean by an integer is a type error. By forcing distinct encodings, this type error is harmlessly detected at compile-time. By merging into the same encoding, this error leads to undefined semantics (even if, by the good fortune of the encoding scheme, it will be interpreted harmlessly).


---

### Answer by username_3 on 2011-12-21. Score: 0

BTW, I heard “disjoint union” and [“sum type”](http://en.wikipedia.org/wiki/Sum_type), but not “disjoint type.”

Natural numbers ($\mathbb{N}$) are constructed with the help of sum types: $\mu(\lambda A. 1+A)$, where $+$ makes a sum type. What is the best approach now? ;)

A little offtopic. IMHO comparing approaches is a common trap. You can waste a lot of time thinking of it with a little reward and even get banned for arguing about the “best approach.” There is no right opinion.

Talking about the hierarchy of numbers, I'd use [structures](http://en.wikipedia.org/wiki/Structure_%28mathematical_logic%29). I.e., consider not only sets (types), but also algebraic operations on them. The canonical injection $\mathbb{N}\to \mathbb{Z}$ is a monomorphism of usual monoids, and this allows us to include $\mathbb{N}$ into $\mathbb{Z}$.

You can check that the only homomorphism of semigroups from $(2, \lor)$ to $(\mathbb{N}, +)$ is a homomorphism $\lambda x. 0$. Then the “natural” injection from $2$ to $\mathbb{N}$ is not a homomorphism. No inclusion. Although, you can try other structures on $2$, and try, and try until you find a structure with some formal properties, and then you may say that you've found a new approach (just new, not the best).

Of course, if you are not concerned about reasoning, you can forget structures and homomorphisms and organize types into any diagram which **feels** solid and neat and defend it as “the best.” Then you step directly into the aforementioned trap.


---

