Narrowing a list

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

A list alternative is {:list, element}, where element is a union: list<number> and list<number | Null> are different members, and the elements of a list literal have the union of their types ([1, "a"] is list<number = 1 | string = "a">; a list that has an element is non-empty list<...>, which is the list type less the empty list, and [] is empty list, D-152). A list has no value set of its own for its length: there is no "a list of three" (D-193: a length is a fact about the node the analyzer holds while it types a comparison, and not about a type), only whether it has an element. So a fact about a list can say four things: whether it is null, what its elements are, whether it has one, and what shape it has when it is compared with another list.

Whether it is null, and its type

• instance of list<T> is true when every element conforms to T, and a null conforms to every type ([1, null] instance of list<number> is true, and so is [] instance of list<string>). In then the list is cut to what is in both; in else the alternative is removed if it is wholly within T; otherwise it becomes the list type less T (list<number | Null> except list<string | Null>, D-152): the lists of the type that are not lists of T.

• xs instance of list<string> leaves list<Null> for a list<number>: the only lists that are both are the empty list and the lists of nulls. It is not —, because the list of nothing is a list of strings too.

For a name of type Any:

Equality with a list

x = other is true only for an x of the shape of the other side's values of the kind, part by part (D-194): xs = [1, 2] leaves a list of the numbers 1 and 2 (that has two, so it has an element), and xs = [] the empty list. Against something whose type is not known it leaves the list as it is. When the shapes have nothing in common the fact leaves nothing, and the branch cannot be taken.

xs = ys can only be true for a list of numbers and a list of strings if both are empty or hold nulls, or are both null. The lengths are not in the type, so [1, 2] and [1, 2, 3] are told apart only when both are literals or constants: Feel.Analysis.Inference.shapes_equal/3 (D-193) types [1, 2] = [1, 2, 3] as false.

The empty list (D-152)

A list is equal to [] if and only if it is empty ([1] = [] is false, [null] = [] is false), null = [] is false, and a value that is not a list is a mismatch, so the result is null. xs = [] leaves the empty list; what is not true has an element or is null.

For a name of type Any:

The comparison itself is true or false and never null against [] (D-170), for a list of any elements and for null: equal_lists/2 of the run is false for lists of other lengths, whatever is in them, and there is no pair to compare for two empty ones. The same for a list of nothing but nulls ([null], which the type reads as list<Null>, as it does []), since a pair with a null is true or false, not an error. Against a list of other elements, or a value that may not be a list, it can be null.

null != [] is true, so null stays in the then of != and is removed from its else. A list that is known to have an element, by xs != [] or because it is the result of append, cannot be []: if xs != [] then (if xs = [] then 1 else 2) else 3 is 2 or 3. What it buys is null: if xs != [] then max(xs) else 0 is number | Null when the elements may be null, and for a list of numbers that are never null it is number (overloaded functions).

The count of a list (D-194)

count(xs) compared with a whole number is a fact about xs. The count of a list is its length, that of a value that is not a list is 1 (it is the list of itself, section 10.3.2.9.4), and that of null is null; so a comparison can be true of the empty list, of values that are not lists, or of lists that have an element, depending on whether it can be true of a count of 0, of 1, or of one or more.

count(xs) != 0 is true of null (null != 0 is true), and count(xs) = 0 is not. A comparison with a number that is not one whole number (count(xs) > n) says nothing. For Any, count(v) > 0 leaves Any except empty list in then, and in else the empty list (and null, and a function, which has no known count).

A function of the list (D-170)

A comparison of a call of a function of lists with a value is not true of a null, so in then the list is not null, and is a list or a list of one value (section 10.3.2.9.4). sum(xs) > 5 is not true of the empty list, which sum rejects, but a type has no list of an element in list<number> to say it.

For a name of type Any the list functions that make a list of a value (append, concatenate, distinct values, flatten, reverse, union, remove, sublist, insert before, list replace, sort) give a value for any kind of argument, a function and a term that is not a value of FEEL included, and so do index of, list contains and is: append(v) != null leaves Any (any, D-155). sum(v) > 5 leaves a number and a list, since a function in a list is not a number.

Conditions that give no fact about a list

An element or a quantifier is not one of the shapes that give facts (what gives none). Apart from the equality with [] and the count, nothing makes a list non-empty.

The type of some and every (D-170)

