Type narrowing

Narrowing is how the analyzer uses what a condition says. In if x > 5 then x else 0 the x that is returned is not the declared number | Null: the condition was true, so it is a number above 5. Every read of a name is analyzed under the facts available in its branch. Narrowing improves result bounds, supports warnings about fixed conditions, and lets the optimizer remove checks. It therefore has consequences for execution, even though the runtime does not apply the facts itself. The assessment states the contracts and the remaining audit work; the rules and tested examples below do not establish general soundness.

This page has the general rules. Each type has a page of its own with the conditions that narrow it and what they leave (the index), and overloaded functions says how narrowed arguments meet functions with several signatures. type-system.md explains the types that are narrowed, and architecture.md where the code sits.

Contents: 1 Vocabulary · 2 The names in the examples · 3 What gives a fact · 4 Then, else and null · 5 And and or · 6 Where facts apply · 7 What it changes · 8 What gives no fact · 9 Limits · 10 Correctness obligations and checks · 11 The code · 12 The pages · 13 Does it narrow as far as it can?

1. Vocabulary

• Subject. What a fact is about: a name (x), a path that starts at a name (p.age), a local, which is a parameter of a function, an iterator, or an entry of a context, identified by the depth of the context that binds it, so that a name bound again deeper takes no fact (D-193), and in the brackets of a filter the element (item) or one of its entries.
• Fact. A function from the type of a subject to the alternatives of it that are left. A fact only takes alternatives away or makes a set of values smaller. It must preserve every value the subject can have in that branch; shrinking alone does not establish this obligation. A fact that leaves nothing says that the branch cannot be taken: a read of the subject there keeps the type it had, since any type will do, and the if leaves the branch out of its type and says that it never runs (section 7, D-152, D-173).
• Branch. then is where the condition was true. else is where it was not: false, null, or a value that is no boolean, since if takes the else branch for anything but true (Table 50). That asymmetry is the source of most of what follows: the not-true branch is rarely as informative as the true one.

Facts compose by the logic around them, and they stack: a read inside a branch has the facts of every condition that encloses it, and the facts of the same subject are applied one after the other.

2. The names in the examples

The tables are checked against the analyzer using this scope (Feel.Sweep.scope/0). Expression rows compare the prepared root types (with default optimization) and warning codes; condition rows inspect the subject in the unoptimized branch IR. Constant folding can make a root type more precise. This is distinct from checking every possible runtime binding. A name has its declared type, with null added, as for every name that is bound from outside (x is number | Null); allowed values narrow the type of the name when the run enforces them (D-138), as in n. An allowed value is a unary test, which is a condition of ?, and narrows by the rules of these pages (D-161): ? * 2 < 100 as an allowed value narrows as x * 2 < 100 does in a condition.

A type is written as Feel.Type.Union.format/1 writes it: number in [0..150] | Null is a number from 0 to 150, or null; -max and max are the ends of decimal128; string except "a" is every string but one. Where a table says — for a branch, the branch cannot be taken.

The tables use the defaults analysis: :full and declarations: :enforce. The core tier keeps kind information but does not apply these set-valued facts. It preserves the same runtime values and diagnostics for supported settings; observable function signatures are captured independently of the extra full-tier precision. Preparation warnings can still describe different inferred bounds. :trust and :audit require full analysis.

Declaration stance also changes the assumptions behind the tables. :enforce_wide checks values without narrowing by allowed values. :trust and :audit use allowed values without repairing invalid bindings; the host must satisfy those assumptions. :report and :ignore do not narrow by allowed values, but still assume declared kinds. Non-null input declarations lose their null alternative only in the enforcing stances. See declarations and Feel.Analysis.Declarations for the full contract.

3. What gives a fact

A condition gives facts about the subjects it reads, in the shapes below, and nothing else does (section 8). Each is read for three outcomes of the condition, and not for two (5).

How a comparison narrows a kind is specific to that kind, and is described on its page. What they all have in common is the subject of the next section.

4. Then, else and null

