Narrowing a number

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

A number alternative of a union is the bare kind, every number, or {:number, set}: a Feel.Type.NumberSet, a list of intervals of decimals within decimal128 (-max to max, where max is 9.999…E+6144), each end open or closed. The comparisons below illustrate the intended sets within the representation budget. Caps and composition have known limitations. Null is a member of the union in its own right (null.md).

Comparisons with a value

The six comparisons, on either side of the subject. 5 < x is x > 5. The then branch is where the comparison can be true; the else branch is where it can be false, and Null, since an ordering of null is not true (the rule).

x != 5 keeps Null when it is true because null != 5 is true, and leaves exactly 5 when it is not.

between and in

x between a and b is x >= a and x <= b (D-69). x in tests is true when one of its tests is true, so the facts of the tests are joined, as or does; it is not true when none is, so they are met, as and does (D-194). A test that is a plain value rather than a comparison, such as a range held in a name, says nothing.

The last row is a range held in a name: it is a value, and the test cannot be read until run time.

The type of between is that of the same range in an in (D-170): the upper comparison is typed for the case where the lower one is true, with the value as the facts of that comparison leave it, and for the case where it is not (the value null, or below the lower bound), as the range of an in is (D-194). An n in [0..10] that may be null is true or null in both. A between reads its value once and has one upper bound; an upper bound that reads a name that the lower comparison narrows (n between 0 and n + 20) is read again in the case where the lower comparison is not true, if it is small (D-170).

An and is typed once, from the facts of its left operand (D-194), since a general right operand is not cheap to type twice. Its first link is typed for each case of the left operand as well (D-170) when the right operand is small, reads a name that the left one narrows, and the left one is not an and or or: the right operand is read again in the case where the left one is not true. A chain a and b and c is typed from the facts of the left operands only after its first link, since reading the right operand again under all of them at each link would make the chain quadratic (D-194).

An in of a list (x in [1, 2, 3]) is list contains, which is true or false for every input, null included (UnaryTests.member/3), so it is never null (D-170). A range held in a name, or a value of another kind, is equality or containment with the input, which can be null.

A number with allowed values

A name with allowed values starts from its set (n is number in [0..10] | Null), so a comparison cuts it, and a branch that the set rules out cannot be taken. The warning for such a condition is in section 7.

n >= 0 is true for every number of the set, so only null is left when it is not true.

The other side is not a constant

The other side is read as the set of numbers it can be, and the subject is cut by its bounds. Where it can be null or its kind is not known, the else branch learns nothing, because the comparison may have been null.

x > n leaves everything above the lowest possible n. x = y is true when both are null. v is Any: the comparison is true only for a number, so x is not null, and nothing else is known.

Operations in the comparison

An arithmetic operation, or a negation, is null when an operand is null or of a kind it does not take. So when x + 1 > 5 is true, x is not null and is a number. And the result is in the set that the comparison allows, so the operands are the numbers that give such a result with some value of the other operand: the preimage (Feel.Analysis.Preimage, D-122). An operand that is itself an operation is read in turn.

• The else branch holds the operands that make the comparison false and those that make the operation null. The branch where the comparison is not true is taken when it is false and when the operation is null. An operand is in it if the result can be one for which the comparison is false (the preimage of those results: x + 1 > 5 is false for a sum up to 5, so x up to 4), or if the operation can be null for it. For the second case the analysis asks whether the operation can be null for the operand at all (x + 1 and -x cannot: the sum rounds back to the largest number), and if it can, which numbers make it so (Feel.Analysis.Failure): a result too large to represent (x * 2 for an x from half the largest number on), a result too small to represent (x / 2 for an x below 2E-6143, where the quotient needs digits below the smallest unit), a divisor of zero or near it (1 / y), and for a date, the end of the calendar. The set is an outer approximation: it contains those numbers and some others. An operand with allowed values that the operation cannot leave is cut to the results that make it false and no more (the table below), and where the other operand can be null or is not known, the operation can be null for every x, so the else says nothing of it (x * y > 10). null is in else unless a comparison of null is true (null != 5 is), and so are the numbers that make the operation null: x * 2 != 10 is true for them, and they are not in its else.
• A set needs a set on the other side. x + y > 5 has an unknown y, so x is a number and no more.
• The result is rounded to 34 digits, so a bound the result may be (>= 5, = 5) is widened by half a unit of the last digit before the preimage is taken, and then brought back in to the first number of 34 digits. x + 1 > 5 has an open bound that the rounding keeps in order, and is exact.
• `is not inverted.**x ** 2 < 4only saysx` is a non-null number.
• The same subject cannot be answered from its type when it is read in an operation (1 / x > 0 leaves a set as a whole), which is what max_narrowing_facts counts (limits).

One value read twice

A name that is read twice is one value, not two numbers of its type (D-170). x - x is 0 for every x, and Null where x can be: the pair x = 3, y = -5 of x - y is not one of the values of x - x. The same holds for a member of a name (p.age - p.age) and for a local (for i in 1..3 return i - i); two reads that are not the same read are two values (x - (x + 0), p.age - ps[1].age). Here k is number!, n is in [0..10], and age in [0..150].

• x - x has the Null of x and no Null of its own: k - k is 0.
• x / x is 1 for every x that is not 0, and null for 0. The Null of k / k comes from the zero, and that is the reason it gives (operand_near_zero: allowed values that keep k away from zero rule it out); a large k is not a reason, and neither is a quotient that is too small to represent. The Null of age / age is that of age, which can be null.
• x * x is never below 0, and the squares of the intervals of a set are not mixed: x in [-4..-2], [2..4] has the squares [4..16], where two numbers of it have [-16..-4], [4..16]. It can be null for a number as near zero as 1E-6176 (the square is too small to represent), unless the name has a grain (D-161).
• x + x is 2x: the numbers of a set that has a gap in it are not added to each other.
• Durations and dates: a non-null dd - dd, d - d, tm - tm or dt - dt is PT0S. dd / dd is 1 for a nonzero non-null duration, and null for zero or null. Month-duration self-division also has numeric-conversion limits (years and months duration).
• age - 1 - age is not one value: the first age is read in age - 1.
• The core tier (analysis: :core) keeps the kinds and does not use it.

instance of

x instance of T is false for null, and never null. In then the type is what lies in both; in else the alternatives wholly within T are removed, and Null stays. For a number, instance of number leaves only Null in else.

Limits

• A set of more than 16 intervals is replaced by the one interval that holds them all, and the next fact cuts from that.
• Intervals that touch merge ([0..5) and [5..9] are [0..9]); [0..5) and (5..9] do not, since 5 is in neither.
• The ends of a result are always included, which can only make a set larger.
• A number outside decimal128 is not a FEEL number: a bound beyond it is taken as the end of the range.

See also: string, null, Any; type-system.md, 3.3.