Boolean as subtype of integer

Question

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?

Answer 1

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 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.

Answer 2

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 3

BTW, I heard “disjoint union” and “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. 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.