null is what makes the two branches unequal. An ordering with a null operand is null, and null is not true; but null = null is true, and null != 5 is true (Table 50, D-04). So:

• When an ordering is true, the subject is not null, and is in the set of values for which it can be true. When it is not true, the subject can still be null, so the type keeps Null.
• x != 5 is true for null, so Null stays in then and drops out of else, where the comparison is certainly false.

• x = null and x != null are the guards. x = null is true only for null, and when it is not true the subject is not null: that is what turns number | Null into number in if x = null then 0 else x + 1.

• else uses the values for which the comparison is false only when it cannot be null: the other side is of one kind and never null. Otherwise every value remains. That is why x > y says less than x > 5:

y can be null, so x = y can be true for a null x, and x > y is read from the bounds of y's set: x is above its lowest value. v is Any, so the other side's kind is not known, and a number is all that x > v can say. The pages of the kinds go through the same questions for their sets. null.md has the whole matrix.

A value compared with itself is one value, and not two of the type (D-170): x = x is true for every value of FEEL, null included, and an ordering of a kind that has one is false (<, >) or true (<=, >=) and null where the value is null, since an ordering with a null is null. A kind without an order (b < b) is a mismatch as always, and Any is not known to be a value of FEEL.

An operand that has no order (a boolean, a list, a context, a range, a function) is null against anything for the four orderings, and so against a name of type Any (D-196): true < v and true <= v are Null with a type_mismatch warning, and if true < v then 1 else 2 is number = 2 with a decided_condition. null.md has the rows.

The same goes for an operand for which an arithmetic operator has no operation (D-203): a boolean, a list, a context, a range and a function have none of + - * / **, a string only +, a date, a time and a date and time + and -, a duration all but **, and a number all. true + v, [1] - v, s - v and d * v are Null with a type_mismatch warning for every v, and if true + v > 1 then 1 else 2 is number = 2 with a decided_condition; s + v is string | Null, d + v is date | Null and x + v is number | Null, the kinds that their pairs give (D-203), and -v is number | years and months duration | days and time duration | Null, the kinds that a negation has (D-207), as v - v is 0 of a number or a duration, or null. null.md has the rows.

5. And and or

The right operand is read knowing what the left said: the right of a and b is analyzed in the then facts of a, and the right of a or b in its else facts (D-194). So x != null and x > 5 is boolean, never null, and x = null or x > 5 is too.

A subject that only one side of an "either" narrows is not narrowed: in x > 5 or y > 3 the second may be the one that was true, so x is as it was.

Three outcomes. else is where a condition was not true, which is two cases that not, and and or tell apart: it was false, or it was unknown (null, or a value that is no boolean; not(5) is null, and so is 5 and true). The facts of a condition are asked for each of them (Narrowing.facts/2: :then, :false, :null, and :else for the two together), and a set of facts holds at least every state that has the outcome, so a shape that is not read says nothing for it. not(c) is true where c is false, false where c is true, and unknown where c is; its else is the other two. a and b is false where a is, or b is; unknown where a is and b is not false, or where a is true and b unknown. The right operand was read knowing what the left said (above), so what it says of the names the left narrowed holds only where the left is true, and the unknown cases of the left are all kept for them.

An operand that is never a boolean leaves one outcome out (D-170). The tables of the runtime distinguish true, false and "otherwise" (null, or a value of any other kind): a false decides a conjunction and a true a disjunction, and otherwise the result is null. So b and null is false or null and never true, and b or null is true or null and never false. A name of type Any may be a boolean, and the same holds for it.

6. Where facts apply

A fact applies to every read in the part of the expression that it holds for, and the part is:

