Products combine components; tagged sums represent alternatives with distinct payloads.
By the end: reason about exhaustiveness and unreachable patterns in a finite variant model.
A pair of booleans has four values: false/false, false/true, true/false, true/true. It contains both components. Option<Bool> instead has three values: None, Some(false), and Some(true). A tagged sum selects one constructor, and that constructor determines its payload.
The tag prevents confusing absence with a false payload. Some(false) is still present. This is more precise than using an undocumented sentinel that could also be an ordinary value. The lesson’s finite case model is separate from the core inference language, which supports pairs but not variants.
A constructor is a named way to form a value. In Option<Bool>, None forms a value without a payload, while Some takes one boolean payload. A payload is the information stored inside the chosen alternative. This notation describes the separate finite coverage lab, not an extension accepted by the earlier core inference engine. Its complete input space is exactly None, Some(false), and Some(true). None and Some are constructor names, but only the first is already a complete value. Listing names alone can therefore underestimate how many cases a match must cover.
For a product, each position must receive a value. Bool has two choices, so Bool × Bool has two choices for the first position and, for each, two for the second. The four complete values are the ordered pairs false/false, false/true, true/false, and true/true. Order matters because a program can use the first and second components differently. The middle two pairs are distinct. Multiplication counts all combinations under the assumption that either boolean is allowed independently in either position.
| Bool × Bool | First / second |
|---|---|
| Pair 1 | false / false |
| Pair 2 | false / true |
| Pair 3 | true / false |
| Pair 4 | true / true |
| Option<Bool> | Payload |
|---|---|
| None | No payload |
| Some(false) | false |
| Some(true) | true |
For a tagged sum, choose an alternative, then fill only that alternative's payload positions. None contributes one value, not zero: absence itself is a legitimate case. Some contributes two because its payload is Bool. Adding those contributions gives three complete values. The tags make the alternatives distinct even if their payload representations could otherwise be confused. This is why a false payload cannot stand for absence. A caller may need to distinguish a present answer of false from having no answer, and Option<Bool> preserves that difference explicitly in its value structure.
Compare the product Bool × Bool with this sum as encodings of an optional yes-or-no answer. If the product's first boolean means present and its second means answer, both false/false and false/true claim absence. You must decide whether both are allowed and, if so, how to treat the irrelevant second component. The type alone does not remove that ambiguity. The option encoding has one absent value and exactly two present values. It avoids inventing two encodings for the same absent state.
These counts extend to nested finite types when every component's allowed values are known. As a separate paper example, Option<Bool × Bool> has one absent case plus four present pair payloads, giving five. By contrast, Option<Bool> × Bool has three choices in its first position and two in its second, giving six. The grouping changes what a complete value contains. The coverage lab cannot select either type; it remains fixed at Option<Bool>. The paper calculation shows how to derive a case space rather than assuming every occurrence of Option and Bool contributes in the same way.
| Paper type | Complete construction choices | Total values |
|---|---|---|
| Option<Bool × Bool> | None, or Some of one of four ordered pairs | 1 + 4 = 5 |
| Option<Bool> × Bool | One of three option values, together with one of two booleans | 3 × 2 = 6 |
Exact counting is useful only after stating the type's restrictions. If a payload were an arbitrary integer, writing down a handful of examples would not enumerate its whole space. If a language allowed additional constructors later, today's list would no longer be complete. Here finiteness and the fixed three-value definition let us check coverage by direct enumeration. The next step is to assign each of these values to its first matching pattern. That is a separate calculation from counting constructors or deciding what result a branch should compute after it receives a value.
Matching None covers the no-payload case. Some(_) covers both boolean payloads; Some(true) covers only one. An exhaustive match covers every value of the declared input type. Knowing the outer tag alone does not guarantee that nested payload patterns cover all possibilities.
Pattern order matters. A wildcard first consumes all remaining values, so later None or Some branches are unreachable. The lab reports newly covered cases for each branch, not merely a union that ignores ordering. Real languages may also need rules for guards, open variants, and recursive payloads.
A pattern describes which values a branch can receive. The literal pattern Some(true) accepts one complete value. Some(_) accepts either boolean inside Some; its underscore means that this payload need not be distinguished. The standalone pattern _ accepts any of the three complete values, including None. These two uses of an underscore have different scopes. One ignores a field after requiring the Some constructor; the other ignores the entire value. None requires the no-payload constructor. There are exactly five supported patterns in the lab, with no conditions attached to them.
Matching is ordered and uses the first branch whose pattern accepts the value. To calculate a branch's contribution, start with the cases its pattern matches in isolation, then remove all cases already handled earlier. Call the result its newly covered set. Begin with no handled cases. After each branch, add its matching cases to the handled set. Braces enumerate members, and ∅ means an empty set. A branch is unreachable in this finite model when its newly covered set is empty. The complete list is exhaustive when no input case remains outside the handled set.
| Branch in order | Matches in isolation | Newly covered |
|---|---|---|
| Some(true) | {Some(true)} | {Some(true)} |
| Some(_) | {Some(false), Some(true)} | {Some(false)} |
| None | {None} | {None} |
| Missing after all branches | Complete space minus handled cases | ∅ |
For the paper branch order Some(true), Some(_), None, the first branch newly covers {Some(true)}. The second matches {Some(false), Some(true)} in isolation, but the true case has already been handled. Its new contribution is therefore {Some(false)}. The final None branch contributes {None}. All three branches are reachable and the final missing set is ∅. Notice that overlapping patterns need not be a mistake. A specific true case followed by a general Some case deliberately assigns different behavior to true while retaining a fallback for other present payloads.
Reverse the first two branches to get Some(_), Some(true), None. The first now receives both present values. The second still matches Some(true) in isolation, but that value never reaches it, so its newly covered set is ∅. The None branch remains reachable and the list remains exhaustive. The union of all pattern matches is unchanged between these two orders. A union can answer whether every value has some accepting branch, but cannot answer which branch handles a value or whether a particular branch contributes anything after earlier branches have been considered.
Exhaustiveness and reachability therefore answer different questions. None followed by Some(true) has two reachable branches yet misses Some(false). A standalone wildcard followed by None has no missing cases, yet its second branch is unreachable. Neither property establishes that the branches return useful answers. A program can handle every case and still produce an incorrect result for every one. The lab computes assignment of input cases to patterns, not branch bodies or return types. Its coverage result should not be read as evaluation evidence or as acceptance by the earlier equality-based inference engine.
| Ordered patterns | Missing values | Unreachable branches |
|---|---|---|
| None; Some(true) | {Some(false)} | No branches |
| _; None | ∅ | Second branch, None |
| Some(_); Some(true); None | ∅ | Second branch, Some(true) |
| Some(true); Some(_); None | ∅ | No branches |
Narrowing describes the extra knowledge available after a test or pattern selects one alternative. Entering a Some(_) branch establishes that a boolean payload exists, but does not establish whether it is true. Entering Some(true) establishes both the outer constructor and that literal payload. Entering None provides no boolean payload to read. In a language with branch bodies, these facts justify different operations inside different branches. Our finite lab displays the case assignments without executing such bodies. Keeping the remaining cases explicit explains why a later branch can be impossible even though its pattern describes a valid value.
| Branch in order | Newly covered | Unreachable? |
|---|---|---|
| None | {None} | No |
| Some(true) | {Some(true)} | No |
Exhaustive: No. Missing: {Some(false)}.
| Type | Distinct values |
|---|---|
| Bool × Bool | Four ordered pairs |
| Option<Bool> | None; Some(false); Some(true) |
Start with A payload hole. Its ordered branches are None and Some(true), so the missing display should identify Some(false). Both branches are reachable. Select Append Some(_) to add a third branch. It matches two values in isolation but contributes only the still-missing false payload here. The result becomes exhaustive. This sequence shows why the lab reports newly covered values rather than just the values named by each pattern. Adding a broad pattern after a specific one can complete coverage without making the earlier specific branch unreachable or changing which branch receives true.
Now remove Some(true). Removal keeps the order of the other branches, leaving None followed by Some(_). The list remains exhaustive, but the second branch now contributes both present values. Append Some(true) again. Appending places it last, after Some(_), so its contribution is empty. You have recovered the same three pattern names as before, yet not the same order or assignment. Removing a pattern and appending it again is an actual way to change its position, but that operation can change whether it is reachable.
| Action | Resulting order | Who receives Some(true)? |
|---|---|---|
| Select A payload hole | None; Some(true) | Second branch |
| Append Some(_) | None; Some(true); Some(_) | Second branch |
| Remove Some(true) | None; Some(_) | Second branch, now Some(_) |
| Append Some(true) | None; Some(_); Some(true) | Second branch; third is unreachable |
Choose Wildcard first to replace the whole list with _, None, Some(_). The first branch takes all three values immediately. The other two report ∅ and are unreachable. Remove the standalone _ and the remaining order is None, Some(_), with both branches useful. Append _ again. It is now last and contributes nothing because the preceding branches are already exhaustive. The wildcard's meaning did not change. What changed was the set of cases still available when execution would reach that position. The displayed per-branch evidence makes that distinction visible without a runtime animation.
Compare None only with Both constructors through the preset buttons. The first leaves both present values missing. The second uses None and Some(_), so it covers all three. Then select A payload hole again. Although this list mentions both constructor names, its Some pattern accepts only true. The missing false case is evidence that constructor coverage and value coverage differ. Each preset replaces the complete ordered list rather than adding to your previous edits, so compare its displayed rows from the start.
The buttons allow at most one copy of each supported pattern in the visible list. Clicking a present pattern removes it; clicking an absent one appends it. Although the underlying helper can analyze duplicates within its eight-branch bound, these controls do not create repeated identical branches. The overlap examples above do not need duplicates: Some(_) and Some(true) already overlap. That distinction matters when reasoning from an interface restriction. A duplicate would be redundant after its first identical predecessor, but the lab's unreachable branches usually demonstrate containment by a broader earlier pattern instead.
| State | Ordered patterns | Wildcard contribution |
|---|---|---|
| Wildcard first preset | _; None; Some(_) | {None, Some(false), Some(true)} |
| Remove _ | None; Some(_) | No wildcard branch |
| Append _ | None; Some(_); _ | ∅ |
The two value-space panels provide a check on your reasoning. The complete space always has the same three values; editing patterns changes which are marked covered on the other side. A missing set of ∅ means every declared input value has a receiving branch. It is not the None constructor, and it does not mean the match has no inputs. Likewise a newly covered set of ∅ belongs to one branch position, not necessarily to the whole list. Read each empty-set display with its scope before deciding whether you have found successful coverage or an unreachable branch.
TypeScript discriminated unions and never checks can report an unhandled declared variant. That does not validate untrusted JSON, nor does a default branch prove the returned result is correct. The type declaration must still match the values that reach the code.
Adding a variant changes the coverage obligation. A compiler error can reveal every place that needs a new case. A wildcard may prevent that reminder by accepting future cases automatically. Decide whether that behavior is intended rather than treating every wildcard as inherently good or bad.
Coverage checking starts from a declared case space. It does not establish that every external value belongs to that space. Suppose a separate application expects an object encoding None or Some with a boolean payload. Receiving text that says Some with a numeric payload would violate that expectation before the match begins. A declaration alone does not inspect the received data. The earlier JSON boundary lesson illustrated this distinction with name and age. This lab does not supply an option validator, read JSON, or check network messages. It reasons only about its fixed three valid values.
TypeScript's discriminated unions illustrate a related static mechanism. A discriminant is a shared field whose literal value identifies an alternative, such as a kind field distinguishing a circle from a square. After checking that field, the checker can narrow the alternatives and permit fields that belong to the selected one. This is an analogy to selecting Some before using its payload, not a claim that our five-pattern lab implements TypeScript. Representation details and checking rules belong to the chosen language. Our direct case enumeration needs no host-language narrowing implementation to compute its result.
| Incoming representation claim | Belongs to Option<Bool>? | Coverage obligation |
|---|---|---|
| None | Yes, absent alternative | Must have a receiving branch |
| Some with false payload | Yes, present boolean | Must have a receiving branch |
| Some with numeric payload | No, payload is not Bool | Outside this declared case space |
| Unrecognized constructor name | No | Outside this declared case space |
An exhaustiveness check can also expose an unhandled declared alternative. TypeScript uses the type never to represent a point where narrowing has left no possible member of the declared union. A check that requires the remaining value to have type never can fail if a newly added member still reaches that point. This is a static obligation, not a way to turn an unexpected runtime value into an impossible event. If external data does not satisfy the declaration, the assumptions behind the narrowing argument were never established. Coverage and validation have different starting evidence.
Consider a separate paper revision that adds a third constructor named Unknown, with no payload, to our option-like type. None and Some are the two original constructors. Some(false) and Some(true) are different values of the same constructor, so Unknown adds a fourth value. This is not a control in the fixed lab. An old explicit list None, Some(false), Some(true) now misses Unknown. That failure usefully identifies a new decision the program must make. An old list None, Some(_) also misses it, because a payload wildcard still requires Some. An old list None, Some(_), _ receives Unknown in its last branch automatically. Whether that default behavior is acceptable depends on what Unknown means and what the branch actually does.
A wildcard therefore makes a trade-off visible. It can deliberately preserve fallback behavior for alternatives the author does not want to distinguish. It can also hide a missing case-specific decision when the type grows. The current lab has no future constructors, so its exhaustive result cannot choose that policy for an evolving application. In the four-case paper revision, compare which branch receives Unknown rather than merely asking whether the match still compiles in some unspecified language. Explicit case assignments reveal both the coverage benefit and the loss of a reminder to handle the new alternative separately.
| Old ordered patterns | Original three values | New Unknown value |
|---|---|---|
| None; Some(false); Some(true) | All handled | Missing |
| None; Some(_) | All handled | Missing |
| None; Some(_); _ | All handled; last branch unreachable | Received by last branch |
Transfer the finite reasoning by separating the obligations. Define the legal values first, retaining each constructor's payload possibilities. For each branch, determine its matching set and subtract all earlier handled values. Check the final missing set for exhaustiveness and each new set for reachability. Then assess the branch results against the application's intended behavior, which is outside this lab. Finally ask how incoming values earn membership in the declared type and how later type changes update the obligation. This separation avoids treating one complete pattern list as proof of validation, correct outputs, or compatibility with every future version.
A match handles None and Some(true). Is it exhaustive for Option<Bool>?
List all three values, not just the two constructor names.
| Value | Covered? |
|---|---|
| None | Yes |
| Some(true) | Yes |
| Some(false) | No |
No. Some(false) remains uncovered. Replace the literal pattern with Some(_) if both payloads should use one branch, or add a separate false branch if behavior differs.
For branches _, None, Some(_), which branches can be reached?
The first matching branch handles a value.
| Branch in order | New cases |
|---|---|
| _ | {None, Some(false), Some(true)} |
| None | No values |
| Some(_) | No values |
Only the first branch contributes cases. It matches all three values, leaving nothing for None or Some(_). The match is exhaustive but has two unreachable branches. Exhaustiveness and usefulness are separate checks.
Selected reference passages support the definitions and algorithms below. The examples, explanations, and implementations are original. Terminology and assumptions are stated within each lesson; source review is not an independent audit of this course. Optional links are not runtime dependencies.
Selected discriminated-union, never, and exhaustiveness examples. Our finite Option<Bool> coverage model is not a TypeScript compiler.