# The type systems of `feel`

`feel` has two type languages that look alike and do different jobs. One is the type system of the DMN specification, a small lattice that says which values an operation is defined for. The other is an internal type that the analyzer infers with, and it is much richer: it makes `null` an explicit alternative, and it carries *sets of values* (intervals of numbers, sets of strings, the dates a date can be). The internal type is what lets `x > 5 and x < 3` be shown never to be `true`, what lets the optimizer drop checks, and what supports explanations for selected possible `null` results. This is a value analysis with bounded approximations, rather than only a check of declared kinds.

This document is the implementation guide: it explains both type languages, their representations, and how the analyzer uses them. The [type-system assessment](type-system-analysis.md) contains the correctness contracts, scientific foundations, language comparisons, recommended design, and open obligations. The original examples were recorded on 2026-10-16 with Elixir 1.20.4 on OTP 29 after D-173; later updates cover callable summaries, three-outcome facts, D-207's unknown negation and repeated-value arithmetic, the initial correctness repairs of 18 October 2026, and the signature, range and DMN proof contracts described in the [assessment](type-system-analysis.md#2-contracts-and-evidence). They are recorded examples rather than a fresh run of the whole guide, and may drift as the analysis improves. [architecture.md](architecture.md) says where the type modules sit in the pipeline; [decisions.md](decisions.md) says why (D-39, D-109 and the rest, cited below).

