Narrowing a boolean

Narrowing › boolean. The names in the examples are those of section 2.

A boolean alternative is the bare kind, true or false, or a single value: boolean = true, boolean = false. There is no interval and no order, so a boolean has the smallest sets of any kind, and the narrowing is mostly about which of the two values a branch leaves and whether null stays.

A boolean also has a role that the other kinds do not have: it can be the whole condition. if b then … is a fact about b: it is true in then, and anything else in else (false or null, since if takes the else branch for every value except true).

A boolean as the condition, and compared

Condition	`b` when true	`b` when not true
`not(b)`	`boolean = false`	`boolean = true \| Null`
`b`	`boolean = true`	`boolean = false \| Null`
`b = true`	`boolean = true`	`boolean = false \| Null`
`b = false`	`boolean = false`	`boolean = true \| Null`
`b != true`	`boolean = false \| Null`	`boolean = true`
`b != false`	`boolean = true \| Null`	`boolean = false`
`b = b2`	`boolean \| Null`	`boolean \| Null`
`b < true`	—	`boolean \| Null`
`b > false`	—	`boolean \| Null`
`true < b`	—	`boolean \| Null`
`b <= true`	—	`boolean \| Null`
`b instance of boolean`	`boolean`	`Null`

b alone is the same as b = true: true in then; in else the value is false or null.
b != true and b != false are true for null as well (null != true is true), so Null stays in then and is removed from else, where the comparison is certainly false.
b = b2 says little: b2 can be null, and two nulls are equal.
Booleans have no order. Table 55 of the specification lists no boolean, and what is outside the domain of an operation is null, so b < true is a type mismatch: null for every value, and never true. The then branch cannot be taken, and the else branch is taken for true and false as much as for null, so b is as it was there. (An earlier version left only Null, and if b < true then 1 else b was typed Null where the run gives true.)
<= and >= follow the same ordered-kind restriction (D-196). The specification also gives the formula e1 < e2 or e1 = e2, which would make true <= true true. The supported interpretation follows the domain table: all four operators are typed Null with a type_mismatch warning, including when the other operand is Any (true <= v). The then branch of b <= true is unreachable.
Booleans have no arithmetic either: + - * / ** and a negation are not defined for one, so b + 1 is a type mismatch, and b + v and v ** b are Null with a type_mismatch warning for every v, a name of type Any included (D-203; see null). A condition that contains one, b + v > 1, is never true.

With `and` and `or`

b and b2 is true only when both are, so each is true in then. It is not true when either is not, so in else neither is narrowed. b or b2 is the other way round: when it is not true, both are false or null.

Condition	`b` when true	`b` when not true
`b and b2`	`boolean = true`	`boolean \| Null`
`b or b2`	`boolean \| Null`	`boolean = false \| Null`

Condition	`b2` when true	`b2` when not true
`b and b2`	`boolean = true`	`boolean \| Null`

A boolean of any other type

A name of type Any, used as a condition or compared with a boolean, is narrowed to the booleans:

Condition	`v` when true	`v` when not true
`v`	`boolean = true`	`Any \| Null`
`v = true`	`boolean = true`	`Any except boolean = true \| Null`
`v = false`	`boolean = false`	`Any except boolean = false \| Null`

Explicit comparisons keep exclusions such as Any except boolean = true | Null. A bare v used as a condition currently leaves Any | Null in the not-true branch; that is a precision limit of this fact, not an absence of complement types (Any).

What the condition's own type does

Expression	Type	Warnings
`if b then b else true`	`boolean = true`	—
`if not(b) then b else true`	`boolean`	—
`if b < true then 1 else 2`	`number = 2`	`type_mismatch`, `decided_condition`
`if b < true then 1 else b`	`boolean \| Null`	`type_mismatch`, `decided_condition`
`if b <= true then 1 else 2`	`number = 2`	`type_mismatch`, `decided_condition`
`{ok: x > 5, r: if ok then x else 0}.r`	`number in 0, (5..max]`	—

not(b) is true where b is false, so in then b is boolean = false, and in else it is true or null (narrowing.md, the three outcomes). A boolean that was computed from a comparison (ok) is the value of the comparison, and a read of it as a condition says what the comparison says of x (narrowing.md).

Limits

There are none to speak of: the sets have two members. The cost of a long chain of and and or is that of the chain (limits).