• the branches of an if, and every condition inside them;
• the right operand of and and of or, and the upper bound of between, and the upper comparison of a range in an in, which are read knowing the first part (D-194);
• the brackets of a filter, for the elements it keeps (D-71);
• the body of a function that is called where it is written or through a key, which is analyzed again with the types of the arguments and the facts that hold at the call (D-193), once for the same ones (D-193);
• the locals: the body of a for, some or every, the entries of a context, the parameters of a function.
• the outputs of a rule of a decision table, for the entries of the rule: the rule matched, so each of its entries was satisfied by the input of its column, and an entry >= 18 of the input age is age >= 18 in its outputs (D-195). A not(...) entry is the outcome false of the tests (D-194), a - is the input values of its column if it has some, and the defaults and output values of the table are not under a rule. A table has no text, so there are no rows of it in the tables of these pages; test/feel/analysis/table_narrowing_test.exs and the sweep of scripts/sweep/tables.exs cover it.

A name that is bound to a condition remembers it (D-194 in decisions.md). ok above holds the value that x > 5 had, so if ok says of x what if x > 5 does, in each outcome: x is above 5 where ok is true, and ok is false or unknown where x is at most 5 or null. It holds for the entries of a context, for the entries that are names of one ({o: ok}), and for the parameter of a function written in the expression that is called at once, or through a key, with a condition (D-193). It is the facts of the condition as they were made where the name was bound, about the names of the scope and the paths from them; those about a local of the place of the call (for i in xs return f(i > 5)) are not about a local of the function, so they are left out. The nodes of the body of a function are those of its analysis for any argument, so the type of the call is narrower and a node in the body is not.

A name that is bound again shadows the fact. x in if x > 5 then (for x in xs return x) else null is the iterator, not the x the condition read, and a fact is about the one that was read. A fact about a variable is not about a local of the same name, and a local is distinguished from another of the same name by the depth of its context.

Rule-output narrowing and table proofs answer different questions. The former analyzes an output under the assumption that its row matched. Feel.Rules separately asks about coverage, overlap and FIRST reachability using possible-input upper bounds and certain-input lower bounds. DMN keeps named type definitions during proof preparation, but cells reading model/local values or filter fields stay unknown when their enclosing scope cannot be preserved. Wildcards use effective inputValues; explicit entries use their own tests. These queries produce diagnostics, not a license to eliminate a rule's outputs. See the table-proof contract.

7. What it changes

The type of every read in the part the fact holds for. That is most of it, and the pages of the kinds have the details.

The type of the if. Feel.Analysis.Inference.reachable/1 says, from the type of the condition, whether the then branch can be taken (some alternative can be true) and whether the else can (unless the condition is boolean = true for sure). The type of the if is the union of the types of the branches that can be taken, and the warnings of a branch that cannot are not reported.

A branch whose facts leave a name nothing is a branch that cannot be taken either (D-152, D-194). It is found in two ways, and both ask the same Refinement.narrowed/2 of the facts of the conditions around the branch and of its own, for the type that a read gives the name:

• By a read (D-152). The facts are applied where a name is read, and a read that finds they leave the name no value tells the if whose branch it is in (count(v) = 1 and v = [], which nothing makes true, since a list of one element is not [], and which the type of the condition does not say for a v of type Any; an ordering of what has no order, v < true, is Null by its type, D-196, and decided without any help from the facts). The branch is left out of the type of the if and its warnings are not reported, as for a condition that cannot be true, and the if says that the branch never runs (an unreachable_branch warning, below). It costs nothing: the read applies the fact already. Only a branch that reads such a name is found this way.
• By a call (D-194). A condition that compares a call of a rounding function, of exp or of log (floor(x) = 2.5) is the one place where the facts know what the type of the condition does not: the type of the call is a hull of its results, floor(x) = 2.5 is undecided for it, and no number gives such a result. The facts are applied to the name that the call reads, whether or not anything in the branch reads it (if floor(x) = 2.5 then 5 else 7 is number = 7). It is asked for a comparison on either side, through an operation or an abs, sqrt or modulo (floor(x) + 1 = 3.5), for the value of a between and the subject of an in, and for the operands of an and or an or; for the then branch, since the facts of a call are those of its then; and for a name, a local or the element of a filter whose type has no Any and no negation in it. What the fact leaves of the type is kept for the reads of the branch, so a branch that reads the name applies the fact once.