**Correctness status.** The reproduced function-result check bypasses, nested-negation errors, false rule proofs, numeric complement/inclusion failures and order-dependent equivalence answers are repaired. Function signatures and call refinements now have separate roles, and certainty bounds use a different approximation direction from possible results. `join/2` promises a conservative common supertype, not a least one. The [assessment](type-system-analysis.md#2-contracts-and-evidence) states each contract and the remaining audit work; these regressions do not establish a general soundness or completeness guarantee.

Contents: [1 The two languages](#1-the-two-type-languages) · [2 The lattice](#2-the-specifications-lattice-feeltype) · [3 The internal type](#3-the-internal-type-feeltypeunion) · [4 Internal type against lattice](#4-the-internal-type-against-the-lattice) · [5 Using the types](#5-what-the-analyzer-does-with-the-types) (inference, why a result is `null`, narrowing, declarations, calls, uses, limits) · [6 Soundness](#6-keeping-it-sound) · [7 Reading list](#7-where-to-read-more)

## 1. The two type languages

| | `Feel.Type` | `Feel.Type.Union` |
| --- | --- | --- |
| Source | DMN 1.6, section 10.3.2.9 | this library (D-39) |
| Shape | an atom or a small tuple: `:number`, `{:list, :string}` | a list of alternatives: `[:number, :null]` |
| `null` | under every type: `number` means "a number or `null`" | an alternative of its own, present only when the value may be `null` |
| Unions | none | the point of it |
| Values | which kind a value is | *which* values: `number in [0..150]`, `string except "a"`, `boolean = true` |
| Lives in | declarations, `instance of`, conformance, the implicit conversions, `Feel.type/1` | `meta.type` of every IR node, inference, narrowing, the optimizer |
| Seen by the caller | yes | IR metadata and explicit `Feel.Type.Union` / `Feel.Rules` APIs |

They are connected by two functions that are not inverses. `Union.from_spec/1` reads a type of the specification and adds `:null` at every level. `Union.to_spec/1` goes back, drops `:null`, and joins what is left with the lattice's join, so it loses information:

```
type expression  --Feel.Type.parse-->  Feel.Type  --from_spec-->  Union
(list<number>)                         (declared)                    |
                                                                     |  Analyzer: infers a Union for every node,
                                                                     |  narrows it by conditions, checks calls
                                                                     v
Feel.type/1  <------ to_spec -------------------------------   meta.type of the IR
(spec type)                                                          |
                                                                     |  Optimizer drops checks the type settles;
                                                                     v  diagnostics warn of certain mismatches
```

`Feel.type/1`, the type a caller sees, uses the declaration type language. The union stays internal. For guarded recursion, `from_spec/1` produces a bounded upper approximation rather than an exact translation. Runtime membership keeps the original declaration graph; see [guarded types](#guarded-recursive-types).

<a id="2-the-specifications-lattice-feeltype"></a>

## 2. The specification's lattice (`Feel.Type`)

The specification (section 10.3.2.9, Figure 10-26) gives FEEL a lattice with `Any` on top and `Null` at the bottom. Apart from the parameterised families the lattice is *flat*: the primitive types are siblings.

```
Any                     the top: every value, null included
 |-- number, string, boolean
 |-- date, time, date and time
 |-- years and months duration, days and time duration      (no common supertype)
 |-- list<T>, range<T>, context<k: T, ...>, function<T, ...> -> R
Null                    the bottom: the value null, which is under every type
```

All the children of `Any` are siblings, with no edge between them. Only the parameterised families, on the last child line, are ordered inside themselves, by the rules below.

The rules, as `Feel.Type.Conformance` implements them (`T <: S` means "`T` can be used where `S` is expected"):

| Rule | Consequence |
| --- | --- |
| `Null <: T <: Any` for every `T` | `null` is a valid value of every type |
| a primitive conforms only to itself | `date` does **not** conform to `date and time`; the two durations have no common supertype (the notes call this A25) |
| `list<T> <: list<S>` and `range<T> <: range<S>` when `T <: S` | covariant |
| `context<M> <: context<N>` when every member of `N` is in `M` with a conforming type | **open** records: a context with more entries conforms to one with fewer |
| `function<P> -> R <: function<Q> -> S` when each `Q` conforms to its `P`, and `R <: S` | contravariant parameters, covariant result; parameter names are not part of the type |

The specification lattice has no union constructor. `Feel.Type.join/2` computes a common supertype, which is why a list literal of mixed things is `list<Any>`. The API promises a conservative common supertype; it need not be the least expressible one for functions or composite declarations. Equivalence accepts equal terms or conformance in both directions, so reordered union declarations can compare equivalent. For bounded relations, failure to prove equivalence does not prove semantic inequality. See [section 2.6](type-system-analysis.md#26-equivalence-and-join).


```elixir
Feel.Type.join(:number, :string)                       #=> :any
Feel.Type.join({:list, :number}, {:list, :string})     #=> {:list, :any}
Feel.Type.join(:number, :null)                         #=> :number          (null is absorbed)
Feel.Type.conforms?(:date, :date_and_time)             #=> false
small = {:context, %{"id" => :number, "name" => :string}}
large = {:context, %{"id" => :number, "name" => :string, "age" => :number}}
Feel.Type.conforms?(large, small)                      #=> true (more entries conform to fewer)
Feel.Type.conforms?(small, large)                      #=> false
Feel.Type.of([1, "a", true])                           #=> {:list, :any}
```

Three more pieces belong to the lattice and not to the union:

- **`instance of`** (Table 62): `null` is an instance of `Null` only, so `Feel.Type.instance?(nil, :number)` is `false`, while `Feel.Type.value_conforms?(nil, :number)` is `true`. The two questions differ, and both are needed.
- **Implicit conversions** (section 10.3.2.9.4, D-24): where a value is bound to a parameter of a declared type it may be converted. The three are from a singleton list (`["foobar"]` to `"foobar"`), to a singleton list (`3` to `[3]`), and from a date to a date and time at midnight UTC. They are tried only when the value does not already fit, in that order, and at most one applies. One more is not in the specification, but the TCK needs it (D-197): a built-in function with several signatures that differ only in their types (`abs`), where a function type is declared that the function is not an instance of but one of its signatures is (`function<number> -> number`), becomes the function of that signature, which takes what the type says and returns `null` for the rest.
- **`T!`**, an extension (D-48): a declaration that the name is never `null`. It is the only way to say "not null", and it exists because the lattice has none. A type in an expression may have it too (D-48).

Two more extensions go past the lattice, for what a host *declares* (D-178), as `T!` does: the lattice has no union and no negation, and the internal type has both, so a declaration may say that a name is anything but a number, or a number or a string.

| Declared as | Written (`Feel.Type.parse/2`, `format/1`) | The values | `Feel.IR.type/1` of the name |
| --- | --- | --- | --- |
| `{:not, :number}` | `Any except number` | every value that is not a number, and `null` | `Any except number \| Null` |
| `{:union, [:number, :string]}` | `number \| string` | a number or a string, and `null` | `number \| string \| Null` |
| `{:not, {:union, [:number, :string]}}` | `Any except number \| string` | neither a number nor a string, and `null` | `Any except number, string \| Null` |
| `{:non_null, {:union, [:number, :string]}}` | `(number \| string)!` | a number or a string | `number \| string` |

Runtime membership evaluates a composite's union or negation directly against the exact component declarations (`Feel.Type.Composite`). This also covers recursion in a value's function signature when the target itself has none. The analysis projection can be wider, especially for recursive negation, and cannot replace that runtime check. Non-recursive composite conformance asks `Union.subtype?/2`; composite conformance with recursive descriptors accepts identical terms conservatively. `null` is in them as it is in every declared type, since the run exempts `null` (D-138), and only a mark on the whole takes it out. They nest in a list, a range, a context and a function type. `Any except` takes the rest of the union (`Any except number | string` is neither), a type may be put in parentheses, and a `!` on a member is refused (`(Any except number)!` is how to mark the whole). The conversions are the lattice's, asked of the union: a singleton list is unwrapped when its element is in the type and the list is not, and nothing is wrapped in a list and no date is converted to a date and time in order to reach a member. `Feel.type/1` is a type of the specification, so for such a name it is wider (`Any`, `list<Any>`).

```elixir
Feel.Type.parse("Any except number | string")      #=> {:ok, {:not, {:union, [:number, :string]}}}
Feel.Type.parse("list<number | string>")           #=> {:ok, {:list, {:union, [:number, :string]}}}
Feel.Type.parse("Any except number!")              #=> {:error, …}   a ! on a member is not read; mark the whole: (Any except number)!
Feel.Type.format({:union, [:number, {:not, :string}]})   #=> "number | (Any except string)"
```

These are for the declarations of a scope, the result type and the input of unary tests, and for a type of the scope that an expression names (`v instance of tId`, `function(a: tId) a`, where `tId` is `number | string`). The types written in an expression are those of the specification and `T!`: `x instance of Any except number` is `Any` followed by a word that is not part of the type.

Because `null` is under every type, the lattice cannot say that `1 < 2` is *never* `null` or that `1 < null` is *always* `null`. Both are just `boolean`. That is what the second type language is for.

<a id="guarded-recursive-types"></a>

### 2.1 Model-defined and guarded recursive types

`Feel.ItemDefinitions` resolves acyclic model definitions into ordinary structural types. Recursion is a caller-selected extension with three modes:

| `Feel.ItemDefinitions.new/2` option | Behavior |
| --- | --- |
| `recursive: :error` (default) | Recursive references leave the definition unread, with a `:recursive` problem. |
| `recursive: :guarded` | Retain a finite graph and validate every finite descendant and its inherited/component constraints. |
| `recursive: :any` | Legacy approximation: replace a reference closing a loop with `Any`, accepting data the full declaration could reject. |

In guarded mode, every cycle must cross a context member or list element. Alias-only cycles and cycles through function signatures remain errors. A finite function item may accept or return recursive data. Build graphs through `Feel.ItemDefinitions`; a plain cyclic map of unresolved `{:named, name}` types still fails `Feel.Type.resolve/2`.

```elixir
definitions = Feel.ItemDefinitions.new([
  %{name: "Node", components: [%{name: "next", type_ref: "Node"}]}
], recursive: :guarded)
type = Feel.ItemDefinitions.types(definitions)["Node"]
Feel.Type.value_conforms?(%{"next" => %{"next" => nil}}, type) #=> true
Feel.Type.value_conforms?(%{"next" => %{}}, type)              #=> false: missing next
```

Runtime membership checks the full finite value. A present `null` member keeps the normal null exemption; a missing member does not conform. Allowed values and type constraints are separate: `instance of` and `Feel.Type.value_conforms?/2` check structure only. Declarations carrying those constraints enforce them at every recursive occurrence through graph paths. Constraint traversal is incremental: a rejected occurrence stops the walk immediately. Successful checks share reversed paths; only a failing diagnostic constructs its complete forward path, avoiding quadratic path materialization on deep chains. During contained FEEL execution, shared worker deadlines and heap policies bound structural membership and recursive selector traversal, including shared-subtree expansion. Constraint tests retain their call and iteration counters even when diagnostics are isolated. Direct host membership queries have no worker, so containing them is the caller's responsibility. Ordinary conversions apply at binding, parameter and result boundaries, including singleton wrapping for a recursive collection or alias, and unwrapping for a recursive context. They do not convert fields inside a context. A collection's allowed values apply to its elements; its type constraint applies to the whole list.

To enforce constraints, build the variable's scope from the definitions. Supplying only `types(definitions)["Node"]` to a plain scope, or calling `value_conforms?/2`, does not carry them:

```elixir
definitions = Feel.ItemDefinitions.new([
  %{name: "Node", components: [
    %{name: "value", type_ref: "number", allowed_values: "[0..9]"},
    %{name: "next", type_ref: "Node"}
  ]}
], recursive: :guarded)
{scope, unread} = Feel.ItemDefinitions.scope(definitions, %{"node" => "Node"})
# unread == %{}; inspect ItemDefinitions.problems/1 and unread before using model declarations
{:ok, expression} = Feel.prepare("node", scope: scope)
bad = %{"value" => Decimal.new(1), "next" => %{"value" => Decimal.new(20), "next" => nil}}
{:ok, nil, [diagnostic]} = Feel.run(expression, %{"node" => bad})
{diagnostic.code, diagnostic.details.path} #=> {:value_not_allowed, ["next", "value"]}
```

This uses the default `declarations: :enforce`: a failing descendant makes the whole variable `null`, and strict execution ends with an error. Declaration stances such as `:report`, `:trust` and `:ignore` keep their existing behavior; selecting guarded mode does not override them. Diagnostic paths use member names and one-based list indexes. For a result boundary, obtain `{:ok, type, constraints}` from `Feel.ItemDefinitions.variable(definitions, "Node")`, then pass `result_type: type, result_allowed_values: constraints` to `Feel.prepare/2`.

Analysis unfolds repeated names conservatively and shares a 256-node projection budget. Exhaustion widens the analysis, with no corresponding cutoff in runtime membership. Inclusion in the projection proves neither recursive membership nor that conversion preserves the operand: parameter and result bounds describe the converted value, and specialization discards pre-conversion shapes, callees and origins. Recursive result checks and reachable negative branches remain.

Recursive conformance accepts identical reachable graphs under consistent one-to-one renaming, including import prefixes, while ignoring unrelated graph entries. Constructors, constraints and reference sharing must agree. It also accepts graphs related by ordinary lattice rules but does not provide general recursive subtyping or equivalence. Even a structural upper projection need not be accepted as a recursive function's result signature. Runtime closures keep an enforced recursive result declaration through result and binding checks (`Feel.IR.result_spec/1`). The analyzer selects the runtime result signature before optimization and stores it in the function's `meta.returns`; both backends keep it when a conditional body folds to a declaration. Observable analysis arrows use `Any | Null` for that result and keep structural bounds only as call refinements. Recursive parameter domains use an empty lower bound in upper arrows. Graph projection and overlapping runtime signatures can lose call precision too. These are analysis limits, not weaker finite-data validation ([D-189](decisions.md#d-189-recursive-items-have-an-explicit-guarded-graph-mode)).

<a id="3-the-internal-type-feeltypeunion"></a>

## 3. The internal type: `Feel.Type.Union`

### 3.1 The shape

A union is a list of the alternatives a value may have, and `:null` is one of them when the value may be `null`:

| Union | The values |
| --- | --- |
| `[:number]` | a number, never `null` |
| `[:number, :null]` | a number or `null` (the specification's `number`) |
| `[:null]` | `null` only |
| `[:boolean, :string]` | a boolean or a string, never `null` |
| `[:any, :null]` | any value (the specification's `Any`) |

`:any` inside a union means *any value that is not `null`*, and it is the union of the kinds of value (D-39): the eight primitive kinds, a list, a range, a context and a function of any shape, and `foreign`, a term that is not a value of FEEL (the host binds what it likes, and the run treats it as a value of an unknown kind). A union that has all of them is `Any`, and one that lacks some is written by what it lacks: `Any except number`. The parts of a list, a range, a context or a function are unions in turn, so `list<number>` and `list<number | null>` are different members.

The members a union can have (`Feel.Type.Union`, the type `member`), and how `Union.format/2` writes them:

| Member | It is | Written |
| --- | --- | --- |
| `:null` | the value `null` | `Null` |
| `:boolean`, `:number`, `:string`, `:date`, `:time`, `:date_and_time`, `:years_and_months_duration`, `:days_and_time_duration` | every value of the kind | `number` |
| `{:number, set}` and the same for the other kinds, `{:string, strings}`, `{:boolean, true}` | some of the values (3.3) | `number in [0..150]`, `string = "a"`, `boolean = true` |
| `{:list, u}`, `{:range, u}` | a list or a range whose parts are the union `u` | `list<number \| Null>` |
| `{:context, entries}`, `{:closed_context, entries}` | an open context (a declared type) or a closed one (a literal), each entry a union | `context<age: number>` for both (`closed context<…>` inside an `except`) |
| `{:function, parameters, result}` | the values that are an instance of one function type, an *arrow* | `function<number> -> number` |
| `{:overload, arrows, refinements}` | observable function arrows with separate call refinements (3.5) | `overload<…>` |
| `{:except, base, negations}` | a list, a range, a context or a function **less** some of it (3.5) | `list<Any \| Null> except list<number \| Null>`, and `non-empty list<number>` for a list less the empty one |
| `{:list, []}` | the empty list: a list with no element it could have (D-152) | `empty list` |
| `{:named, name}` | a type of a model that is not looked into | the name |
| `:any` | any value that is not `null`: the union of the kinds | `Any`; a union that lacks some kinds is written by what it lacks, `Any except number` |
| `:function`, `:foreign` | a function of any shape (also the fallback for unsafe arrow erasure), and a term that is not a value of FEEL | `function`; `:foreign` is not written, it shows only as what `Any except …` leaves |

A union has a **normal form**, built by `Union.new/1`, so that two unions of the same alternatives are equal: no repeats, a fixed order with `:null` last, `:any` absorbs everything else, and at most one alternative per kind of number, string, boolean, date and duration (the sets of several are joined).

```elixir
Union.new([:null, :number, :number])    #=> [:number, :null]
Union.new([:number, :any])              #=> [:any]
Union.new([:any, :null, :boolean])      #=> [:any, :null]
```

A union that is built has at least one alternative: `Union.new/1` raises for none. The least type of an expression that runs is `[:null]`, because a failure is a `null` and not the lack of a value, so a type with no alternative is not the type of anything that has a value. But there is one, the **empty union**, `Union.never()`, `[]`, written `Never` (D-173). It is the `never` of TypeScript and the `none()` of Elixir:

- It is the type of **code that cannot run**, and it is not `[:null]`. `[:null]` is code that runs and gives `null`; `Never` is code that gives nothing because it is not run. The analyzer gives it to every node of a branch of an `if` that cannot be taken (5.3).
- It is the bottom of the order: `subtype?([], u)` is true for every `u`, nothing but itself is within it, `contains?([], v)` is false for every value, and `Union.new/1` leaves it out of what it joins. Where the lattice has `Null` at the bottom because `null` is under every type, the union has `Never`, because `[:null]` is not under `[:number]`.
- `Union.intersect/2` and `Union.difference/2` return it when two unions share nothing, or when nothing is left (the two cannot be the same value), and it is the element type of the empty list (`{:list, []}`, below).

A node of this type that a run reaches means that the type was wrong, and `Feel.Paranoid` says so (section 6).

### 3.2 `null` made explicit

This is the first of the two things that the union adds to the lattice (D-39). The analyzer can now say that a result is, or is not, `null`:

| Expression | `Feel.type/1` | `Feel.IR.type/1` |
| --- | --- | --- |
| `1 < 2` | `boolean` | `boolean = true` |
| `1 < null` | `Null` | `Null` |
| `1 / 0` | `Null` | `Null` |
| `1 = null` | `boolean` | `boolean = false` |
| `age` (a name of type `number`) | `number` | `number \| Null` |
| `[1, "a", true]` | `list<Any>` | `non-empty list<boolean = true \| number = 1 \| string = "a">` |
| `{a: 1, b: "x"}` | `context<a: number, b: string>` | `context<a: number = 1, b: string = "x">` |
| an unknown name `v` | `Any` | `Any \| Null` |

A `number` that is bound from outside may be `null`, so `age` is `number | Null`. A constant never is. Note the two rows of structure: the type of a list is the union of its elements (the specification's `list<Any>` forgets that the elements are a boolean, a number and a string), and a context literal has a **closed** type, the entries it has and no others, where a *declared* context type is open (D-65). A closed context is a subtype of the open one with the same entries, so it knows more, for instance that an entry it does not list is not there.

### 3.3 Value sets

Numeric set endpoints and runtime numbers are related but not interchangeable. `NumberSet` can hold decimal bounds that do not themselves fit the runtime's 34-digit format; month-duration images can also contain integers of arbitrary size. Rounding images cut their endpoints outward to representable FEEL numbers (D-220), preserving upper bounds instead of using a huge exact integer step as a runtime operand. Power inference remains conservative for unsupported corners; root, logarithm and exponential images can fall back to signature bounds. See the [numeric endpoint rules](narrowing/number-functions.md#numeric-endpoints-and-conservative-fallback).

This is the second addition (D-39, D-109). An alternative can say *which* values it has. The bare kind (`:number`) is every value of the kind and contains any set of it.

| Kind | The set | Written | Module |
| --- | --- | --- | --- |
| number | intervals of decimals, within decimal128, ends open or closed | `number in [0..150]`, `(5..max]` | `Feel.Type.NumberSet` |
| string | single strings (up to 64), or intervals of strings, with strings left out | `string = "a"`, `string except "a"` | `Feel.Type.StringSet` (D-39) |
| boolean | `true` or `false` | `boolean = true` | built in |
| date, years and months duration, days and time duration | the *image* of a value as a number (days, months, seconds), as a `NumberSet` | `days and time duration = PT2H` | `Feel.Type.Image` (D-109) |
| time, date and time | the second it falls in, on three lines (the clock, the instant, the zoned clock), plus the fraction of the second | `date and time = 2021-01-31T10:30:00` | `Feel.Type.Moment` (D-109, D-118) |

The image trick is worth a sentence. A date, a duration, a time and a date and time are ordered, and for the durations also added and scaled. If each value is mapped to a number, one-to-one and order-preserving, then the interval algebra written for numbers works for them too: the seconds of `PT1H + PT2H` are `3600 + 7200`. A time and a date and time cannot use one number, because the order of two of them depends on their zones, so `Moment` keeps three lines of numbers far apart on the number line and a value is in a set when its numbers are on the right lines.

Numeric construction, union and intersection take an approximation policy: `:outer` (the default) replaces more than 16 merged intervals by their hull; `:inner` keeps at most 16 intervals as a subset; `:exact` keeps all intervals. Possible-result analysis uses upper bounds, while `TestSets.certain/2` uses inner numeric bounds. `NumberSet.complement/1` and `subset?/2` are exact over their supplied sets, including when the complement of 16 intervals needs 17. Exact complement cannot recover values lost by an earlier approximation; callers must still choose the correct bound direction. In particular, numeric and numeric-image exclusions are combined exactly before complementing in `Union.difference/2`. Range-subtyping proofs can combine several individually small endpoint sets past the cap; using an outer hull there would erase genuine gaps and could prove false range coverage. The remaining positive result can still be widened safely. This does not turn every union operation into exact algebra.

Ordinary union normalization also widens string sets with more than 64 points or exclusions to the whole string kind. Certain string sets instead discard information before that widening can establish a false proof. The boundary cases are in [sections 2.3 and 2.5](type-system-analysis.md#23-certain-and-possible-sets-in-rule-analysis). The ordinary upper-bound simplifications include:

```
[0..5) and [5..9]      become   [0..9]              touching intervals merge
[0..5) and (5..9]      stay     [0..5), (5..9]      5 is in neither, so there is a gap
[0..1], [10..11], ... [190..191]   (20 intervals)
                       become   [0..191]            over 16 intervals: the one that holds them all
a string set with more than 64 points or exclusions becomes every string in Union normalization
```

A set is not a type in the sense of a name for a class of values. It is a *value domain* with a union, an intersection, a complement, a subset test and a membership test. `NumberSet.complement([0..150])` is `[-max..0), (150..max]`, and `StringSet.complement(["a"])` is `(..) except "a"`. That is the complement of a *set of values*. The negation of a *type* with parts, which has no set to cut, is a member of its own (3.5).

### 3.4 The operations

| Operation | Intended role | Current limitation |
| --- | --- | --- |
| `Union.new/1` | Combine alternatives in normal form | Retains nested exclusions and function domains; scalar caps and structural merging can still widen alternatives |
| `Union.intersect/2` | Keep values common to both descriptions | Depends on scalar and structural representations; a named type is not looked into |
| `Union.difference/2` | Remove described values, by kind (D-39, D-152) | Structural search and representation limits can retain extra values; it is not unrestricted exact subtraction |
| `Union.subtype?/2` | Establish inclusion | `false` can mean not proved; numeric inclusion uses exact complement/intersection, but the wider procedure remains bounded |
| `Union.restrict/3` | Cut a scalar kind to a set | Must respect the set's approximation direction and resource policy |
| `Union.contains?/2` | Check membership in the represented union | Agreement with this predicate does not establish the intended meaning of an incorrectly translated declaration |
| `Union.of_value/1` | Describe a value, including list element alternatives | A description of elements does not necessarily denote only that concrete list |
| `from_spec/1`, `to_spec/1` | Translate between the two languages | Projection can lose precision; a function projects to `Any` if the public language cannot express a safe parameter domain |

Existing tests compare `subtype?/2` with `Feel.Type.conforms?/2` on selected specification types. An alternative that no alternative of the other union holds by itself may be held by several together (D-152): `subtype?/2` then asks whether anything of it is left when the others are taken out (`difference/2`). So a case that a comparison alternative by alternative cannot see is detected, as in the [set interpretation](type-system-analysis.md#31-semantic-subtyping-gives-types-a-meaning-before-an-algorithm), for lists, ranges and contexts:

```text
# the unions are written in shorthand here (Union.format/1 prints a closed context as `context<…>`); `|` is the union
a = closed context<k: "a" | 1>
b = closed context<k: "a"> | closed context<k: 1>
Union.subtype?(a, b)            #=> true      (every value of `a` is in `b`; it was `false` before D-152)
Union.subtype?(b, a)            #=> true
```

The procedures use resource bounds: a range search stops above 6 negations, and a context search above 4,096 parts or 256 for one entry (D-158). Functions use the signature model in section 3.5. A built-in with several signatures is an **overload**. A negative Boolean answer may mean only "not proved". A positive answer still needs a valid underlying inclusion argument; the current boundaries and projections prevent a blanket soundness claim.

Normalization keeps exclusions inside lists, ranges, contexts, functions and excluded types. Readers request a positive approximation explicitly at the level they inspect. Widening an excluded part or a function parameter during normalization would change the meaning in the wrong direction. For paths, that includes list elements and nested entries traversed by descendant selection, as well as the source union. `Paths` approximates those inspected unions locally; a selected context entry keeps its original exclusion-bearing type. The path-result check regression is described in [section 2.4](type-system-analysis.md#24-nested-exclusions-and-the-readers-of-types).

This obligation also applies to filter name discovery, recursive equality of context fields, context construction/merge, callback classification and generic signature-derived flattening. An excluded context can supply filter entries and unknown descendants; it cannot be treated as absent when deciding bindings or domain emptiness. Open context types do not establish that an unlisted `key` or `value` is missing. A callback's runtime acceptance follows its observable arrows, not a specialized Boolean call result. Recorded arrows are guarantees, not an exhaustive signature list: a three-argument function can also support a two-argument Boolean callback. Without a qualifying guaranteed arrow, list images keep both success and rejection, including after narrowing or exclusion. [Section 2.4](type-system-analysis.md#24-nested-exclusions-and-the-readers-of-types) states the reader rules, the result-check regressions and the bounded independent oracle.

A list has two more types that the union of the kinds does not give (D-152): the **empty list**, `[]`, a list with no element it could have, and a **list that has an element**, a list type less it (`non-empty list<number>`). `list<T>` is the two, and the meet of two lists with no element in common is the empty list. These examples illustrate the supported list operations:

```text
Union.intersect([list<number = 7>], [list<string>])        #=> [empty list]
Union.difference([list<number | Null>], [empty list])      #=> [non-empty list<number | Null>]
Union.new(non_empty ++ [empty list])                       #=> [list<number | Null>]
```

<a id="function-signatures"></a>

### 3.5 A kind less some of it, overloads, and functions

A list, a range, a context and a function have no set of values to cut, so what is left of `Any` when some of one is taken out is a member of its own, `{:except, base, negations}` (`Feel.Type.Except`, D-152): the values of `base` that are in none of the `negations`. It is how `v instance of list<number>` leaves its `else` branch:

```feel
if v instance of list<number> then 1 else v     #=> Any except list<number | Null> | Null      (v is Any)
```

Whether such a member has any value is queried kind by kind, subject to the representation and search limits. A list less lists of `N1`, `N2`, … is treated as empty when its base is within one of them (a list avoids each with an element of its own); a range has two ends that each avoid some of the negations (a range with more than 6 negations is taken to have values); a context is a box of the types of its entries and the question is whether the boxes of the negations cover it (at most 4,096 parts are visited, and 256 for one entry), and an entry that an open context does not list is there or not. Past a bound, or where the answer is not shown, the member is kept: the type holds more than it has to. Two members are also in normal form when no negation is within another and each shares values with the base.

<a id="function-signature-contract"></a>

A function has no values to list either. The only thing the run says of one is the function types it was declared with, so a function is a finite set of **arrows**, and it is an instance of a function type when one of its arrows is within it (`Feel.Type.Arrows`, D-171). That is what `instance of` answers, so it is the meaning of the type: the `else` of a test is taken out when the run takes it. An arrow `A` is within `B` when `B`'s parameters are within `A`'s and `A`'s result is within `B`'s (the rule of the specification), and a type of arrows less arrows has a function unless some arrow of the first is within some arrow taken out. It is one comparison and not a search.

A built-in function with several signatures is all of them. `before` is four function types, a point or a range for each of its two parameters; `abs` is declared with one parameter for the three kinds it takes. Its type is `{:overload, arrows, refinements}`: the arrows are what the algebra sees, and the refinements are what a *call* does for arguments within the parameters of a signature (`abs` of a duration is a duration), which types a call and nothing else:

```feel
before instance of function<number, number> -> boolean       #=> boolean = true
abs instance of function<number> -> number                   #=> boolean      (not true: abs takes the three kinds in one parameter)
```

The algebra stops short of the semantic subtyping of Frisch and Castagna, where `(A → B) ∧ (C → D)` is within `(A ∪ C) → (B ∪ D)`. The run does not say that, and a type that said more than the run would put a value in an `else` branch that the type excluded. A union holds at most four overloads; past that each is its arrows.

A function literal also uses an overload when its body gives a more precise call result than its observable signature. For `function(x: number) 1`, the arrow returns nullable `number`, matching runtime metadata; the call refinement returns exactly `1`. Only the arrow participates in `instance of`. Calling the function can use the refinement without claiming that the value has a non-null result signature. Literal closures keep this distinction when stored in a list or context. The observable signature comes from kind-only analysis in the written environment and stays fixed across analysis tiers, call specialization and optimization (D-219). Full analysis makes this additional bounded pass only when the expression contains function literals. Each pass retains the callable reanalysis budgets described in section 5.5. Private AST occurrence keys distinguish functions independently of their spans, so embedded trees with coincident spans do not share signatures.

For `v: Any` bound to `5`, `(if v instance of number then (function() v) else (function() 1)) instance of function<> -> number` is `false` in both tiers: the selected closure's written result signature is `Any`. Calling that closure still returns `5`; full analysis can keep its numeric call result. Runtime signature inspection, callback acceptance and result-check removal must not substitute that call fact for the observable arrow.

The [guarded-recursion contract](#guarded-recursive-types) also applies to scope-declared functions and function values. Structural recursive call bounds are not observable signature proofs. When runtime signatures overlap, their possible results remain alternatives; projection does not turn each signature's result into a simultaneous call guarantee.

Public projection preserves a parameter's outer non-null mark and checks that the projected domain is within the original domain. If that check cannot be established, the whole function projects to `Any`. `Union.erase_sets/1` follows the same variance rule: a parameter that would become broader makes the arrow fall back to the internal `:function` kind; result refinements can be widened normally.

## 4. The internal type against the lattice

| | The lattice | The union |
| --- | --- | --- |
| Question it answers | may this operation be applied? what does `instance of` say? | what can this expression's value be, exactly enough to act on? |
| `null` | in every type | explicit, absent unless possible |
| Join | conservative common supertype: `number` ⊔ `string` = `Any`; no general leastness promise | combined alternatives: `number \| string`, subject to normalization |
| Meet | always `Null` for two different kinds | `Union.intersect/2`: the values in common, set by set; `Never` if there are none |
| Bottom | `Null`, under every type | `Never`, `[]`: the type of code that cannot run (3.1); `[:null]` is not under `[:number]` |
| Difference | none | `Union.difference/2`: what is left, kind by kind (`Any except number`), and a kind with parts less some of it (`Any except list<number \| Null>`) |
| Information about values | none | intervals, string sets, booleans, images of temporal values |
| Records | open, structural | open for declarations, **closed** for literals |
| Functions | one arrow, contravariant in the parameters | observable signature bounds plus call refinements; built-ins, literal closures and recursively declared results can use overloads (3.5) |
| Why a result is `null` | not asked | an info that names a pair of values that cause it (5.2) |
| Relations | `conforms?`, mutual-conformance `equivalent?`, conservative common-supertype `join` | `subtype?`, `intersect`, `difference`, `restrict`, `contains?`; each needs its own approximation contract |
| Reaches the caller | yes, `Feel.type/1` | no |
| Correctness obligation | implement the specified declaration meaning | results need upper bounds; certain inputs need lower bounds; proofs need valid premises (section 6) |

The conversion loses information in both directions, which is why the union is for inference and the specification's type for everything else. Going out, `to_spec([:number, :string])` is `:any`, and `to_spec([:number])` is `:number`, which in the lattice also includes `null`. Going in, `from_spec(:number)` is `[:number, :null]`, a `null` that may not be there.

A declaration has a specified meaning independent of the code translating it. Analysis facts may approximate that meaning, but their direction depends on the consumer. Neither the declaration implementation nor the inferred union is correct merely because its own membership and normalization procedures agree.

## 5. What the analyzer does with the types

### 5.1 Inference

`Feel.Analysis.Inference` types each operation by typing every *pair* of alternatives, one from each operand, and joining the results. `[:number, :null] + [:number]` is the pair `number + number` (`number`, or `null` on overflow) and the pair `null + number` (`null`). For numbers the operation runs on the sets: `Feel.Analysis.Intervals` gives the interval of what `+ - * /` can produce, and says whether `null` is possible for lack of range (overflow past decimal128, a zero divisor, a result too small to write). The ends of a result are computed by the runtime's own arithmetic, so the rounding to 34 digits is the run's, and the ends are always included, which can only make a set larger.

The same expressions for names that are plain numbers, and for names whose scope declares allowed values (`age` in `[0..150]`, `d` in `[1..10]`):

| Expression | no allowed values | with the allowed values above |
| --- | --- | --- |
| `age` | `number \| Null` | `number in [0..150] \| Null` |
| `age + 1` | `number \| Null` | `number in [1..151] \| Null` |
| `age * 2` | `number \| Null` | `number in [0..300] \| Null` |
| `age > 200` | `boolean \| Null` | `boolean = false \| Null` |
| `age < 200` | `boolean \| Null` | `boolean = true \| Null` |
| `100 / d` | `number in [-max..-1E-6143], [1E-6143..max] \| Null` | `number in [10..100] \| Null` |

The last row shows the hole at zero that the divisor's set leaves (the bounds are abbreviated here: they are `-max`, `1.000…E-6143` with 34 digits, and `max`), and that a divisor whose set does not contain zero adds no `Null` of its own. The `\| Null` that remains is the name's: a bound `d` may be `null`.

An operand that has no order (a boolean, a list, a range, a context, a function, or a term that is no value of FEEL) is `null` for the four orderings whatever the other operand is, and so against `Any`, `Any | Null` and a named type (D-196): the run takes a pair of one such kind as an error, a pair of kinds that differ as a mismatch, and a `null` as `null`, so `true < v` and `true <= v` are `Null` (a mismatch, with a warning) for every `v`. The pairs are typed one by one, as ever, so a union is `Null` only if every pair of its alternatives is (`number | boolean` against `Any` is `boolean | Null`: the number can be above or below). `OrderingKindsTest` checks this against the runtime's table for every pair of kinds. The supported interpretation follows the domain table rather than using the alternative formula `a <= b` as `a < b or a = b` outside the ordered kinds. That formula would make `true <= true` true; both runtime and inference instead give null (D-196).

An operand of a kind that an arithmetic operator has no operation for is `null` whatever the other operand is, `Any`, `Any | Null` and a named type included (D-203), for the same reason: the run takes a pair with it as a type mismatch (and a `null` as `null`), so `true + v`, `{a: 1} * v` and `[1] - v` are `Null` (a mismatch, with a warning) for every `v`. A boolean, a list, a range, a context, a function and a term that is no value of FEEL have no operation at all; a string has `+` and no other (`"a" - v` is `Null`, `"a" + v` is `string | Null`: the `v` that is a string); a date, a time and a date and time have `+` and `-` (`d * v` is `Null`); a duration has all but `**`; only a number has `**`. The kinds are what the runtime's table says, and `ArithmeticKindsTest` checks the types against it for every pair of kinds. A union is `Null` only if every pair of its alternatives is.

A kind that has an operation against one that is not known (D-203) is a value of the kinds that its pairs give with a kind of the unknown one, and `null`: the unknown one is a value of every kind, and the run gives a value for the pairs of kinds that the tables name only. So `x + v` is `number | Null` (a number is added to a number only), `s + v` is `string | Null`, `d + v` is `date | Null`, `ym + v` is `date | date and time | years and months duration | Null` (a years and months duration is added to a date, a date and time and a years and months duration), `dd / v` is `number | days and time duration | Null`, `x * v` is `number | years and months duration | days and time duration | Null`, and `v + w` is the seven kinds that have a `+`, and `Null` (`v - w` has six of them, `v * w` and `v / w` three, `v ** w` one). The type is the union over the kinds of the unknown one of what the pair of the two kinds gives, so it is never narrower than the run, and no wider than the kinds say; the set of values of the known operand does not cut it (`x` in `[0..10]` makes `x + v` the same `number | Null`).

A negation has one operand, so no other to say what `v` is, and the run negates a number and the two durations only (D-207): `-v` is `number | years and months duration | days and time duration | Null`, the kinds of a negation (a string, a date, a time and a date and time have none: `-s` is `Null`, as ever). One `v` read twice (below) is one value of one kind, and the run gives for a value against itself `v + v` a number, a string, a years and months duration or a days and time duration (two dates are not added), `v - v` a `0` of a number, of a years and months duration or of a days and time duration (a date, a time and a date and time minus themselves are a days and time duration), `v * v` a number (a duration times itself is not defined), `v / v` a number (a duration over itself is one), and `v ** v` a number, and `null`: it is the union over the kinds of the pair of that kind with itself, and not of the pairs of two kinds (`v - w` has the six kinds, for a date and a duration are a pair).

In full analysis, the pairs are of two values unless the operands are **one value** (D-170): a name read twice, a member of one, a local. `age - age` is `0`, not the difference of two numbers of `[0..150]`, `d / d` is `1` (and `null` for a `d` that is `0`), `age * age` is not below 0, and `age + age` is `2 * age` (a set with a gap in it does not add its intervals to each other):

| Expression | the two reads as two values | as one value |
| --- | --- | --- |
| `age - age` | `number in [-150..150] \| Null` | `number = 0 \| Null` |
| `d / d` | `number in [0.1..10] \| Null` | `number = 1 \| Null` |
| `age < age` | `boolean \| Null` | `boolean = false \| Null` |
| `age >= age` | `boolean \| Null` | `boolean = true \| Null` |
| `p = p` | `boolean \| Null` | `boolean = true` |
| `v - v` (`v` of type `Any`) | `number \| date \| time \| date and time \| years and months duration \| days and time duration \| Null` | `number = 0 \| years and months duration = P0M \| days and time duration = PT0S \| Null` |
| `v + v` (`v` of type `Any`) | the seven kinds that have a `+` and `Null` | `number \| string \| years and months duration \| days and time duration \| Null` |
| `ym / ym` (a duration of years and months) | `number in [-9999999999999999999999999999999999..9999999999999999999999999999999999] \| Null` | `number = 1 \| Null` |

For `ym / ym`, a non-null duration gives one only when its month count is nonzero and has magnitude less than `10^34`. Larger magnitudes fail the runtime's numeric conversion, even though the formal quotient would be one. Inference keeps null for that failure and for zero; if every possible month count fails, the result type is `Null`. A non-null declaration alone does not eliminate those failures.

A duration with a set of values added to itself is twice a value of the set, as `x + x` is for a number: a duration that can be either one or six months gives two or twelve months for `ym + ym`, not also seven, and the seconds are the same (D-207). The core analysis tier keeps independent-operand types for repeated reads.

Unary-test lowering uses inferred kinds only when that preserves dynamic matching's meaning. A nullable scalar expression that reads `?` keeps a null result as an unknown answer, so `-?` and `if b then -? else []`, with `b` true, both remain unsatisfied on null input with the original arithmetic diagnostic. A null literal and explicit `? = null` keep ordinary equality (D-40, D-209). Inferred precision must not change which null rule applies.

The same holds for the orderings and for a declared context (D-170): a number, a string, a date, a time, a date and time or a duration is neither less than itself nor greater, and is less or equal and greater or equal, and an ordering with a `null` is `null`, so `age < age` is `false` or `null`, and `k < k` for a `number!` is `false`. A context is equal to itself whatever its entries are, an open one (a declared type) included, since the run answers `true` for a context that is the same term before it looks at an entry (D-168). A boolean, a list or a range has no order (`b < b` is a mismatch, as ever), and `Any` is not known to be a value of FEEL (`v < v` is `boolean | Null`).

A relation between two names is held by the bounds only: `age` that allows `<= max age` is cut by the highest `max age` there is, where the test reads `max age` as it is verified, so that the type of `max age` is true of what the test sees (D-170).

### 5.2 Why a result can be `null`

The analysis tries to explain a possible `Null` by finding operands that cause it (D-161). This search is bounded and incomplete; a remaining `Null` need not have a discovered witness. Take three names declared `number!`: a price `p` of at most two decimals in `[0..1000]` (`? >= 0 and ? <= 1000 and round half up(?, 2) = ?`), a whole quantity `q` in `[1..99]` (`floor(?) = ?`), and an `r` in `[0..1000]` with any number of decimals. `p * q` is `number in [0..99000]`, with no `Null`, and `p * r` is not:

```
p * q    number in [0..99000]
p * r    number in [0..1000000] | Null
  info operand_near_zero: the result can be null: a result too small to write when p = 0.5 and r = 1E-6176
  hint: allowed values that keep p and r away from zero rule that out, for example a lower bound of 0.001
```

The info is given for an operation whose operands cannot be `null` themselves (a name that may be `null` has the `Null` of its own, and says nothing more), and its code says what would rule the `null` out (D-161): `:operand_near_zero`, `:operand_too_large`, `:operand_unbounded`, or `:null_possible` for the rest. The reasons are found by running the operation. `Feel.Analysis.NullReasons` takes the values at which an operation fails (`Feel.Type.Witness.edges/2`: zero, the smallest numbers there are, the ends of the sets, the largest number, the first and last day of the calendar), runs it on every pair, and keeps the first pair the run turns down for each cause:

| Cause | The run's code |
| --- | --- |
| a division by zero | `:division_by_zero` |
| a result too large to write | `:overflow` |
| a result too small to write (a digit below 1E-6176, D-59) | `:overflow` |
| no value for a power (a negative base to an exponent that is not whole) | `:argument_out_of_domain` |
| an amount of 34 digits or more | `:argument_out_of_domain` |
| a year out of the calendar | `:date_out_of_range` |
| a zone on one operand only | `:offset_mismatch` |

So a reason is a fact and not a guess: the pair is in the types of the operands and the run says `null` for it. A call of a built-in is searched in the same way (`NullReasons.find_call/3`, the code `:null_possible`, the function in `details.function`): the function is run on up to 256 combinations of edge values for a call, and 20,000 in an analysis. The search is sound and not complete (a cause whose values are not at an edge is missed); it also tests the sets from the other side, since a set that says `null` where no pair of edges does it is not exact there.

What takes the `Null` of a product away in the example is the **grain** of a number (D-161, step D): every number of a node is a multiple of `10^-d`. A literal has its decimals, a name has the grain its allowed values say (`round half up(?, 2) = ?` is 2, `floor(?) = ?` is 0, `modulo(?, 5) = 0`, `even(?)`), a sum has the larger of its operands' grains, a product their sum, and `floor`, `ceiling`, `round *`, `decimal`, `count` and `string length` give theirs. A number of a grain is zero or at a distance of `10^-d` from it at least, so a product of two with grains that add up to 6176 or less is never too small to write. The grain is a fact of the *node* and not a part of the type, as the length of a list is (D-193): a set of the multiples of a step is not an interval.

### 5.3 Narrowing

To inspect a bound, read the typed IR, rather than projecting it through the public FEEL type:

```elixir
scope = Feel.Scope.new(%{"x" => :number})
{:ok, expression} = Feel.prepare("if x > 5 then x else 0", scope: scope)
Feel.type(expression) #=> :number
expression |> Feel.Expression.unoptimized_ir() |> Feel.IR.type() |> Feel.Type.Union.format()
#=> "number in 0, (5..max]"
```

The tables in the [narrowing catalog](narrowing.md) use full analysis and enforcing declarations. Core analysis keeps broader bounds; runtime outcomes still follow the same contract. Preparation warnings describe inferred types and need not be identical between tiers. Runtime diagnostics and observable function signatures are covered by the separate tier-stability contract (D-219).

`Feel.Analysis.Narrowing` reads what a condition says about the names in it (D-194); [narrowing.md](narrowing.md) has the rules, and a page for each kind of value. A *fact* is a function from the type of a name to the alternatives that are left, and it only ever takes alternatives away or makes a set smaller. After `x > 5` is true, `x` is a number above 5 and not `null`; after `y != 0`, `y` is not 0. Facts come from comparisons, `between`, `in`, `instance of`, a name that is a whole condition, and `and` / `or`, which meet and join the facts as the logic does. They hold in the branches of an `if`, in the right operand of an `and` or an `or`, and for a path (`p.age`) and for a local (D-65, D-193).

```
x > 5 and x < 3                            boolean = false | Null          x < 3 is read with x above 5
if x > 5 then x else 0                     number in 0, (5..max]           the then-branch above 5, the else a point
if x != 0 then x else null                 number in [-max..0), (0..max] | Null
if s != "a" then s else null               string except "a" | Null
if n != 5 then n else null                 number in [0..5), (5..10] | Null          n allowed in [0..10]
if v instance of number then v else 0      number                          v is Any; a null is not a number
if x != null then x + 1 else 0             number                          never null: x + 1 cannot overflow
if x between 1 and 10 then x else null     number in [1..10] | Null
if p.age > 18 then p else null             context<age: number in (18..max], name: string | Null> | Null
```

The last line is the narrowing of a *path*: the fact is about `p.age`, and it shows up in the type of the context `p`. A comparison of an operation is read backwards by `Feel.Analysis.Preimage` (D-122): `x + 1 > 5` leaves `x` above 4, and `n + m > 150` for `m` in `[0..100]` leaves `n` above 50.

A comparison of a call of a built-in leaves, for an argument of type `Any`, the kinds for which the rule of the call gives a value of the kind the other side has, taken kind by kind with a function and a term that is not a value of FEEL among them (D-155): a list function makes a list of any value, so `append(v) != null` leaves `Any`, a function too, and a type that left it out was a check the optimizer then took away.

A condition that is decided removes a branch. A branch in which a read finds that the facts leave its name no value is out of the type of the `if` (D-152), and gets an `unreachable_branch` warning with the span of the branch (D-173; `if floor(x) = 2.5 then x else 7` is `number = 7`); a condition whose own type is decided gets a `decided_condition` warning, which says it for the condition, so the two never say the same branch. Neither is said for a constant condition (`if true`), which is how a branch is switched off. A branch that is taken out cannot run, so every node in it is `Never` (D-173), and not the type it was given under facts that no run has. The body of a `for`, `some` or `every` over a list that is known to have no element never runs either, and its nodes are `Never` (D-170, `every i in [] satisfies i > 2`), and so are the domains after a domain that has none, which a loop does not read (D-170, `for i in [], j in null return j` is the empty list):

```
if x < 4 then (if x > 5 then x + 1 else 0) else 1        number in 0, 1
  if x > 5 then x + 1 else 0                              number = 0
    x > 5                                                 boolean = false      x is number in [-max..4) here
    x + 1                                                 Never                and so are x and 1 in it
    0                                                     number = 0
```

The branches:

```
if n > 10 then 1 else 2            number = 2        warning: the condition is never true; the then branch never runs     (n in [0..10])
if v instance of list<number> then 1 else v     Any except list<number | Null> | Null          (v is Any; the else is a kind less some of it, 3.5)
```

A branch that reads none of the names its facts are about stays in the type, unless its condition compares a call of a rounding function, `exp` or `log` (`if floor(x) = 2.5 then 5 else 7` is `number = 7`, D-194): applying the facts at every `if` costs 20 to 65 per cent at the least, and the comparisons that the facts say more of than the types are those of such a call.

The shape of the algorithm is the shape of *abstract interpretation*: sets of numbers are an interval domain, the arithmetic of `Intervals` is its transfer function, the cap of 16 intervals is a widening, and `Preimage` is the backward transfer function used to refine a condition. One place does it by the book. In `for i in 0..4 return if i = 0 then 1 else i * partial[-1]`, the type of `partial` (the results so far) depends on the type of the body, which depends on `partial`, so the analyzer iterates to a fixpoint: it starts from a list of nothing, types the body, takes what the body can be into `partial`, and types again until the body is within it. From the second round on the sets of values are given up, because `i * partial[-1]` never stops growing, and after the third round the results are `Any` (`partial_fixpoint` and `widen` in [`analyzer.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/analyzer.ex)).

### 5.4 Declarations: what a scope says

A `Feel.Scope` gives the names their types and says what a bound value has to satisfy. An **allowed value** is the source of a list of unary tests, as in the `allowedValues` of a DMN item definition, and a **type constraint** the same for the value as a whole (for a list, `count(?) > 0` is for the list, where allowed values are for each element, D-51). A unary test is a condition of `?`, so a constraint narrows by the rules of the narrowing pages (D-161, step A): `? * 2 < 100` as an allowed value narrows as `x * 2 < 100` does in a condition. Both can be given for a **member** of a value by a subject `{name, steps}`, where a step is a key of a context or `:each` for the elements of a list (D-161, step E), and a source may be a list of texts that all hold:

```elixir
scope = Feel.Scope.new(
  %{"person" => {:context, %{"age" => :number, "name" => :string}},
    "orders" => {:list, {:context, %{"total" => :number}}},
    "grid" => {:list, {:list, :number}}, "xs" => {:list, :number}},
  allowed_values: %{
    {"person", ["age"]} => "[0..150]",
    {"orders", [:each, "total"]} => "[0..1000]",
    {"grid", [:each]} => "> 0"},
  type_constraints: %{"xs" => "count(?) > 0"})
```

| Expression | Type |
| --- | --- |
| `person` | `context<age: number in [0..150] \| Null, name: string \| Null> \| Null` |
| `person.age + 1` | `number in [1..151] \| Null` |
| `orders.total` | `list<number in [0..1000] \| Null> \| Null` |
| `grid[1][1]` | `number in (0..max] \| Null` |
| `xs` | `non-empty list<number \| Null> \| Null` |
| `count(xs)` | `number in [1..max] \| Null` |

The run makes the types true (D-138): when it starts it checks the bound value of each name the expression reads, and a value that a test does not accept is `null` with a `:value_not_allowed` error, `null` itself being exempt. For a member the first one that is not allowed makes the whole value `null`, and the error says which: `the value of "orders[3].total" is not one of its allowed values`. A name declared `!` ends the run instead. What a run does with a value that does not fit, and whether the constraints narrow the types, is the *stance* (`:declarations`, D-138; section 6). `Feel.ItemDefinitions.scope/2` makes a scope from the item definitions of a model, with the constraints of each definition, of its components and of a collection's elements.

The declared type of a name may be a negation or a union (section 2, D-178). The stances treat it as any other: `:enforce` and `:enforce_wide` convert the bound value or make it `null` with a `:type_mismatch`, `:audit` and `:report` leave it and report it, `:trust` and `:ignore` rely on the host. With `x` declared `Any except number`, `x + 1` is `Null` with a `type_mismatch` warning, where `Any` gave `Any | Null`, and `if x instance of string then x else null` is `string | Null`; with `u` declared `number | string`, `u + 1` is `number | Null` and `if u instance of number then u + 1 else 0` is `number`. The allowed values of such a name are enforced and do not narrow it (5.7).

### 5.5 Calls: built-in functions and functions of FEEL

A call of a **built-in function** starts with the type its signatures give (result kinds and `Null`), refined by a result *rule* (D-161, step C): `Feel.Analysis.Images` has a module for each family (booleans, contexts, conversions, lists, numbers, ranges, strings, temporal values), each registered built-in has a rule, and each rule is held to the run on the values at the edges of the types of its arguments (`Feel.ImageCheck`). These tests check containment and selected null witnesses on the exercised inputs; they do not establish exact result sets for every argument combination.

```
string length(s)                       number in 3, 4, 5 | Null          s allows "red", "green", "blue"
upper case(s)                          string in {"BLUE", "GREEN", "RED"} | Null
not(b)                                 boolean                            b is boolean!
abs(k)                                 number in [0..5]                   k is number! in [-5..3]
date("2024-05-01") + duration("P1D")   date = 2024-05-02
```

A comparison of a call narrows its arguments by their kinds, for every built-in with a rule: `string length(s) > 0` leaves the strings but `""` (`if string length(s) > 0 then s else null` is `string except "" | Null` for a `s` that has no allowed values, and for a `v` of `Any` the same with the lists: `string except "" | list<Any | Null> | Null`).

A **function of FEEL** has a type: `function(a: number, b: number) a + b` is `function<number | Null, number | Null> -> number | Null`. A call of one written in the expression, called at once or through the key of a context, is typed by analyzing its body again with the types of the arguments (D-193), so `(function(a: number, b: number) a + b)(n, 1)` for `n` in `[0..10]` is `number in [1..11] | Null`. That goes no deeper than three calls, and a call that repeats an earlier one has its type. A name declared with a function type is typed by its arrow, which knows nothing of the sets (`f(n)` for `f: function<number> -> number` is `number | Null`). A call with another number of arguments is `Null` with an `arity_mismatch` warning when the actual function values are known from syntax or the built-in registry; through a function or overload type alone it starts at `Any | Null`, since recorded arrows may omit signatures (`ceiling` takes a scale, D-171). The same applies when recorded arrows have the right arity but do not cover every argument's domain: another same-arity signature can succeed. Applicable call refinements can still narrow the result. Linked recursion carries separate single-signature callee evidence. Members are prepared again with their original settings before link signatures are probed; only the peer bindings constructed by `Feel.Recursion` receive this evidence, and local shadowing does not inherit it. Thus a self-call with an `Any` argument can keep its declared numeric result without treating a host extension's partial signature list as complete. Completeness is a fallback beside closure identities: discovery through contexts, list indexes, conditionals and iterator domains still specializes known literal bodies for their arguments. Forwarded containers prefer their retained shapes over compact completeness. Named calls of complete peers keep the written result or `Null` when they supply at most the parameter count; more names give `Null`. Omitted parameters can be null, while unknown or duplicate names still fail runtime binding. Names are not inferred from the arrow type. Context-entry containers retain completeness before aliases are bound, even when their detailed shapes exceed the 32-entry limit. If a known literal cannot be specialized because the three-call depth or source budget is exhausted, its marked complete signature still bounds the call. This uses its written result and possible null, without further specialization or treating an ordinary host declaration as complete. Descendant selection preserves this evidence when every function contained in the source is known complete: `({g: f}...g)[1](n - 1, v)` retains a linked peer's result bound just as an ordinary path does. Partial host functions and unknown containers do not acquire completeness from their declared arrow types. A function that a call gives and that its body writes is the overload of the arrow as it was written, with the arrow typed for the arguments of the call as a refinement (D-171). Literal functions use this signature/refinement separation from their first analysis; the [check-bypass example](type-system-analysis.md#21-function-signatures-and-call-refinements) is kept as a regression. A built-in function with several observable signatures, used as a value, is an overload (3.5; `not`, `count` and `upper case` are plain function types). `abs` does not itself satisfy `function<number> -> number`, but declaration conversion can select its numeric signature and produce a function enforcing that contract (D-197). For a call without that conversion: `(function(h: function<Any> -> Any, ys: list<number>) for x in ys return h(x))(abs, xs)` is `list<number in [0..max] | Null> | Null`, since `abs` has a refinement for numbers (the other overloads, such as `floor`, give `list<Any | Null> | Null` there). Returned containers can still lose built-in call summaries, so `{fs: (function() [abs, floor])(), r: fs[1](n)}.r` is `Any | Null`. This is separate from keeping literal FEEL closures' signature/call distinction inside their types. A written list or context bound to a name also keeps known functions beside its type (D-193). There are no type variables, and a function written in FEEL has no declared result type.

A returned list or context still does not preserve every nested callable shape. For a newly created function inside such a container, call analysis restores the written parameters and an `Any | Null` result. Matching an arrow in an argument or unrelated entry is not proof of identity. It must not export a specialized body arrow as observable metadata (D-203). Nested overload arrows participate in this fallback too. Callable precision beyond the retained shapes remains open work.

Named calls through function types are `Any | Null`, since parameter names and the complete signature list are absent. Known function values still use their own binding rules. Callee identities passed to a parameter are retained only when conversion cannot replace the function: restricting `abs` to its numeric signature changes which calls it accepts. Specialized closure arrows are call facts; equality with an argument's arrow does not prove that the same function was returned. Alternative returned function signatures remain a union; combining them into an overload would incorrectly require every signature. Ambiguous alternatives keep their broader written types. [Section 2.7](type-system-analysis.md#27-readers-of-function-types) states the reader rules and the conservative precision tradeoffs.

A callee that **says which function it is** is not typed by its type but by the functions (D-193). The node of the callee is a key of a context literal, an item of a list literal or a branch of an `if`, and it is read (`Feel.Analysis.Callees`): each function literal in it is analyzed again for the arguments as one written at the call is (D-193), each built-in function is typed as its call by name would be (the rule of its family, above), and the call is any of them, `null` too where the callee or an argument may not fit. So `{g: function(a) a * 2}.g(x)` and `[abs, floor][1](x)` are `number | Null` (they were `Any | Null`), `(if b then abs else ceiling)(age)` is `number in [0..150] | Null` for an `age` in `[0..150]` (it was `number | Null`), and `(if b then function(a) a * 2 else function(a) a + 1)(3)` is `number in 4, 6`. At most 4 alternatives are read, and 64 KiB of function source are analyzed again for them in one analysis; past either the call is typed by the type of its callee.

A name keeps the functions too (D-193). The analysis keeps what it knows of a list or a context that a name is bound to beside its type, in the **shapes** of its structure (D-193: the shape of each item and of each entry), and the shape has the functions that the node of the item or entry says (`callees`). So `{fs: [abs, floor], r: fs[1](x)}.r`, `{c: {g: function(a) a * 2}, r: c.g(x)}.r` and `fs[1].g(3)` for a list of contexts are read from the name as they are at the call, four deep; the iterator of a `for`, `some` or `every` over a list of functions is any of them (`for f in [abs, floor] return f(x)` is `list<number | Null>`), and a parameter that a call gives an `if`, an item or a key of functions is any of them (`(function(f: function<Any> -> Any, y) f(y))(if b then abs else ceiling, x)` is `number | Null`; it was `Any | Null`). The shape is not part of a type, so the functions are not lost to D-152.

A call that gives a function says which (D-193): the body of a function that is analyzed again for a call says what it gives when it is a function written in it, an `if` of them, a name that has them or a call that gives them, and the node of the call keeps it beside its type (`callees`). So `{g: function(a) function(c) a + c}.g(1)(2)` is `number = 3` through a key, a list item, an `if`, a name or a parameter, as `(function(a) function(c) a + c)(1)(2)` was, and a call that gives a value that may not be a function is typed by its type. A list or a context literal that is selected from more than once (`{fs: [abs, floor]}.fs[1](x)`) and a parameter that is given a list or a context of functions (`(function(fs) fs[1](x))([abs, floor])`) are read as a name that holds the value is.

<a id="56-what-the-types-are-used-for"></a>

### 5.6 What the types are used for

**Diagnostics, for what is certain.** An operation is a `:type_mismatch` warning at `prepare/2` only when *every* pair of alternatives without a `null` operand is a mismatch. A `null` operand excuses a pair, and a mismatch that only some pairs have is not reported.

| Source (`x` a number, `v` any, `b` a boolean) | Type | Warnings |
| --- | --- | --- |
| `1 + "a"` | `Null` | `type_mismatch` |
| `x + "a"` | `Null` | `type_mismatch` |
| `b + v` | `Null` | `type_mismatch`: a boolean has no `+`, whatever `v` is (D-203) |
| `v + 1` | `number \| Null` | none: `v` is a number or not, and a number is added to a number only (D-203) |
| `(if b then 1 else "a") + 1` | `number = 2 \| Null` | none: only one pair is a mismatch |

Preparation warnings and runtime diagnostics serve different purposes. A statically impossible built-in call is typed as `Null` and may warn using the inferred argument types. It keeps ordinary runtime validation, whose error message and details describe the actual values. They agree across analysis tiers, including in strict mode. Structural call errors such as invalid arity instead carry a fixed diagnostic in the IR. Preparation warnings themselves are allowed to differ across tiers.

**The optimizer** (D-45) removes a runtime check when the type has already settled it. The scope's declarations become wrapper nodes around the expression (`allowed`, `conform`, ...); after optimizing, the ones that the types prove are gone:

| `age` in `[0..150]`, expression `age + 1` | Analyzer's root | Optimized root |
| --- | --- | --- |
| result allowed `[1..151]` | `allowed` | the `allowed` check is dropped |
| result allowed `[0..100]` | `allowed` | kept (`age + 1` can be 151) |
| result type `number` | `conform` | the conversion is dropped |
| result type `string` | `conform` | kept |
| `1 + 2`, result type `number` | `conform` | a constant: `3` |

**Folding.** A pure operation on constants is evaluated, and full analysis can keep its exact value (`number = 3`), so most constant sub-expressions fold away before a backend sees them.

**Decision tables.** `Feel.Rules` asks of a table whose entries are unary tests whether the rules cover the inputs, overlap, or are dead, and the interface distinguishes proved, refuted with an input, and unknown (`Feel.Type.Verdict`, D-158). A rule is bounded from outside by the inputs it may match and from inside by the inputs it certainly matches, both as types, and a column has the type of its input (one narrowed by its allowed values, for instance). Numeric certainty keeps bounded subsets instead of filling gaps; string certainty drops information at its point budget. The former 17-point false coverage, overlap and deadness claims are now regression tests. Unsupported proofs may remain unknown; witnesses are not yet universally checked against the original unary tests. DMN adapts prepared wildcard entries to their effective `inputValues`, and keeps cells depending on model/local bindings, filter fields, aliases, dynamic lookup, extensions or indirect calls unknown. The original unit's named types are preserved through the queries' optional `types: map`, including resolved or folded `instance of` tests. Standalone `Feel.Rules` callers must supply those type definitions and effective tests or explicit `:unknown` cells; that API cannot reconstruct a DMN or lexical scope from text. See DMN's [table-checking contract](https://github.com/FeeJai/BDM/blob/main/apps/dmn/docs/feel-integration.md#step-5-questions-about-a-table).

For a standalone proof using a named type, supply its definitions explicitly:

```elixir
columns = [{"x", Feel.Type.Union.of_value(Decimal.new(1))}]
rules = [["if 1 instance of N then 1 else 2"]]
Feel.Rules.coverage(columns, rules, types: %{"N" => :number}) #=> :covered
```

These diagnostics concern the supplied abstract column domains, not reachability through upstream model decisions. Silence is not a coverage or disjointness proof: a query can be unknown, skipped for table size, or contained by its time/memory guard. Rule-output narrowing is a separate consumer that analyzes an output assuming its entry matched; unknown table proofs do not justify eliminating that output or its runtime checks.

String alternatives are combined with bulk union, and negated lists with bulk intersection, before applying the lower-bound point/exclusion budget. Intervals do not count toward that budget; a fold over a growing interval set would repeat sorting and intersection work without reaching the cap. Scaling regressions measure process reductions on positive and negated lists of disjoint intervals.

**The audit.** `Feel.Paranoid.run/3` (D-159) runs the IR as the analyzer made it, with nothing taken out, and checks for every node that its value is in its type with `Union.contains?/2`; it also compares optimized execution. Result and error comparisons include every diagnostic field, in order, using recursive value equality for embedded decimals, contexts and functions. FEEL functions compare by signature metadata with their implementation closures ignored; equal metadata does not establish equal behavior. A shared membership bug can still escape the monitor.

The types therefore *change what runs*. An unsound type in this library is not a missed warning: it is a check that was removed and should not have been. This is why the [correctness assessment](type-system-analysis.md#2-contracts-and-evidence) distinguishes precision losses from invalid proofs and execution changes.

### 5.7 Current limits

The [assessment](type-system-analysis.md#2-contracts-and-evidence) distinguishes the contracts that are kept from remaining precision and verification work. Nested normalization, observable signatures, parameter projection and certainty construction now preserve the contracts described above. This does not complete the audit of every proof consumer, aggregation path, declaration assumption or observable effect.

The analysis also deliberately loses information: it has no general polymorphic type schemes or relational solver; cardinality, grain, temporal inverse rules and callable summaries are partial and bounded. Host declarations can express unions and negations that expression syntax cannot write. Non-null result constraints are rejected. Recursive item definitions default to rejection. The explicit `recursive: :guarded` mode keeps a finite graph and validates every finite descendant and component constraint. Cycles must consume a context member or list element and cannot cross a function signature. Analysis uses a structural upper approximation with a shared 256-node projection budget, which cannot justify recursive check removal or subtraction from a negative branch. Complete recursive subtyping and inference remain unsupported. The legacy `recursive: :any` mode is still explicitly approximate and does not validate the full recursive structure.

Use the [narrowing catalog](narrowing.md#13-does-it-narrow-as-far-as-it-can) for concrete precision cases and the [maintained backlog](todo.md) for open work. The decision record explains current choices; Git keeps earlier limits and implementation stages.

## 6. Keeping it sound

Under valid assumptions, an inferred possible-result type must contain every returned value. Making such a positive bound larger sacrifices precision. The same direction does not apply unchanged to certain rule inputs, negative positions or observable effects. The [assessment](type-system-analysis.md#33-negation-and-variance-determine-the-direction-of-approximation) states the obligations and lists the remaining audit work.

Representation budgets bound selected work: numeric/temporal intervals, finite strings, structural exclusions, overloads and callable reanalysis all have caps. Replacing a positive bound by its hull can be safe locally while complementing that hull is unsafe. Shrinking a fact alone does not prove it valid, and failure of `subtype?` can mean the algorithm could not establish inclusion.

The test evidence comes from complementary checks:

| Evidence | What it exercises |
| --- | --- |
| Operator, image and narrowing tests | Runtime values against inferred bounds on selected operands and bindings |
| Construct suite and documentation tables | Recorded precision examples and identified gaps |
| Type algebra tests | Selected subtype, conformance, arrow, exclusion and composite laws |
| `Feel.Paranoid` and [generated sweeps](https://github.com/FeeJai/BDM/blob/main/apps/feel/scripts/sweep/README.md) | Membership at monitored IR nodes and prepared-result agreement on finite grids |
| DMN audit and rejected-declaration sweeps | Monitored units, chained optimized results and values rejected by embedded constraints |
| Mutation checks | Handwritten wrong rules and generated changes, with survivors requiring review |
| Backend, tier and optimizer comparisons | Complete returned outcomes and diagnostics; the tier sweep compares core/unoptimized with full/optimized interpreter execution in strict and lenient modes, complemented by focused tests on both backends |
| Specification, decimal128 and TCK fixtures | External examples and references with explicit provenance and accepted deviations |

The sweeps share membership code with the analyzer; that limits their independence. Mutation checks probe selected blind spots, but neither passing tests nor unchanged precision establishes a theorem. The [open obligations](type-system-analysis.md#7-open-obligations-and-extensions) gives stronger acceptance criteria, including independent oracles and cap/variance boundary tests.

Declaration assumptions also matter. With `:enforce`, the runtime checks declarations and converts or rejects invalid bindings through the declared conformance/conversion boundary. `:trust` and `:audit` narrow without enforcing, so the host must supply valid values for those inferences to hold. `:enforce_wide` checks without allowed-value narrowing; `:report` and `:ignore` do not narrow by allowed values, but still assume declared kinds. An optimization justified by an unchecked assumption inherits that assumption.

## 7. Where to read more

| Topic | Where |
| --- | --- |
| The lattice | [`type.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type.ex), [`type/conformance.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/conformance.ex), [`type/instance.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/instance.ex), [`type/conversion.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/conversion.ex) |
| The union | [`type/union.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/union.ex) |
| The sets | [`type/number_set.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/number_set.ex), [`type/string_set.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/string_set.ex), [`type/image.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/image.ex), [`type/moment.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/moment.ex) |
| Inference | [`analysis/inference.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/inference.ex), [`analysis/refinement/operations.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/refinement/operations.ex), [`analysis/intervals.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/intervals.ex) |
| A kind less some of it, functions | [`type/except.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/except.ex), [`type/arrows.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/arrows.ex) |
| Why a result is `null`, and the grain | [`analysis/null_reasons.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/null_reasons.ex), [`type/witness.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/witness.ex), [`analysis/grain.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/grain.ex) |
| The result of a built-in | [`analysis/images.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/images.ex) and the modules under `analysis/images/` (one for each family), held to the run by `test/support/image_check.ex` |
| Calls of functions | [`analysis/calls.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/calls.ex), [`analysis/invocations.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/invocations.ex) |
| Declarations | [`scope.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/scope.ex), [`analysis/allowed_values.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/allowed_values.ex), [`analysis/declarations.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/declarations.ex), [`runtime/allowed_values.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/runtime/allowed_values.ex), [`item_definitions.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/item_definitions.ex) |
| Decision tables, and the audit | [`rules.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/rules.ex), [`type/verdict.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/type/verdict.ex), [`paranoid.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/paranoid.ex) |
| Narrowing | [`analysis/narrowing.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/narrowing.ex), [`analysis/preimage.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/preimage.ex), [`analysis/test_sets.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/analysis/test_sets.ex) |
| The optimizer | [`optimizer.ex`](https://github.com/FeeJai/BDM/blob/main/apps/feel/lib/feel/optimizer.ex) |
| Decisions | [Current choices and rationale](decisions.md), organized by values, syntax, runtime behavior, declarations, analysis and compiler boundaries |