# Narrowing a context

[Narrowing](../narrowing.md) › context. The names in the examples are those of [section 2](../narrowing.md#2-the-names-in-the-examples).

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.

| Condition | `p` when true | `p` when not true |
| --- | --- | --- |
| `p.age > 18` | `context<age: number in (18..max], name: string \| Null>` | `context<age: number in [-max..18] \| Null, name: string \| Null> \| Null` |
| `p.age < 0` | `context<age: number in [-max..0), name: string \| Null>` | `context<age: number in [0..max] \| Null, name: string \| Null> \| Null` |
| `p.age >= 18 and p.name = "a"` | `context<age: number in [18..max], name: string = "a">` | `context<age: number \| Null, name: string \| Null> \| Null` |
| `p.age > 18 or p.name = "a"` | `context<age: number \| Null, name: string \| Null> \| Null` | `context<age: number in [-max..18] \| Null, name: string except "a" \| Null> \| Null` |
| `p.age + 1 > 18` | `context<age: number in (17..max], name: string \| Null>` | `context<age: number in [-max..17] \| Null, name: string \| Null> \| Null` |
| `p.age = x` | `context<age: number \| Null, name: string \| Null> \| Null` | `context<age: number \| Null, name: string \| Null> \| Null` |

The `then` of the second-last row is the preimage of the sum ([number](number.md#operations-in-the-comparison)); 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:

| Condition | `p.age` when true | `p.age` when not true |
| --- | --- | --- |
| `p.age > 18` | `number in (18..max]` | `number in [-max..18] \| Null` |

| Condition | `p.name` when true | `p.name` when not true |
| --- | --- | --- |
| `p.name = "a"` | `string = "a"` | `string except "a" \| Null` |

| Condition | `x` when true | `x` when not true |
| --- | --- | --- |
| `p.age > x` | `number in [-max..max)` | `number \| Null` |

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

| Condition | `p` when true | `p` when not true |
| --- | --- | --- |
| `p = null` | `Null` | `context<age: number \| Null, name: string \| Null>` |
| `p != null` | `context<age: number \| Null, name: string \| Null>` | `Null` |
| `p.age = null` | `context<age: Null, name: string \| Null> \| Null` | `context<age: number, name: string \| Null>` |
| `p.age != null` | `context<age: number, name: string \| Null>` | `context<age: Null, name: string \| Null> \| Null` |
| `p.age instance of number` | `context<age: number, name: string \| Null>` | `context<age: Null, name: string \| Null> \| Null` |
| `p = {age: 1, name: "a"}` | `context<age: number = 1, name: string = "a">` | `context<age: number \| Null, name: string \| Null> \| Null` |
| `p instance of context<age: number>` | `context<age: number \| Null, name: string \| Null>` | `Null` |
| `p instance of context<age: string>` | `context<age: Null, name: string \| Null>` | `context<age: number \| Null, name: string \| Null> except context<age: string \| Null> \| Null` |
| `p instance of context<zip: string>` | `context<age: number \| Null, name: string \| Null, zip: string \| Null>` | `context<age: number \| Null, name: string \| Null> except context<zip: string \| Null> \| Null` |
| `p.zip = "x"` | `context<age: number \| Null, name: string \| Null, zip: string = "x">` | `context<age: number \| Null, name: string \| Null> \| Null` |
| `p.zip != null` | `context<age: number \| Null, name: string \| Null, zip: Any>` | `context<age: number \| Null, name: string \| Null> \| Null` |

- **`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):

| Condition | `v` when true | `v` when not true |
| --- | --- | --- |
| `v.age > 5` | `context<age: number in (5..max]>` | `Any \| Null` |
| `v.name = "a"` | `context<name: string = "a">` | `Any \| Null` |
| `v.a.b > 1` | `context<a: context<b: number in (1..max]>>` | `Any \| Null` |
| `v.age != null` | `list<Any \| Null> \| context<age: Any>` | `Any \| Null` |
| `v instance of context<a: number>` | `context<a: number \| Null>` | `Any except context<a: number \| Null> \| Null` |
| `v = {a: 1}` | `context<a: number = 1>` | `Any \| Null` |

| Condition | `v.a` when true | `v.a` when not true |
| --- | --- | --- |
| `v.a.b > 1` | `context<b: number in (1..max]>` | `Any \| Null` |

`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:

| Expression | Type | Warnings |
| --- | --- | --- |
| `{c: {a: x}, r: if c.a > 5 then c else null}.r` | `context<a: number in (5..max]> \| Null` | — |
| `{q: p, r: if q.age > 5 then q else null}.r` | `context<age: number in (5..max], name: string \| Null> \| Null` | — |
| `{c: {a: 1}, r: if c.a > 5 then 1 else 2}.r` | `number = 2` | — |
| `{a: x, r: if a > 5 then a else null}.r` | `number in (5..max] \| Null` | — |

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.

| Expression | Type | Warnings |
| --- | --- | --- |
| `get value(q, "age")` | `number in [0..150] \| Null` | — |
| `get value(p, "name")` | `string \| Null` | — |
| `get value(q, "zz")` | `Any \| Null` | — |
| `get entries(p)` | `non-empty list<context<key: string, value: Any \| Null>> \| Null` | — |
| `context put(q, "x", 1)` | `context<age: number in [0..150] \| Null, name: string \| Null, x: number = 1> \| Null` | — |
| `get value(context put(q, "x", 1), "x")` | `number = 1 \| Null` | — |
| `context merge([p, q])` | `context<> \| Null` | `null_possible` |
| `context([{key: "a", value: 1}])` | `context<a: number = 1>` | — |

## 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](list.md#over-a-declared-context-type)).
- `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](../narrowing.md#9-limits)).

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