Nothing else is asked of a branch that reads none of the names its facts are about, and it is in the type, with no warning: applying the facts at every if costs 20 to 65 % of preparing a chain of else if on a number at least (a number given, no look-up of the name: one x = 1 is 550 to 850 reductions, and a term of the chain is analyzed in 2,300 to 5,000), 25 to 185 % with the type of the name looked up, and 80 to 470 % applied to Any, which does not find the floor condition at all; a chain of v instance of … that returns constants is twice the cost of preparing it. The sets of the types decide a comparison of a name, of an operation on names or of an abs, sqrt or modulo as the facts do (an image of an interval is an interval), and of 6,702 conditions of those and of the calls against constants, the facts find 196 that the type of the condition does not, every one a rounding function, exp or log (D-194 has the measure). A conditional whose two branches are both found out is not taken in the branch of the one around it.

A decided_condition warning, when a condition that reads a name still has one outcome: always true (the else never runs), or never true (the then never runs). The same for an operand of and or or (it can be left out, or it decides the operation) and for a unary test that no input satisfies. A condition of constants is how a branch is switched off (if true) and is not reported, nor is a branch that cannot run itself.

An unreachable_branch warning (D-173), for a branch that the type of the condition leaves and in which a read found that the facts leave its name no value: the analogue of the redundant clause that Elixir reports. Its span is the branch, its message says which branch and the name that was read, and its details have branch (:then or :else) and name. It is a warning and not an info for the reason a decided_condition is one: a condition that no value of a name satisfies, or that every value satisfies, is most often a mistake, and an :info is for what was done on a value's behalf. It is found when the expression is prepared and changes no result. The facts that the branch has are those of its own condition and of the conditions around it, so the message does not blame the condition of the if it is reported for. It is not reported:

• for a branch that reads none of the names its facts are about, unless the condition compares a call of a rounding function, exp or log (above): if count(v) = 1 and v = [] then 5 else 7 is number in 5, 7, and so is if floor(v) = 2.5 then 5 else 7 for a v of type Any; nor for the facts of a path such as p.age: neither a read of the path nor the call finds that they leave it nothing (if floor(p.age) = 2.5 then p.age else 7 is number | Null);

• for a constant condition (if true then x else 7), nor for a branch that the type of the condition rules out, which a decided_condition has already reported for the condition, so the branch is not reported twice;
• for a conditional both of whose branches are found out, nor for one in a branch that is not taken: the place that cannot be reached is the branch of the conditional around it, which says so once;
• for a conditional in the right operand of an and or an or, or in the upper bound of a between, that has facts of the left one: the operand is read under facts that hold only where it decides the operation, and is run all the same (D-53), so what the facts rule out is run as well. The branch is out of the type as before; it is not reported as unreachable. (A branch that is out because of the condition of its own if alone is not reported either, in these places.)
• for the body of a function that is analyzed again for a call: the facts of the call are not the function's, and the warnings are those of the function as it is written (D-193). (function(n) if floor(n) = 2.5 then n else 7)(x) is number = 7 with no warning, and with n: number in the parameter the function reports it itself.

if n >= 0 then 1 else 2 is not decided because n can be null, and then the condition is null. That is the reason a warning is as exact as the types: x < 0 or x >= 0 is true or null, not true.

The optimizer. It reads the types: a check that a type already settles (a conversion of the result, the allowed values of a result) is dropped, and a condition whose type is a constant is folded. A narrowing that was unsound would make it drop a check that was needed, which is why section 10 matters (type-system.md, 5.6 and 6).

8. What gives no fact

The facts are read from a closed set of shapes (section 3). Anything else says nothing about its subjects, and a subject keeps the type it had:

• Built-in functions as conditions on their own: includes(r, x), contains, starts with, matches, with no comparison. (count(xs) compared with a whole number is a fact about xs, D-194, and a call compared with a value says what it does of its arguments, D-170; the else of a call is read where the call cannot be null for the argument: an operation, a number function and string length, not another built-in.) not(c) is read (5).
• A boolean that was computed, where its facts are not kept. A name that is bound to a condition remembers it (section 6), and a name that is bound to anything else (ok: f(x) > 5 with a call that gives no fact, a value that came from a list) does not.
• A comparison of two expressions (x + y > 5 narrows x to a non-null number, but no set: y is unknown).
• A condition on an indexed element (xs[1] > 0), a range held as a value (x in r), or a quantifier (some i in xs satisfies i > 5) does not generally propagate a fact back to xs or the range's endpoints. Selected comparisons of count(xs) with whole numbers do narrow empty versus non-empty lists; they do not encode arbitrary lengths (list).

• An unsupported or indeterminate exclusion from Any. Scalar comparisons can keep the complement of their certainly-true set: v > 5 leaves Any except number in (5..max] | Null when not true. If the other side is unknown, or no useful certainty bound can be constructed, the not-true branch may remain Any | Null (any.md).

• A function value: instance of function<...> removes null, and takes the function types of a function out of the type or leaves them (an overload, D-171), and a call finds what the test says of the arguments it takes (function.md).

9. Limits

The intended policy for possible-value facts is to widen when a representation budget is exhausted. The limits below describe that policy. Negation, function parameters and certain-input rule sets require different directions: nested exclusions are kept, function projection checks variance, and certain numeric/string sets use lower bounds rather than these ordinary upper-bound policies. NumberSet complement and inclusion are exact over their supplied sets. The assessment states the contracts and remaining proof obligations.

A property walk that finishes still stores its amounts in a number set, so more than 16 intervals become the hull in the first row. dds.minutes = 30 does that. The walk limits above are where the walk refuses and the subject stays as it was. Past the date-arithmetic and month limits, the result is one interval that holds every piece the walk would have built, and more.

The 16 pieces are why x != 1 and x != 2 and … narrows a number until the sixteenth hole: with x != 15 as the last, the set is [-max..1), (1..2), …, (15..max], sixteen intervals. One more, and the seventeen intervals become number | Null, and each fact after that cuts the hull again (x != 17 gives [-max..17), (17..max]). For this positive numeric bound, taking the hull keeps possible values and loses precision. The same operation cannot be reused as a lower bound for certainty. Exact complement preserves the meaning of the supplied set, but cannot recover gaps already filled by an earlier hull.

For certain string inputs of decision rules, the 64-point/exclusion check follows bulk union or intersection of the entry list. String intervals do not count toward that cap. Keeping the bulk operations avoids repeatedly rebuilding a growing interval set in positive and negated lists.

max_narrowing_facts counts facts that cannot be answered from the type the subject is read at, and have to be applied to it at each read: the work for a subject grows with the square of their number. A thousand facts that the type answers (x = "a" or x = "b" or …) cost no more than one. The condition that went over is named:

p.age > 1 and 1 / p.age > 0 and p.age > 2 and 1 / p.age > 0 and …        (20 pairs, max_narrowing_facts: 5)
→ {:error, %Feel.Error{kind: :limit, code: :too_many_facts}}
  the conditions say too much about "p.age": 6 facts about it have to be applied to its type, and at most 5 are allowed

With the default of 256 the same 20 pairs are prepared. The example uses a path: the same chain about a plain name (x > 1 and 1 / x > 0 and …) is answered from the type of the name, and was prepared without reaching the limit with 200 pairs.

10. Correctness obligations and checks

The documentation tables themselves are executable checks. From the umbrella root:

mix test apps/feel/test/feel/sweep/docs_test.exs
MIX_ENV=test mix do --app feel cmd mix run scripts/sweep/check_docs.exs

