Narrowing a name of any type

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

A name whose type is not known (a name of type Any, or one that the scope does not have, which is looked up when the expression runs) has the type Any | Null. Any in a union is every value that is not null, so the type is "any value" and a condition is the only way to say more. Any is the union of the kinds of value (Feel.Type.Union.tops/0, D-39): a boolean, a number, a string, a date, a time, a date and time, the two durations, a list, a range, a context, a function, and what is not a value of FEEL at all (a term that the host binds, which the run treats as a value of an unknown kind). A condition takes kinds out of it, and what is left is written Any except number.

A fact narrows Any kind by kind: to the kinds that the condition can be true for, each with the set the condition leaves of it (Feel.Analysis.TestSets, D-194). A comparison of v with a value of a known kind is true or false only for a value of that kind: v > 5 is true for a number, and null for a string or a boolean, so the then branch of v > 5 is number in (5..max].

Comparisons and tests

Condition	`v` when true	`v` when not true
`v > 5`	`number in (5..max]`	`Any except number in (5..max] \| Null`
`v >= 5`	`number in [5..max]`	`Any except number in [5..max] \| Null`
`v < "m"`	`string in (.."m")`	`Any except string in (.."m") \| Null`
`v = 5`	`number = 5`	`Any except number = 5 \| Null`
`v != 5`	`number in [-max..5), (5..max] \| Null`	`Any except number in [-max..5), (5..max]`
`v = "a"`	`string = "a"`	`Any except string = "a" \| Null`
`v > "a"`	`string in ("a"..)`	`Any except string in ("a"..) \| Null`
`v between 1 and 10`	`number in [1..10]`	`Any except number in [1..10] \| Null`
`v in [1..10]`	`number in [1..10]`	`Any except number in [1..10] \| Null`
`v in ("a", "b")`	`string in {"a", "b"}`	`Any except string in {"a", "b"} \| Null`
`v > 5 or v = "a"`	`number in (5..max] \| string = "a"`	`Any except number in (5..max], string = "a" \| Null`
`v > 5 and v < 3`	—	`Any \| Null`

The then branch is exact for the kind the other side is. v != 5 is true for a number other than 5, and for null (null != 5 is true); not for a string, which gives null (a different kind).
An or is the union of the kinds. v > 5 or v = "a" is a number above 5, or the string "a".
The else branch of a comparison is Any minus what the comparison is certainly true of (D-194). v > 5 is certainly true of the numbers above 5 and of no value of another kind (it is null for them), so what is left is every kind except those numbers, the numbers that are not above 5, and null: Any except number in (5..max] | Null. v != 5 is certainly true of a number other than 5, so Any except number in [-max..5), (5..max] is left (the 5, and every other kind). A comparison with something that is not one value of a kind (a name, a range) is certainly true of nothing, and leaves Any | Null.

`null`

Condition	`v` when true	`v` when not true
`v = null`	`Null`	`Any`
`v != null`	`Any`	`Null`
`v instance of Null`	`Null`	`Any`