The test of a quantifier is typed for an iterator that is any element of the domain. A domain that is a list written out (or a name bound to one) is tested one item at a time, as the run does: each item is a value that is tested, and the result is the three-valued or (some) or and (every) of the outcomes, folded from false or true. i > 2 for i in 1, 2, 3 is boolean, but it is true for the 3, so some is true. Several domains that are lists written out are tested for each combination of their items. This is done for at most 64 combinations and 4096 nodes of the test (the combinations times its size), and for lists of up to 32 items, which is what a type keeps of a list (D-193); a list that is not written out, a longer one, and more combinations than that are tested as the type of their elements. The test of a quantifier over a list that has no element never runs, so its nodes are of no value (Never, D-173) and its warnings are not reported.

The domains of a loop (D-170)

A domain is read for each element of the one before it, so a loop reads it only if the domains before it have an element, and one that cannot be iterated (null, a range) ends the loop where it is read. A for over a list that has no element is the empty list, and so is one whose first domain has none, regardless of what comes after (for i in [], j in null return j). A domain that cannot be iterated makes the loop null for sure only where it is read for sure, because every domain before it has an element (for i in [1], j in null return j is Null, with the warning); where the domains before it may have none, the loop is null or the value of an empty product. The domains that are not read are of no value.

The elements a filter keeps

A filter source[brackets] has a mode decided from the type of the brackets (D-71): a predicate (no number can come out of them: keep the elements for which they are true), an index (only a number can: take that element), or dynamic (it cannot be known: the evaluator decides from the value, and the type is that of both readings). A predicate narrows the elements it keeps, by the facts of the brackets about the element item or its entries; an index takes one element and narrows nothing. A predicate that is never true keeps nothing, and the result is the empty list.

An index takes one element, and the element is null for a position that is not there. The first and the last element of a list that has one are there (D-152), so [k, 1][1] and [k, 1][-1] are the element type, which is not null for a k that is not null (an element that is null, xs[1] of a list<number>, is still null). The inferred number | Null for [k, 1][2] is conservative: that position exists and the runtime returns 1, but this index-result bound does not keep that positional precision. It does not mean the written list can have fewer than two elements. A value that is not a list is treated as the list of itself, so its position 1 is the value: k[1] is k. This holds when the brackets are one of those numbers by their type ([k, 1][2 - 1], a name that allowed values make 1), and not when they may be null or anything else. There is no position 0 (D-170): xs[0] is null for every source, a list, a value that is not one, and null (the run has no element at 0, Feel.Runtime.Filter.index/2).

The entries of an element are names in the brackets (a >= 2). For a context in the list, an alternative of the element type is kept with the entry narrowed, and is dropped if nothing is left of the entry: the contexts with a equal to 1 are dropped. An element that is null or a scalar is selected as null, so it is dropped if the fact cannot hold for null.

Field names in a filter can shadow ordinary scope names and builtins. In [{abs: 2}][abs instance of number], abs reads the current item's field. A nested filter can read a field from an outer filter frame when the inner item does not supply it. Resolution distinguishes a definite field (:item_field), the item itself, and dynamic fallback across frames; facts must keep that binding identity. Repreparing just the predicate without its filter scope can change its meaning. DMN's table checker therefore treats field-dependent cells as unknown rather than proving facts about a standalone builtin with the same spelling (DD-43).

Over a declared context type

An element whose type is a declared context (ps is list<context<age: number, name: string>>) is an open type: it may have an entry called item. So item.age in the brackets cannot be trusted to be the entry, and narrows nothing:

Writing the entry as a bare name (ps[age > 18]) is read as the entry of the first element that has it, and narrows it, but it warns unknown_name unless a name of that kind is in scope, because the type does not say that every element has it. A list of context literals has closed types and has neither problem.

Limits

• No length: a list type says whether it has an element, but not how many (D-193, D-152). A list literal and a constant have one ([1, 2] is non-empty list<number in 1, 2>), the result of a filter does not.
• A literal of more than 32 elements keeps only its length for the comparison of lists, not the types of the elements by position (D-193).
• A fact about item over an open context type is lost (see above).
• The elements of a declared list are narrowed by the allowed values of the name, which apply to each element (D-51, Feel.Analysis.TestSets.restrict_elements/2), and not by conditions on the list.

See also: context, range, Any; type-system.md, 3.1.