Both compare the recognized tables in this page and narrowing/*.md with current analysis, including warning codes. They do not execute every prose example, compare warning wording, or prove that a bound contains all runtime results. The sweep guide explains the separate generated runtime and tier checks.

A narrowed type must contain every value that its subject can have where it is read, under the stated assumptions. Unknown conditions should contribute no fact; bounded approximations must preserve the required inclusion direction. The optimizer may otherwise remove a check the run needs.

These are obligations, not properties established by the current implementation. The contracts of the assessment show why checking each rule in isolation or widening positive result bounds does not establish correctness of their composition.

What looks for a violation:

Precision checks also require useful narrowing in selected cases. Neither precision checks nor a finite soundness grid prove the universal obligation; shared membership code can hide a semantic defect.

11. The code

The current decision record groups the relevant choices: D-194 for condition outcomes, D-122 for inverse arithmetic, D-193 for binding summaries, D-173 for unreachable code, and D-154 for budgets.

12. The pages

13. Does it narrow as far as it can?

Section 10 is about one half of the question: a narrowed type has to hold every value that the subject can have. The other half is that it should hold nothing else, and nothing in the tests of section 10 asks about it. The construct suite (test/feel/construct_suite, test/support/construct_suite) does.

What a case is. A catalog (Feel.ConstructSuite.Catalog.*) is a list of expressions, each an example of a construct, with the IR that the analyzer makes of it as text, one node per line with its type (Feel.ConstructSuite.IRText):

if :: number in 0, (5..max]
  compare gt :: boolean | Null
    var x :: number | Null
    const :: number = 5
  var x :: number in (5..max]
  const :: number = 0

The catalogs cover every kind of node of the syntax tree and every operator (expressions), the nodes that the declarations of the scope put around an expression (declarations), lists of unary tests, a function of an extension, the conditions of section 3 for each kind of subject, in the then and in the else branch (conditions, a case is if C then S else S), and the places of section 6, what shadows a fact, what gives none, and the limits of section 9 (positions). coverage_test.exs reads the tables of Feel.AST and Feel.IR and fails for a kind of node that has no case, so that a new construct cannot be added without one. A test holds each case to its IR and its warnings, so a change of the analysis shows as the diff of the IR. From the umbrella root, MIX_ENV=test mix do --app feel cmd mix run scripts/construct_suite.exs --check reports changed snapshots; omitting --check rewrites them and requires reviewing the diff.

How "as far as it can" is asked. Feel.ConstructSuite.Oracle runs the expression on a grid: the product of the values of its names, each name with the constants of the expression and the edges of its allowed values, and the number below and above each (Pools), the way the sweeps do, and observes the values that reach each node (Feel.Backend.Interpreter.run_monitored/4, the monitor of Feel.Paranoid), each node by itself and not by its text: the two comparisons of the range in n in [20..30] are one span, and so are a node of the verification of a declared value and one of the expression. A node is wider than the runs when its type holds something that no run brings to it:

The grid is not all values, so a witness is a lead and not a proof: a value that the pools lack makes a type look wider than it is. Every gap in the catalogs has been examined, and a case can add values (extra:). The suite does not judge a node that is not a condition or a read, such as the result of an arithmetic operation; a case can say what such a node should be (ideal:) when it is known.

Gaps. A gap is a node that is wider than the runs, with the reason, in the case (gaps:). The test of the case fails for a gap that is not listed and for one that is closed, so the list is always the list that the runs find. Each case that has gaps has a second test, tagged :gap and left out of mix test, that says what the narrowing should do (no node wider than the runs, the nodes of ideal: as they should be):

mix test apps/feel/test/feel/construct_suite --include gap

The current gaps: and ideal: entries in the construct catalogs are the maintained precision backlog. The tagged run above intentionally exposes cases whose ideal bounds are not yet inferred; it is separate from the ordinary passing regression suite. Old inventories included direct-call specialization and impossible floor comparisons that later repairs can handle, so they should not be read as a current list of missing features. A gap on a finite grid still needs semantic review before being treated as a valid optimization opportunity.

This catalog is not an inventory of every precision gap. Repeated-read rules cover selected operators (D-170, D-207), but duration self-addition still combines independent intervals and can admit sums of different possible values. See the month-duration and second-duration limits and the backlog.