Booleans, lists, contexts

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`
`v = [1, 2]`	`non-empty list<number in 1, 2>`	`Any \| Null`
`v = {a: 1}`	`context<a: number = 1>`	`Any \| Null`
`v.age > 5`	`context<age: number in (5..max]>`	`Any \| Null`

An equality with a list or a context is true only for one of the shape of the other side, part by part (list, context). A path v.age makes v the kinds that have an entry (context).

`instance of`

v instance of T is the meet of Any and T in then (Union.intersect/2, D-194), and never null unless T is Null. In else it is Any minus T (Union.difference/2, D-39): Any is taken apart into its kinds and each loses the part that T covers, so a chain of instance of ends in the kinds that are left, not in Any:

Condition	`v` when true	`v` when not true
`v instance of number`	`number`	`Any except number \| Null`
`v instance of string`	`string`	`Any except string \| Null`
`v instance of boolean`	`boolean`	`Any except boolean \| Null`
`v instance of list<number>`	`list<number \| Null>`	`Any except list<number \| Null> \| Null`
`v instance of context<a: number>`	`context<a: number \| Null>`	`Any except context<a: number \| Null> \| Null`
`v instance of range<number>`	`range<number \| Null>`	`Any except range<number \| Null> \| Null`
`v instance of function<number> -> number`	`function<number \| Null> -> number \| Null`	`Any except function<number \| Null> -> number \| Null \| Null`

A kind that has no value set (a list, a range, a context, a function) is taken out in part when T is not the top of the kind: list<number> is not the lists, and what is left of Any is the lists that are not lists of numbers, written Any except list<number | Null> (a kind minus part of it, Feel.Type.Except, D-152). The kind that T is the top of is taken out whole: v instance of list<Any> leaves Any except list. A repeated test is then decided: once v instance of list<number> is false, v instance of list<number> is false (a decided_condition), and a second test takes a second piece out (Any except list<number | Null>, list<string | Null>).

Expression	Type	Warnings
`if v instance of number then 0 else v`	`Any except number in [-max..0), (0..max] \| Null`	—
`if v instance of number then null else if v instance of string then null else v`	`Any except number, string \| Null`	—
`if v instance of number then null else v + 1`	`Null`	`type_mismatch`
`if v instance of number then null else v = 1`	`boolean = false \| Null`	`type_mismatch`
`if v instance of number or v instance of string then null else v`	`Any except number, string \| Null`	—

The last kind that is left is a value that is not a value of FEEL, and the kinds that take part in an operation are the ones that it is defined for: v + 1 for a v that is not a number is a mismatch whichever kind it is, which the analysis now sees, where Any kept every pair open. A union that has every kind is Any again (Any except number and a number are Any), so the types of the two branches of an if join into the one that holds both.

The other side of an operation is Any too, and the kind of the operand that is known can decide it alone (D-203): true + v, [1] - v, s - v and d * v are Null for every v, where x + v is number | Null and s + v is string | Null, the kinds that their pairs give (D-203), and -v is a number, a duration or null (D-207); null has the rows.

Where a function may be accepted

A function of any parameters is a kind of its own in the union (:function, D-39), and the then of a comparison keeps it where the comparison could be true for a function: = against something that may be a function, and != against that or against something that may be null. A term that is not a value of FEEL (:foreign) stays only where the other side is not known, or for != where it may be null; next to a value of FEEL it is a type mismatch, which is null.

Condition	`v` when true	`v` when not true
`v = f`	`function \| Null`	`Any \| Null`

An ordering never accepts a function, so v > 5 leaves the numbers. (Until D-152 the then of v = f was Any \| Null, because there was no type for every function.)

The other side is not known

If the other side's type is not known, there is nothing to cut with: x > v leaves x a non-null number and no more (null). A comparison with a name whose kind is known cuts, as with a constant.

Used in a call

A narrowed Any is what makes a call's arguments checkable: if v instance of string then abs(v) else 0 types v as string in the call, and abs takes no string (overloaded functions).

A call in a comparison

A comparison of a call of a built-in with a value is not true of a call that is null (D-194), so in then an argument of type Any is limited to the kinds for which the call gives a value of a kind that the other side has (D-170). Any is taken kind by kind, and a function and a term that is not a value of FEEL are two of the kinds (D-155): the rule of the call (Feel.Analysis.Images) says what it gives for each. A parameter that is a list takes any value as the list of it (section 10.3.2.9.4), so a list function is a value for a function as it is for a number, and append(v) != null leaves all of Any; upper case(v) = "A" is true of a string and of a list of one string, and of no function; string(v) = "a" is true of every kind that has a text, except a function and a term that is not a value of FEEL, for which string is null.

Condition	`v` when true	`v` when not true
`append(v) != null`	`Any`	`Any \| Null`
`index of(v, 1) != null`	`Any`	`Any \| Null`
`sum(v) > 5`	`number \| list<Any \| Null>`	`Any \| Null`
`upper case(v) = "A"`	`string \| list<Any \| Null>`	`Any \| Null`
`string(v) = "a"`	`boolean \| number \| string \| date \| time \| date and time \| years and months duration \| days and time duration \| list<Any \| Null> \| range<Any \| Null> \| context<>`	`Any \| Null`
`sort(xs, v) != null`	`function`	`Any \| Null`

The function is left only where the call takes it: sort(xs, v) takes a function of two parameters in place of v, and leaves function (of any parameters, which a type has no other way to write); v as the list of a call that makes a list of it is Any. The operations and the number functions (abs(v) > 0, v + 1 > 5, number functions) take numbers and lists of one number, and leave neither a function nor a term that is not a value of FEEL.