Narrowing a context

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

A context type is {:context, entries}, open, or {:closed_context, entries}, closed (D-65): a declared type is open (context<a: number> is every context that has an entry a that is a number, and may have others), and a context literal has a closed type (the entries it has and no others). A context has no value set, but its entries are unions, so a fact can narrow an entry. And a fact about a path is a fact about the source of the path as well.

Exclusions stay inside those entry and list-element unions. Path and descendant readers request a positive upper approximation where they inspect one, rather than treating :except as a kind with no properties. For a list whose elements exclude context<a: number>, an element can still be {a: "s"} and selecting .a can return ["s"]. The inferred path type must contain that result; declaring list<Null> must still reject it, with or without optimization. Selecting a context entry itself keeps its exclusion-bearing type for the next reader.

Filter entry lookup follows the same rule: xs[a = "s"] must see an a supplied by an excluded context before falling back to an outer name. This includes entries named item or like a built-in. Narrowing an implicit entry works on the positive context base and keeps the exclusions; failure of the outer fallback does not discard a matching context. Structural summaries used by descendant iteration also treat an excluded context as a possible context, never as proof of an empty domain.

A fact about a path narrows the source

p.age > 18 is a condition about the subject p.age (a path that starts at a variable, a local or the element of a filter). Where p is read in the branch, it has to be a value for which p.age can be what the fact leaves (Narrowing.narrow_source/3, D-194):

• an alternative of p stays if selecting from it can be what the fact leaves, and goes if it cannot. A null and a number select null, so p.age > 18 leaves neither;
• a context type that lists the entry has it narrowed (age: number in (18..max]);
• one that does not list it gets it listed, when what the fact leaves is not null: then the entry is there, since an entry that is not there is selected as null;
• a closed context that does not list the entry selects null, so it stays only if the fact can hold for null;
• Any is taken kind by kind where the fact leaves no null (a function has no entries);
• a path of several keys narrows the entries in turn.

The then of the second-last row is the preimage of the sum (number); the last row has nothing to say because x can be null, and then p.age = x can be true for a null age and a null p. The or row shows the rule of the logic: in then neither side narrows alone, and in else both do.

The path itself, and the other side, are subjects as well:

null, shape, and an entry the type does not list

• p.age = null is true for a p whose age is null, or for a p that is null itself (selecting from null gives null); when it is not true p is not null and has an age.
• p = {age: 1, name: "a"} is true only for a context of that shape, part by part, and leaves the closed context<age: number = 1, name: string = "a">. Contexts of other keys are unequal.
• p instance of context<age: string> leaves age: Null: the context types are open and a null conforms to every type, so the only p that is both is one whose age is null.
• p.zip = "x" lists an entry the type does not have. p.zip != null lists it as Any; p.zip = null would list nothing, since it is true of an entry that is missing too.

A name of type Any

Any is taken kind by kind where the fact leaves no null. A path selects from a context, and from a list too (a list of the entries):

v.age != null is true of a context with an age, and of a list (the path from a list is a list, which is not null), and of nothing else: a date has no age, and null.age is null.

Locals, aliases and closed contexts

A path starting at a local is a subject too, identified by the depth of the context that binds it (D-193). So a local that is an alias of a name or a path is narrowed by what the condition says of its own entries, and a context literal has the closed type of its entries:

The third row: c.a is the constant 1, so c.a > 5 is never true.

The functions of a context

get value, get entries, context put, context merge and context are typed by the entries of the context they are given (Feel.Analysis.Images.Context, D-170): the entry of get value is the type of the entry, null for a key that a closed context does not list and Any or null for one that an open context does not, and context put is the context with the entry set (a closed context stays closed). A list of one context is that context, so a list is null where it does not have one. A merge of several contexts is any context, and null only where an item can be no context.

Which paths have a subject

A fact is kept for a path that starts at a variable, a local, or the element of a filter. A path that starts at anything else ({p: 1}.p, a call) has none, because what it selects could be shadowed, and a fact about it would be about another value (D-26). The path is read by its keys as written, so p.address.city is the subject {:path, "p", ["address", "city"]}.

Limits

• 16 facts about the other paths from a name are applied by one read (@max_path_facts, D-154); a name with more is read as if it had 16, and its type says less. The facts about the paths a read follows are always applied.
• A fact about an element of a filter over an open context type is lost (list).
• max_narrowing_facts counts the facts about one path, which in a chain of p.age > 1 and 1 / p.age > 0 and … cannot be answered from its type (limits).

See also: list, Any, date (a fact about a property narrows the date); type-system.md, 3.2.