The FEEL type system

This document explains the type system in apps/feel, states which of its contracts are established and which are not, and recommends a target design and the work that remains. It complements the type-system guide, which describes usage and implementation conventions.

Stance. The type system is a substantial value analysis whose inferred types change execution: the optimizer removes a check when the inferred type already satisfies it. The contracts it keeps are in chapter 2. There is no general soundness claim; the evidence is tests, sweeps and bounded oracles, and it covers the cases they exercise.

Recommended direction. Retain FEEL's structural types, null semantics, and numeric and temporal precision. Build a small set-theoretic core that preserves declaration meaning, use explicitly bounded analysis around it, and allow execution-changing conclusions only when their assumptions and proof obligations are satisfied. Chapters 6–7 describe a proposed destination and the work needed to reach it; they do not describe guarantees the implementation already provides.

Shared worker deadlines, heap policies and transfer checks confine public preparation and execution; they do not make an inferred type a valid proof. See the security model.

Reading guide

1. How the type system works: current architecture and strengths.
2. Contracts and evidence: the contracts the analysis keeps, examples of their current behavior, and what the evidence does and does not establish.
3. The science behind the design: semantics, approximation, variance, and the Elixir research.
4. Hindley–Milner and other typing concepts: distinctions between the relevant ideas.
5. Concrete language comparisons: precedents and their relevance to FEEL.
6. Recommended target design: architectural choices, guarantees, and feature boundaries.
7. Open obligations and extensions: what is in place, what remains, priorities and acceptance criteria.
8. Primary references: research and official language documentation.

For a design review, read chapters 2, 6, and 7 first; use chapters 3–5 to examine the reasoning behind the choices. The detailed comparisons are kept together so they can be consulted independently of the delivery plan. Work-item identifiers R1–R8 throughout the document refer to chapter 7.

1 How the type system works

1.1 Types participate in execution

The compiler pipeline is approximately:

FEEL source → parser → analyzer → typed IR → optimizer → interpreter or BEAM
                         ↑
                  scope declarations

Feel.prepare/2 prepares an expression and Feel.run/3 executes it. The analyzer attaches a type to each intermediate representation node. Those types guide diagnostics, condition narrowing, function-call analysis, and optimization. The optimizer can remove a conformance check when the inferred type is already within the required type.

Consequently, an inferred type is a claim about execution, not just information for an editor. A type that includes too many possible results merely loses precision. A type that excludes an actual result can make execution incorrect after optimization. This distinction decides how serious an error in the type system is. See the architecture, analyzer, and optimizer.

1.2 Two related type languages

The implementation has two representations with different purposes:

The declared language starts with FEEL kinds: numbers, strings, booleans, dates, times, date-times, the two duration families, and parameterized lists, ranges, contexts, and functions. Acyclic named types resolve to structural types. Cycles are rejected by default; recursive: :guarded keeps finite graphs for complete finite-data membership and descendant constraints. The legacy recursive: :any policy instead cuts back references and is explicitly approximate. Non-null types, unions and negation are additional host declaration extensions. See the guarded-type contract for cycle restrictions and analysis limits.

In ordinary declared conformance, number admits both numbers and null. number!, represented as {:non_null, :number}, excludes null. This must be distinguished from instance of:

Feel.Type.value_conforms?(nil, :number) # true
Feel.Type.instance?(nil, :number)       # false
Feel.Type.instance?(nil, :null)         # true

Null is therefore not mathematical bottom in the internal value-set interpretation. It contains one value. Internal bottom is [], often called Never; [:null] is the singleton containing null. Similarly, [:any] describes non-null values, while [:any, :null] is the full internal universe. That universe also accommodates foreign host values.

Union.from_spec/1 translates declarations into analysis types. Union.to_spec/1 projects analysis types back into the less expressive declared representation. These operations are not inverses: projecting a numeric interval back to number, for example, forgets its bounds. Such forgetting needs a variance-aware contract; it is not automatically safe inside every type constructor. See Type, Union, and Composite.

1.3 Structural conformance and conversion

Lists and ranges are covariant: making their element or endpoint type broader makes the whole type broader. Contexts have width and depth subtyping. A context with all the required keys, appropriately typed values, and additional keys conforms to an open context declaration. A nullable field still requires the key to exist.

Functions have contravariant parameter types and covariant result types. A function that accepts more inputs and promises more specific outputs can satisfy a weaker function contract. Parameter names do not affect conformance.

Conversions are a separate relation. At applicable declaration boundaries the runtime can unwrap a singleton list, wrap a value into a singleton list, or convert a date to a date-time. A conversion is considered only when the value does not already conform. An additional TCK-driven conversion can select a type-specific built-in signature, currently used for abs. It produces a new function that enforces that signature's arguments; it does not make the original function an instance of the selected arrow (D-197). Composite declarations have additional restrictions on which conversions are attempted. Conversion and its diagnostics should not be silently equated with subtyping. See Conformance and Conversion.

1.4 Internal sets and refinements

An internal union is a list of alternatives. It can distinguish true from arbitrary booleans, an interval from arbitrary numbers, and a particular string from arbitrary strings. Structural members contain further unions:

[:number, :null]
[{:list, [:number, :string]}]
[{:context, %{"amount" => [:number], "note" => [:string, :null]}}]
[{:function, [[:number]], [:string]}]

These examples omit many refinements but show the recursive representation. There are also closed contexts, symbolic differences of the form {:except, base, exclusions}, and overloaded function descriptions. The latter distinguish required arrows from additional facts useful for analyzing calls.

The empty list has its own representation, {:list, []}. It is a value even though its element type has no values. A nonempty-list refinement excludes this value from a broader list type.

Types derived from values are not generally singleton descriptions of those values. For example, recording that a nonempty list contains elements from {1, 2} does not fix its length, ordering, or multiplicities. Documentation that calls every such result “exact” needs this qualification.

Normalization merges overlapping scalar sets, removes redundant alternatives, and sometimes discards detail. Resource limits include a cap of 16 numeric intervals and a cap of 64 string-set pieces. Larger numeric unions can become their convex hull. Other limits bound structural and function reasoning. These are useful engineering controls, but their correctness depends on where approximation occurs. See Union, NumberSet, StringSet, and Arrows.

1.5 Inference and conditions

Inference combines operator rules with the possible values of operands. It can propagate interval bounds, identify impossible combinations of kinds, and include null where an operation may fail. Full analysis uses value refinements; core analysis keeps less detail. Neither mode is an independent guarantee of soundness.

Conditions supply facts about individual occurrences of variables and paths. Inside the true branch of x instance of number, the analyzer can remove non-numeric alternatives from x. Compound guards combine such facts. Binding identities distinguish variables that happen to share a name, preventing a fact about one binding from being applied to a shadowing binding.

FEEL's treatment of conditions matters: only true selects the then branch. The else branch includes cases where the condition is false or null. Thus the else branch of x > 5 does not, without further assumptions, establish that x is a number at most 5. See Inference and the narrowing guide.

Matching decision-table entries contribute facts to their rule's outputs (D-195). Negative entries use the predicate's false outcome rather than its false-or-null outcome; earlier columns and failed prior FIRST rules do not yet contribute facts to subsequent analysis.

Numeric refinements model the runtime's decimal arithmetic rather than ideal real arithmetic. Directed rounding protects interval bounds, while additional grain information records discrete numeric structure. Temporal refinements map values to numeric coordinates; some temporal values require several related coordinates. These abstractions can preserve useful bounds without capturing every relation between coordinates. See ExactNumber, Grain, Image, and Moment.

1.6 Declaration assumptions and rule analysis

The declaration stance determines which assumptions the analyzer may rely on and what happens to invalid inputs. This table describes full analysis; core analysis does not narrow by allowed values and rejects :trust and :audit:

Declared kinds still inform analysis in the latter modes. Keeping a value that violates an assumed declaration does not make the inferred type contain that value. Soundness must therefore state its assumptions about the host and stance. In particular, reporting a violation is different from enforcing the assumption that justified an optimization. Non-null declarations have special handling: their null alternative is removed only under enforcement. See Declarations.

Decision-rule analysis adds another important distinction. It needs both values a test may accept and values it certainly accepts. Possible sets support conservative exclusion of cases; certain sets support coverage and overlap claims. A single operation that always enlarges sets cannot safely implement both roles. See TestSets and Rules.

1.7 What is already strong

The architecture contains several valuable foundations: explicit nullability internally, separate conversion rules, dedicated numeric and temporal domains, identity-aware narrowing, two execution backends, and a monitor that checks intermediate values against inferred types. Feel.Paranoid also compares optimized execution with the unoptimized interpreter, including diagnostics.

The analysis includes three-outcome facts and stored-condition origins (D-194), rule-output narrowing (D-195), ordered-kind and unknown-arithmetic inference (D-196, D-203), built-in signature conversion (D-197), result-compatibility checks (D-198), date and duration refinements (D-204), unknown negation and repeated-value arithmetic with month-duration self-division failures (D-207), and linked recursion with per-run closure reuse and diagnostic origins (D-200, D-201). Returned nested functions are widened where their written shapes cannot be preserved (D-203).

Verification combines ordinary tests, full sweeps available on demand, checked documentation tables, whole-model chain audits, rejected embedded declarations and generated mutations. These exercise different obligations; none makes the others redundant. Experiments found no failures in 5,000 numeric Boolean-law trials below the cap, 5,000 string-law trials and 5,000 directed-rounding trials. The cap contracts in chapter 2 explain why passing below-cap grids cannot establish the algebra globally.

This is substantial empirical evidence for the exercised cases. It is not evidence that untested combinations are sound. The contracts in chapter 2 show why an independent oracle and boundary-focused generation are necessary.

2 Contracts and evidence

Each section states a contract that the analysis keeps, the reason it matters, an example of its current behavior where one helps, and its limits. The first three contracts matter most, because breaking them removes an executable check or produces a definitive rule-analysis answer that is false. The others fix the meaning of types or of the algebra over them. Elixir snippets can be evaluated in an iex -S mix session at the repository root after the usual dependency setup.

2.1 Function signatures and call refinements

A function literal carries two separate descriptions, and only one of them is observable. Its runtime signature is an arrow, Union.to_spec(IR.plain_type(body)), taken from a kind-only analysis of the written environment and stored in the function node's meta.returns. Its call refinement is the precise result of the body, which holds for calls. Signature predicates (instance of function<...>), function membership and callback acceptance read the arrow only. Both backends build the runtime function's result metadata from meta.returns.

The signature is stable. It does not change with condition facts, call specialization or optimization, because private occurrence keys tell literals apart even when their source spans coincide. Using plain_type is intentional: exclusions (:except) in the body never become promises of the runtime signature. Each analysis pass keeps its own specialization budget and clears its preparation-local memo state afterwards.

With v: Any bound to 5, this predicate is false in core and in full analysis:

(if v instance of number then (function() v) else (function() 1))
  instance of function<> -> number

The consequence is that the observable signature can be broader than the body result, while a justified call result stays precise. For v = true, a sort callback selected from if v instance of boolean then (function(a,b) v) else (function(a,b) a < b) keeps its written Any result signature and is rejected in either tier.

An expression whose function literal returns 1 has the signature result nullable number. It therefore does not satisfy function<number> -> number!:

if (function(x: number) 1) instance of function<number> -> number!
then 1
else "wrong"

The expression selects "wrong", and with result_type: :number every combination below returns {:ok, nil, diagnostics} with a :type_mismatch error diagnostic:

for backend <- [:interpreter, :beam], optimize <- [false, true] do
  {:ok, expression} =
    Feel.prepare(source, backend: backend, optimize: optimize, result_type: :number)

  IO.inspect({backend, optimize, Feel.run(expression)})
end

Preparation warnings for a built-in call may describe inferred types; the executable call uses the ordinary built-in validation of actual values, so its diagnostics and strict failure are the same in every tier.

This says nothing about whether runtime signature inspection is the right FEEL behavior. It says that inference must model the predicate the runtime implements. Behavioral facts about a function's body and facts about its inspectable signature are kept in different representations.

Limits. Arbitrary returned aliases, selections and containers can lose callable precision. A preserved summary must keep the empty-list alternative of a selection such as (function(fs) fs[x])([function(a) a]) when x is null. The metadata is built in two places, one for each backend; a shared construction is a possible refactor.

Coverage: the FEEL correctness suite, the DMN integration suite, the optimizer-signature regressions and the tier regressions. Relevant code: function analysis, interpreter construction, BEAM construction, type-test inference and check removal.

2.2 Variance in projection and erasure

Forgetting detail inside a function type must follow variance. Enlarging a result type weakens a promise and broadens the function type. Enlarging an accepted-input domain strengthens a promise and narrows it. Replacing every nested type by a broader one is therefore wrong for arrows.

In the implementation:

• Normalization keeps nested exclusions and function domains. There is no plain_parts/1.
• Public function projection (Union.to_spec/1) preserves outer non-null parameters and keeps an arrow only if the projected domain is within the original domain. Otherwise it returns Any for the whole function. function(x: number!) 1 exports the parameter domain number!.
• Set erasure applies the same variance check and falls back to the internal :function kind where necessary.
• Function membership compares runtime arrows directly and does not go through the lossy projection.

When no safe parameter approximation can be expressed, a broader whole-function abstraction or Any is used, never a stronger signature than the value has. For example:

scope =
  Feel.Scope.new()
  |> Feel.Scope.put_type("T", {:not, {:list, :number}})

source = "{f: function(x: T) 1}.f instance of function<Any> -> number"
{:ok, expression} = Feel.prepare(source, scope: scope)

The condition is false at run time, so placing it in an if with a numeric then branch and a string else branch keeps the required numeric result check, also when the function sits in a context or a list. See normalization and projection.

Limits. Every remaining projection and bounded fallback through contexts, lists, overloads and higher-order parameters is part of the wider audit (R2).

2.3 Certain and possible sets in rule analysis

A rule's certain input set is a lower bound, and it never grows to fill gaps. TestSets.certain/2 returns values certainly accepted by a test; coverage, overlap and dead-rule answers rest on it. Possible sets are upper bounds and may be enlarged. A single operation that always enlarges cannot serve both roles.

• Numeric certainty unions and intersects with the :inner policy: at most 16 intervals, no gap filling.
• Certain string sets drop information when the 64-point budget is exhausted. They never widen to every string.
• These are lower bounds also for the false outcome that negated tests use.
• Positive entry lists use StringSet.union_all/2 and negated lists use StringSet.intersect_all/1, and the lower-bound budget is checked after the bulk operation. Pairwise folds over disjoint open intervals rebuild a growing range set, and interval ranges do not count toward StringSet.point_count/1, so the bulk operations are what keeps the work bounded.

With 17 isolated numeric points, a hull would claim more than the rule accepts:

alias Feel.Type.NumberSet

columns = [
  {"x", [{:number, NumberSet.interval(Decimal.new(0), Decimal.new(32))}]}
]

points = Enum.map_join(0..16, ", ", &Integer.to_string(2 * &1))

Feel.Rules.coverage(columns, [[points]])
Feel.Rules.overlaps(columns, [[points], ["1"]])
Feel.Rules.dead(columns, [[points], ["1"]])

The first rule accepts only 0, 2, 4, …, 32 and rejects 1. The queries claim neither coverage, nor an overlap at x = 1, nor deadness of the second rule; some verdicts are unknown, because an inner bound deliberately drops accepted values.

Limits. Unknown answers are acceptable. Universal witness validation is not implemented. A DMN table is checked with its prepared tests (DD-43). See certain-set construction, the numeric cap and Rules.

2.4 Nested exclusions and the readers of types

Normalization preserves exclusions inside structural members and inside another exclusion, and each reader interprets the level it inspects. An excluded declaration stays in the type. A reader that needs positive information requests a positive upper approximation at each union it inspects.

Declared membership follows the compositional reading:

type = {:not, {:context, %{"x" => {:not, {:list, :number}}}}}
value = %{"x" => [Decimal.new(1)]}

Feel.Type.value_conforms?(value, type) #=> true

[1] is a list of numbers, so it fails the inner "not a list of numbers" requirement; the context fails the excluded context type and belongs to its complement. Double negation agrees with the original: for S = list<Any except list<number>>, [[1]] is rejected by S and by its double negation.

How the readers treat excluded declarations:

Partial callback signatures. An arrow guarantees a runtime signature but does not exhaust the value's signatures: matches has both a two-argument and a three-argument form. With f declared function<string, string, string> -> boolean and bound to matches, narrowing through f instance of function<string, string> -> boolean leaves the three-argument arrow and a two-argument refinement. The same holds for f declared not function<string> -> boolean and guarded on its three-argument signature. An arity or overload without a qualifying recorded arrow is therefore uncertain for sort and list replace, and their list and null results are kept. A guaranteed two-argument Boolean arrow establishes acceptance; call refinements do not. Excluded functions use the same rule through their positive base. The callback regressions cover both list operations.

These readers can remove a required result check if they get it wrong:

scope = Feel.Scope.new(%{"x" => {:not, {:list, :number}}})
source = ~s|if context put({}, "a", x) = {a: ["s"]} then "wrong" else 1|
{:ok, expression} = Feel.prepare(source, scope: scope, result_type: :number)
Feel.run(expression, %{"x" => ["s"]})
# {:ok, nil, diagnostics}, including :type_mismatch, with and without optimization

Evidence. The reader regressions run both backends, both analysis tiers, optimization settings, strict failures and monitored intermediate types. The structural oracle interprets 120 generated declarations over a bounded value grid without calling Union for its expected answers. It checks declaration translation and positive subtype claims across 14,400 ordered pairs. The fragment has lists, open contexts, ranges, nullable and non-null marks, unions and nested negation; it excludes functions, recursive names and arbitrary host contexts. The bound-direction audit checks possible upper bounds and certain lower bounds against executed positive, negated and nested Boolean tests at 15/16/17/33 numeric alternatives and 63/64/65 string alternatives.

Limits. The composite module defines membership through its translated union, so agreement between runtime and analysis alone cannot validate the compositional meaning of nested declarations: two operations can agree with each other while sharing the wrong interpretation. That is why the oracle does not reuse Union. Iteration domains, list-element, position and flatten readers, context accessors, range relations, conversion and string images, closure summaries and structural narrowing were inspected; some handle excluded bases, others keep the type or return unknown. Broader function variance, temporal and string algebra, declaration and effect assumptions and witness validation remain obligations. Permissive declaration modes assume declared kinds even when violations are retained, so none of this is an unconditional guarantee for such inputs. See composite translation.

2.5 Numeric and string set algebra

Complement and inclusion are exact; union and intersection are bounded and say in which direction. Numeric construction, union and intersection take :outer (fill gaps), :inner (drop pieces) or :exact. Complement uses exact construction. Inclusion is exact intersection with the exact complement. Default union and intersection are :outer, so the bounded API as a whole is not an exact Boolean algebra.

Let set contain the 16 points 0, 2, …, 30:

alias Feel.Type.NumberSet

set =
  0..15
  |> Enum.flat_map(&NumberSet.point(Decimal.new(2 * &1)))
  |> NumberSet.new()

NumberSet.subset?(set, set) #=> true
(set |> NumberSet.complement() |> NumberSet.complement()) == set #=> true

The first complement needs 17 intervals, and exact construction keeps all of them. A hull would be the entire numeric domain, whose complement is empty, and subset? would fail even at reflexivity.

Exact accumulation before complement. Range proofs combine several endpoint unions that are each below the interval cap. Union.difference/2 combines numeric and numeric-image exclusions exactly before complementing; only the remaining possible-value bound may widen. An ordinary outer union of the combined exclusions would fill genuine gaps and falsely establish range subtyping. Exact complement alone cannot repair information lost earlier in accumulation. The range regressions keep gap witnesses and check membership, subtype verdicts and range plans in both exclusion orders.

Limits. Exact interval predicates can often avoid materializing a capped complement; a direct sorted-interval scan for inclusion is an optional improvement. Approximation should stay an explicit operation separate from exact complement and inclusion. The string policy (64 pieces) and the numeric sets of the temporal domains still need the audit of R3. See complement and subset.

2.6 Equivalence and join

Equivalence accepts identical terms or mutual conformance; join is a conservative common supertype, not the least one. Union extensions are not canonical terms:

a = {:union, [:number, :string]}
b = {:union, [:string, :number]}

Feel.Type.Conformance.equivalent?(a, b) #=> true

Conformance.join/2 and the public Feel.Type.join/2 promise a common supertype that contains both operands. Joining function<number> -> number and function<string> -> number returns Any, although function<Null> -> number is a strictly narrower common supertype under the implemented nullable conformance rules. That is a precision limit and an API contract, not an unsafe bound. An exact union or least-upper-bound API would be separate work with a stated supported fragment.

A failed bounded conformance proof does not establish semantic inequality. See equivalence and join.

2.7 Readers of function types

A type alone does not give the complete list of a function's signatures, so readers of function types start from Any | Null and add only what is justified. Several families of readers follow this rule.

| Positional invocation (Arrows.application/2, result/2, Invocations.result/2) | An unrecorded arity, or an unrecorded parameter domain at a recorded arity, starts at Any | Null, and matching call refinements are applied. A recorded arrow bounds the result only if it covers every argument domain. With f: function<string, string, string> -> boolean bound to matches, f("aa", "a") is true and is typed Any | Null. A truthful extension with separate text: string -> string and value: number -> number signatures fits f: function<string> -> string, and f(1) returns a number; the result is not string | Null. Known values still permit actual arity checks. | | Named invocation through a type (plain arrows, overloads, exclusions) | Any | Null: neither parameter names nor the completeness of the signature list are represented. Known values use their separate binding analysis. | | Known parameter callees (Analyzer.known_parameter?/3) | Callee identity is retained only when the argument is within the parameter type or the parameter cannot convert the function. An arrow declaration can select a restricted built-in signature: abs passed to a non-null numeric function parameter is restricted to its numeric signature, so a duration call of it is not a call of unrestricted abs. | | Returned closure signatures (Invocations.declared_closures/2) | Pair only a unique unspecialized written arrow at the top level. Matching argument or entry arrow types are not identity proofs. Without container provenance, nested closure results widen to Any | Null, retaining written parameters. | | Returned function alternatives (Arrows.narrow/2) | Alternatives stay a union. Call refinements attach only for a unique written and refined pair; ambiguous alternatives establish neither an intersection nor a correlation. |

source = ~s|if (function(x, existing) function(a,b) x)(true, function(a,b) true) instance of function<Any, Any> -> boolean then 1 else "wrong"|
{:ok, expression} = Feel.prepare(source, result_type: :number)
Feel.run(expression)
# {:ok, nil, diagnostics}, including :type_mismatch, with and without optimization

The function written there returns a function whose written result signature is Any; a specialized Boolean arrow that happens to match the unrelated argument's arrow is a coincidence, not an identity.

Limits. Arbitrary higher-order domains, recursive aliases and host functions with untruthful metadata are not covered.

2.8 What the evidence establishes

What they show: no failures in numeric Boolean-law trials below the cap, in string-law trials or in directed-rounding trials. Failures concentrate where broad sweeps need not look: cap boundaries, negative positions, projected function signatures, nested composites, unrecorded arities, and budget boundaries. Many ordinary expressions do not stand in for those dimensions, and passing below-cap grids cannot establish the algebra globally. The cap-boundary and budget-boundary cases have their own generators and regressions.

What they do not show: the monitor and the sweeps share membership machinery with the analyzer, which limits their independence, and Feel.Paranoid cannot independently certify a declared composite's meaning. Function equality ignores implementation closures and compares signature metadata, so returned functions must also be applied to representative inputs to test behavior. An empty violation list shows only that the particular run was not a counterexample. Mutation checks probe selected blind spots, and unchanged precision does not establish a theorem.

This is substantial empirical evidence for the exercised cases. It is not evidence that untested combinations are sound, and it is not a proof of unrestricted soundness. See Paranoid.

3 The science behind the design

3.1 Semantic subtyping gives types a meaning before an algorithm

Choose a universe of values V. A type T denotes a set ⟦T⟧ ⊆ V. Semantic subtyping is inclusion:

A <: B            exactly when  ⟦A⟧ ⊆ ⟦B⟧
⟦A ∪ B⟧          = ⟦A⟧ ∪ ⟦B⟧
⟦A ∩ B⟧          = ⟦A⟧ ∩ ⟦B⟧
⟦¬A⟧             = V \ ⟦A⟧
A <: B            exactly when  ⟦A ∩ ¬B⟧ is empty

The defining idea is that the algorithm should implement these meanings; its implementation does not define inclusion merely by returning true. Function types require a carefully chosen semantic model, rather than an unrestricted powerset construction over all mathematical functions. Frisch, Castagna, and Benzaken develop this approach and distinguish semantic subtyping from the separate task of establishing type safety for a language. Semantic subtyping, 2008.

Applied to this project, there are three obligations. First, specify the universe, including null and host values. Second, define each constructor independently of its normalization code. Third, show that the algorithms preserve that interpretation or expose where they approximate it.

The nullable declaration language needs a translation into this model. Its Any except T keeps null, so it is not simply complement over the entire universe. For an unmarked declaration, the intended reading is:

⟦Any except T⟧ = ((V \ {null}) \ (⟦T⟧ \ {null})) ∪ {null}

That convention is coherent; the nested-negation contract of section 2.4 concerns non-null values and does not depend on it.

Structure also carries correlations. list<number | string> permits mixed lists, while list<number> | list<string> permits only homogeneous lists under the corresponding element interpretation. Widening the latter to the former can be a useful analysis approximation, but cannot be called equality of sets. Likewise, describing list elements does not describe sequence length or order.

3.2 Abstract interpretation explains useful approximation

An analyzer rarely computes the exact set of outcomes of every program. It computes an abstract description that safely includes them. Abstract interpretation supplies the order-theoretic framework for relating concrete computations to such abstract computations, including conservative approximation and iterative analysis. Cousot and Cousot's foundational paper develops this framework. Abstract interpretation, 1977.

For this project, write γ(a) for the concrete values described by an analysis type a. A suitable result-containment obligation is:

If the environment satisfies the analysis assumptions,
and evaluating e returns value v,
then v ∈ γ(infer(e)).

This is conditional on declaration handling, supported host values, and runtime semantics. It does not assert termination. An optimizer needs a further obligation: preserving values, diagnostics, and strict failure behavior. Containing the returned value alone does not justify suppressing an observable diagnostic.

Each abstract transfer operation should satisfy a local inclusion obligation. For a concrete binary operation F and its abstract counterpart F#:

{ F(x, y) | x ∈ γ(a), y ∈ γ(b), F returns a value }
    ⊆ γ(F#(a, b))

This formula must include null results where runtime semantics produce null. Separate reasoning is needed for diagnostics and failures.

A convex hull can satisfy this upper-approximation requirement. It need not be the exact union or the least representable upper bound. Also, a resource cap is not automatically a formal widening operator: widening has additional convergence obligations in iterative analysis. Naming every loss of detail “widening” does not establish those properties.

The useful architectural separation is an exact language for the meanings of declared types, plus bounded abstract domains for program analysis. The analyzer may deliberately forget facts without changing what a user's declaration means.

3.3 Negation and variance determine the direction of approximation

This is the mathematical explanation behind the contracts of sections 2.2–2.5. Suppose a concrete set S has lower and upper approximations:

L ⊆ S ⊆ U

L supports “certainly belongs”; U supports “possibly belongs.” Exact complement reverses inclusion:

V \ U ⊆ V \ S ⊆ V \ L

Thus complementing an upper approximation produces a lower approximation, not another upper approximation. Union and intersection can combine lower bounds with lower bounds and upper bounds with upper bounds, provided their own approximation policy preserves the respective direction.

For function contracts, domain and result positions have opposite variance. Under a fixed arrow semantics, if A_lower ⊆ A ⊆ A_upper and B_lower ⊆ B ⊆ B_upper, then:

(A_upper → B_lower) <: (A → B) <: (A_lower → B_upper)

This explains why “replace every nested type by a broader type” is invalid. A broader parameter domain gives a narrower arrow. Negation introduces the same reversal, and nested arrows or negations can reverse direction repeatedly.

An implementation can track polarity while traversing types, maintain separate lower and upper descriptions, or avoid approximation inside exact type expressions. For rule certainty, dropping accepted pieces is safe; filling gaps is not. For possible results, filling gaps may be safe; dropping actual outcomes is not. These contracts should be visible in APIs rather than inferred from comments.

3.4 Occurrence typing connects conditions to local facts

Occurrence typing refines the type of an expression occurrence using evidence from control flow. Logical formulations attach propositions to predicates and combine them through conditionals and Boolean operators. This supports facts about paths and compound tests, not only direct variable checks. Tobin-Hochstadt and Felleisen's work provides a foundational treatment of this approach. Logical Types for Untyped Languages, 2010.

The project's narrowing machinery follows this general pattern. Its correctness depends on adapting the logic to FEEL's conditions, null propagation, path semantics, and binding identities. It must prove that the fact installed in each branch holds for every execution that reaches that branch. A sound Boolean-domain rule copied from another language can become unsound when false and null are collapsed incorrectly.

Precision can be improved with relations between variables, such as x < y, or between a list's length and an index. Such relational domains are optional extensions. Their absence usually means missed deductions; it is distinct from an incorrect deduction in the existing domain.

3.5 Function behavior and function introspection are different questions

A behavioral arrow constrains what happens when a function is applied to inputs in a domain. A signature predicate inspects a declared or stored description. These can coexist, but the type checker must not substitute one for the other without a proven implication.

For example, under a suitable behavioral interpretation:

(number → number) ∩ (string → string)
    <: (number ∪ string) → (number ∪ string)

The intersection records two correlated guarantees. The broader arrow loses the relationship between the input kind and output kind. The project's overload and call-refinement machinery already addresses some of this distinction, and section 2.1 states how the boundary is kept.

A full specification must say what arrows promise about null, argument conversion, diagnostics, failure, and divergence. One cannot decide arbitrary function behavior by inspecting its implementation or testing finitely many inputs. This limitation does not prevent decidable subtyping for a carefully restricted language of type expressions. Deciding relations between declared descriptions and inferring every true property of arbitrary programs are different problems.

The practical rule is to keep inspectable signature facts separate from behavioral call facts. instance of inference should use the former when that is what runtime inspection observes. Call analysis can use the latter when their assumptions are satisfied.

3.6 Numeric and temporal reasoning needs the runtime's mathematics

Correctness over real numbers does not imply correctness for decimal128 operations. The runtime uses bounded precision and exponent ranges. Rounding, overflow, underflow, and invalid operations affect both values and diagnostics. An interval operation must enclose results after the runtime's rounding and error policy, not merely after ideal arithmetic.

Outward rounding is the standard enclosing construction: round a lower bound downward and an upper bound upward. This still requires checking endpoint openness, monotonicity, discontinuities such as division around zero, and any intermediate operation that can fail. Grain information adds arithmetic structure beyond an interval, but each transfer of that structure needs its own invariant.

Temporal values similarly need a domain-specific interpretation. Local clocks, offsets, calendar dates, and elapsed durations cannot all be reduced to one interchangeable real coordinate. A box of independent bounds can safely include correlated temporal possibilities, yet complementing or intersecting an approximate box does not automatically recover the exact feasible combinations.

The directed-rounding and scalar-law tests are encouraging evidence for these domains. They do not establish the correctness of every composition with normalization, nullability, or temporal conversion.

3.7 How this differs from a complete set-theoretic type system

“Set-theoretic” describes a semantic approach, not a mandatory feature checklist. A system need not have polymorphism or recursive types to interpret its supported types as sets. The central question is whether it faithfully implements the semantics it claims for its supported language.

The remaining gaps can be closed without replacing the whole architecture. The scalar domains, narrowing machinery, runtime monitoring, and separation of compiler stages remain useful. The key changes concern semantic boundaries and the contracts of shared operations.

3.8 What the Elixir publications contribute

Two complementary works are especially relevant:

The design paper combines semantic subtyping with polymorphism, local inference, guards, and gradual typing. Sections 2–3 explain why intersections preserve input/output correlations, why function arity needs explicit treatment, and how records and dictionaries fit a common framework. Section 5 makes unchanged compilation an integration requirement. Its proposed annotation syntax illustrates the design; it should not be read as a description of syntax already available in a particular release. Design paper, sections 2–5.

The formal companion's section 2 develops strong functions: even outside their intended input domain, they cannot return outside the specified result type, though they may fail or diverge. Theorem 2.3 gives a gradual soundness result using a weak value-typing judgment and explicitly permits runtime-check failure. Section 3 separates possibly accepted inputs from surely accepted inputs. The formal development deliberately omits records/maps and parametric polymorphism. These are guarantees for its calculus, not a verification of an entire production compiler. Formal companion, sections 2–3 and 9.

Research design and released implementation. Elixir 1.20.4 documents best-effort inference across all language constructs; user-facing set-theoretic function signatures remain a roadmap item. It distinguishes term(), the top type, from dynamic(), which represents uncertainty and can be restricted as dynamic(T). Its documented scalar types also differ from this project's refinements: individual integers and binaries are represented by their broad types, whereas atoms have singleton types. Elixir 1.20.4 reference.

The following consequences are this document's assessment of how those ideas apply to FEEL.

Unknown information must not become an optimization proof. The internal [:any, :null] describes the full value universe. It is useful as an upper approximation, but this project does not thereby acquire a gradual type discipline. Likewise, :trust, :audit, and :ignore configure declaration handling; they do not establish a calculus of gradual compatibility. If gradual types are added, compatibility that permits a call to be checked at runtime must be kept separate from the subtype proof required to remove that check.

Safe erasure and check removal require different arguments. This project's optimizer deliberately changes the checks performed by execution. Its relevant obligation is therefore stronger than “the remaining runtime checks protect the type.” Each removal must establish that the removed check could neither reject nor produce an observable diagnostic for any reachable input. Sections 2.1 and 2.2 state how the implementation meets it for function signatures: metadata is separate from call facts and projection respects variance, so the required checks stay. A later implementation could record which proven facts justify each removal, making the dependency testable.

FEEL also needs its own account of failure. If an invalid operation returns null with a diagnostic, null is a returned value that must be included in the inferred result. A proof allowing exceptional termination does not justify a non-null numeric result for that operation. A FEEL analogue of strong functions would have to specify both the returned-value guarantee and what happens to diagnostics under ordinary and strict execution.

Guard analysis gives a concrete repair pattern for rules. The companion subtracts surely accepted inputs of earlier clauses when analyzing later clauses, and uses surely accepted coverage to establish exhaustiveness. Formal companion, section 3.

Applied to this project's rule analysis, let D be the input domain, R_i the actual inputs accepted by rule i, and L_i ⊆ R_i ⊆ U_i its certain and possible approximations. The following are sufficient proof conditions, derived from the inclusion rules in section 3.3:

Full coverage:           D ⊆ ⋃ L_i
Possible reach of i:     (D ∩ U_i) \ ⋃_{j<i} L_j
Dead under first match:  the possible-reach set is empty
Certain overlap i, j:    a witness belongs to D ∩ L_i ∩ L_j

These conditions need not decide every case. A nonempty possible-reach set does not prove a rule is live. Failure to establish certain coverage does not prove a gap. A certain set that fills gaps, as a hull of the 17 points of section 2.3 would, violates the premise L_i ⊆ R_i, and the final verdict logic cannot repair that; the lower-bound construction itself must keep the premise. An exactness flag can help track which pieces are usable as certain information, provided every constructor and resource limit preserves the flag's meaning.

Preserve this project's useful specialization. Numeric intervals, directed decimal rounding, grain facts, and temporal coordinates address FEEL-specific needs. Adopting a better Boolean type representation need not discard these domains. Each can remain an atomic theory with its own membership and inclusion procedures, while a common structural layer handles nesting and polarity. Conversely, adding polymorphism or a richer map language would not repair an incorrect complement or function projection.

This comparison strengthens the proposed direction: keep the project's value analysis, specify its semantic boundaries, and repair the operations that cross them. The literature supplies relevant methods; establishing their assumptions for FEEL and its optimizer remains implementation and proof work.

The scientific obligations established here inform the choices in chapter 6. Their implementation and validation criteria are collected in chapter 7.

4 Comparison with Hindley–Milner and other typing concepts

These concepts answer different questions and can be combined. A type language determines which properties can be expressed; an inference algorithm determines how descriptions are obtained; a soundness theorem relates those descriptions to execution. More expressive notation does not automatically provide better inference or a stronger guarantee.

The notation below is explanatory; it is not additional FEEL syntax.

4.1 Hindley–Milner and principal type schemes

Classical Hindley–Milner uses type variables, unification, and let-polymorphism. Variables independent of the surrounding environment can be generalized at a let binding and freshly instantiated at each use. For example:

let id = λx. x in (id 1, id true)

id : ∀α. α → α

The two calls instantiate α differently. Algorithm W computes a principal scheme: other valid typings are obtained by instantiation, within the specified calculus. This is a completeness result relative to its typing rules, not a claim to infer every true property of a program. Damas and Milner, 1982.

Here, α is not Any. The scheme connects an argument's type to its result type at every instantiation. Any → Any permits unrelated input and output types, including a function that always returns a fixed string.

The project's declared type language has no universal quantifier or type-variable constructor. A named type resolves to a definition; it is not a variable instantiated separately at calls. Instead, call analysis can reanalyze a known function body using the argument types. This can recover detailed results for particular calls without constructing a reusable polymorphic scheme. Passing the function through a less informative declaration may lose those facts.

Unification solves equality constraints on type expressions. This project's inclusion questions, exclusions, interval bounds, and branch refinements need additional machinery. Conversely, a narrow numeric result type does not supply the generic input/output relationship of a polymorphic scheme. Adding polymorphism could improve reusable function interfaces, but would require generalization, instantiation, and suitable constraint solving alongside the existing analysis. It would not replace the variance and approximation contracts of chapter 2.

4.2 Subtyping, structure, names, and overloading

Subtyping allows a more specific value description where a broader one is expected. Structural typing compares shapes; nominal typing also distinguishes explicitly declared identities. Neither choice determines whether a system is sound. TypeScript, for example, documents structural compatibility together with deliberate unsound compatibility rules. TypeScript compatibility reference.

FEEL's context relation is structural. If two model-defined names resolve to the same context shape, their names do not distinguish the resulting types. Thus naming two otherwise identical declarations CustomerId and InvoiceId does not by itself prevent mixing them. Such a distinction would require a nominal or branded extension, or distinguishable value structure. It is a separate feature from improving set operations.

Overloading is also distinct from parametric polymorphism. An intersection such as (Number → Number) ∩ (String → String) records several guarantees for one function. A type-class system instead expresses requirements on operations and supplies implementations through instances; Haskell's classes are an extension of its underlying polymorphic system. Haskell 2010, section 4.1.

The project's overload members describe arrow contracts and call refinements. They are not evidence of general type-class resolution or quantified polymorphism. Each could be added independently if a concrete use case warrants it.

4.3 Algebraic data types and set unions

An algebraic datatype introduces constructors with payloads. For example, the conceptual type Option(T) = None | Some(T) distinguishes values by constructor. A set union T ∪ Null simply includes the existing values from both sets. Constructor-based datatype declarations are described in the Haskell 2010 report, section 4.2.

The difference matters for nested optionality. Option(Option(Number)) distinguishes None, Some(None), and Some(Some(n)). In contrast, (Number ∪ Null) ∪ Null collapses to Number ∪ Null. The latter cannot identify which layer was absent.

FEEL's nullable declarations use the union interpretation. More elaborate alternatives can be encoded using contexts with distinguishing fields, but naming a union does not create a constructor or a new runtime tag. This is a modeling choice rather than a soundness defect.

4.4 Refinement types and dependent types

A refinement restricts a base type with a predicate, for example {v : Number | 0 ≤ v ≤ 100}. The project's numeric intervals express this particular kind of property directly. A relational predicate such as 1 ≤ i ≤ length(xs) additionally connects two program values; independent intervals for i and xs generally cannot preserve that relationship.

Liquid Types demonstrate how Hindley–Milner inference can be combined with predicate abstraction and decidable logical implication checks. Their inference searches a restricted space of refinements built from logical qualifiers. This is one example of combining polymorphism and value reasoning rather than choosing between them. Rondon, Kawaguchi, and Jhala, 2008.

For this project, richer relational refinements could improve indexing, bounds, and condition analysis. Their solver would need to model FEEL's decimals, nulls, and diagnostics accurately; an implication valid over mathematical integers or reals need not justify an optimization under FEEL arithmetic.

Dependent types allow types to be indexed by values. A length-indexed sequence can support a contract such as:

concat : Vec(m, A) × Vec(n, A) → Vec(m + n, A)

The output type records a relationship between input lengths. Idris uses this example to introduce value-dependent types. Idris tutorial.

Some refinement systems are restricted forms of dependent typing, so these categories overlap. This project's ability to represent a numeric singleton does not give it general dependent functions, indexed datatype families, or proof terms. Adding a useful length relation would be a targeted extension; a general dependent type language would be a substantially larger design change.

4.5 Gradual typing and dynamic typing

Section 3.8 describes Elixir's explicit distinction between a broad static type and dynamic uncertainty. In FEEL, Any is a broad value type. The declaration stances determine which assumptions are enforced or trusted. Those are different roles, even when both allow programs whose precise types are unavailable.

A gradual extension would need explicit rules for compatibility, propagation of uncertainty, and enforcement at dynamic boundaries. It must also state which facts remain usable by the optimizer. Merely accepting an unknown input, adding an Any fallback, or allowing execution after a warning does not establish such rules.

Dynamic typing likewise does not imply an absence of runtime guarantees: a runtime may check operations and reject invalid values. FEEL frequently communicates invalid operations through null and diagnostics instead. Its static analysis must describe that actual behavior, including paths that remain executable after a diagnostic.

4.6 Success typing and the direction of a guarantee

Success typing, developed for Erlang, overapproximates the inputs and outputs of successful function evaluations. For a success signature A → B, its defining implication is:

f(x) returns v  ⇒  x ∈ A and v ∈ B

Membership in A is necessary for successful evaluation; it is not sufficient to establish that the call avoids failure. Being outside A rules out a successful return, which supports detection of definite clashes. An absence of warnings is therefore not a general safety certificate. Lindahl and Sagonas, 2006, section 4.

The distinction matters when using an inferred domain to optimize this project. Knowing that all successful calls satisfy a constraint does not establish that every reachable call satisfies it: the excluded calls might be exactly those where a runtime check must report failure. Removing the check requires the latter argument.

For FEEL, “successful” also needs an explicit definition. Returning null with a diagnostic is still a return in the value semantics used in section 3.2. An analysis restricted to diagnostic-free runs could be useful for bug finding, but its result would not automatically describe all runs that the optimizer must preserve.

4.7 Effect types and observable behavior

Effect systems describe behavior beyond a returned value, such as exceptions, state changes, or divergence. Koka provides a concrete example where function types track such effects alongside result types. Koka language guide, section 3.2.

For FEEL, two expressions can have the same possible values but different diagnostics. One can return null normally; another can return null after reporting a mismatch; strict execution can distinguish them further. Union.t() alone does not express those differences.

An explicit summary of possible diagnostics and failure behavior could therefore complement the value type. Such a summary would support optimization, but a set of possible diagnostic codes would not by itself preserve their order or multiplicity. This is a proposal for strengthening the analysis contract, not a claim that the implementation already has a full effect system.

5 Comparison with TypeScript and other language designs

Chapter 4 compares theoretical concepts. This chapter compares how concrete languages and tools use them, with particular attention to runtime consequences. The comparisons use the official references linked below, consulted on 17 October 2026; TypeScript examples assume strictNullChecks and strictFunctionTypes are enabled. Statements about this project refer to the current implementation. Similar syntax does not imply the same semantics, and a feature comparison is not a soundness ranking.

5.1 Why these comparisons are useful

These systems were chosen for different design questions. Chapter 4 supplies the underlying concepts; the comparisons below focus on concrete language choices and their relevance to FEEL. OCaml and F# are especially useful for the proposed polymorphism work, Elm for boundary validation, and C# for separating nominal identity from nullable annotations. Dafny adds a different perspective: verifying an implementation rather than enriching its type syntax.

5.2 TypeScript: similar surface features, different runtime obligations

Structure and narrowing. TypeScript's object compatibility is primarily structural, so an object can satisfy an interface through its members without explicitly declaring that interface. Its compatibility rules also include exceptions and additional constraints; “structural” is not a complete description of the language. FEEL's context types and resolved aliases provide a useful comparison, although its rules for missing fields, null, and conversion differ. TypeScript compatibility.

TypeScript tracks control flow, recognizes type guards, and uses literal discriminants to narrow unions. A never check can expose an unhandled variant. Those are close practical analogues of FEEL's branch refinements and empty internal union, but TypeScript's exhaustiveness over a declared union does not establish coverage of a FEEL decision table with numeric predicates and three-valued tests. Narrowing and exhaustiveness.

For example, the two representations below express different relationships:

type Decision =
  | { kind: "approved"; limit: number }
  | { kind: "rejected"; reason: string };

type LooseDecision = {
  kind: "approved" | "rejected";
  limit?: number;
  reason?: string;
};

Decision connects a particular tag with a required payload; LooseDecision does not. FEEL's internal representation can keep analogous correlations in a union of separately described context alternatives, subject to the implementation limitations in chapter 2. Its declared type language does not provide TypeScript's literal-property syntax. Merging internal alternatives into one context with independently widened fields may lose the correlation. This is a useful regression scenario for R4 and future precision work.

Type manipulation is not general set algebra. TypeScript supports generics and transformations involving keys, indexed access, mapped types, and conditional types. These are useful for reusable APIs. FEEL currently has neither that general type-level language nor quantified type schemes; specialization of a known function body serves a different purpose. Creating types from types.

In particular, Exclude<T, U> removes members of T that are assignable to U. Applying that rule gives:

type Selected = Exclude<0 | 1 | 2, 0>; // 1 | 2
type NonZeroAttempt = Exclude<number, 0>; // number

The broad type number is not assignable to the singleton 0, so it survives the second exclusion unchanged. Zero therefore remains permitted. This calculation follows the documented utility-type rule; Exclude is not a general complement or subtraction operator over all represented values. Utility types.

FEEL's internal numeric sets can represent an interval with a point removed. That is a different capability from filtering named union alternatives. It gives this project useful domain-specific precision, while also creating the algebraic obligations of its cap and negation contracts. Neither system dominates the other simply by having more type operators.

any, unknown, and null. TypeScript's unknown can describe any value while requiring refinement before operations that need a particular type. any permits operations without that checking. FEEL's full internal universe, [:any, :null], has the broad-value role; its name should not be read as permission to assume a particular operand type. This is an analogy of roles, not an identity between the languages' universes or checking rules. TypeScript's unknown.

With strictNullChecks, TypeScript distinguishes null and undefined from ordinary non-null types. FEEL's ordinary declared number includes null, and number! excludes it. A nullable context field still has to exist in FEEL; this is different from TypeScript's optional-property syntax. Nullability and presence need separate treatment in any cross-language schema translation. Strict null checks, optional properties.

Soundness and execution. TypeScript explicitly documents accepted unsound behavior. strictFunctionTypes catches unsafe parameter assignments in function syntax, but method syntax is still an exception. Enabling strict checking therefore does not turn TypeScript compatibility into a universal semantic-inclusion proof. Compatibility and soundness, strict function checks.

TypeScript type annotations are erased and do not themselves perform runtime validation. An interface describing external data does not make that data conform at runtime. Erased types.

FEEL has a different obligation: declarations can drive runtime checks and conversions, function signatures can be inspected, and inferred types can cause checks to be removed. The contracts of 2.1–2.2 exist because inferred signatures change observable execution. TypeScript's compatibility tradeoffs do not justify importing similarly permissive rules into FEEL's optimization proofs. TypeScript is a useful reference for expressive interfaces and readable narrowing; R1–R6 must establish the stronger contracts needed by this compiler.

5.3 Python typing: unknown information and runtime validation

Python's typing specification distinguishes object, a static type containing all Python objects, from Any, an unknown static type. It also distinguishes static subtyping from gradual assignability. Classes provide nominal relationships, while protocols and typed dictionaries describe structural requirements. These distinctions offer a clearer vocabulary for FEEL's broad types and host assumptions than treating every permissive boundary as Any. Python type-system concepts.

Python does not automatically enforce function and variable annotations at runtime. NewType can introduce a static distinction without wrapping the runtime value; its constructor returns the supplied object. Consequently, a static business-identifier distinction and a runtime data validator are separate facilities. Python typing reference.

The lesson for FEEL is to distinguish three things explicitly: the set a declaration denotes, uncertainty about an input, and the runtime action taken at a boundary. :trust relies on a host promise; it does not validate that promise. :audit observes violations while keeping the values. Neither should silently become the same operation as enforcement. R6 should make these dependencies visible, and any future gradual extension should define its own compatibility relation rather than weakening the optimizer's subtype relation.

5.4 Kotlin: nullability and the lifetime of a fact

Kotlin distinguishes non-null types such as String from nullable types such as String?. Its documentation also identifies ways null-related failures remain possible, including !!, initialization problems, and Java interoperability. The comparison is useful because it makes the boundary assumptions part of the explanation rather than treating a non-null spelling as an unconditional guarantee. Kotlin null safety.

Kotlin smart casts use control-flow information, but only where the checked value is sufficiently stable between the check and its use. Mutable properties and custom getters, for example, restrict the available reasoning. Its compiler also uses internal intersection information that is mostly not directly expressible in source syntax. Type checks and smart casts.

FEEL already distinguishes public declarations from richer internal descriptions, and binding identities prevent refinements from crossing shadowed names. Kotlin suggests a further review question: does a fact still refer to the same value at every use, especially when host functions or external context behavior are involved? This is an audit obligation, not a newly demonstrated FEEL defect. Public function projection checks the variance contract of 2.2; the wider audit must preserve it. FEEL's nullable declarations and null-with-diagnostic behavior also require their own rules rather than a direct translation of Kotlin's null checks.

5.5 Rust: explicit alternatives and explicit trust boundaries

Rust enums associate each alternative with its own payload. Option<T> distinguishes absence from a present value, and exhaustive match checks require the alternatives to be covered. Result<T, E> distinguishes a successful result from an error value. These are concrete examples of preserving distinctions in the value representation. Enums and Option, exhaustive matches, recoverable errors.

For FEEL, missing input, an explicit null, and an invalid operation returning null with diagnostics need not mean the same thing. A tagged context representation could keep distinctions needed by a business model; an effect summary could keep the execution distinctions needed by the optimizer. These address different layers. Replacing FEEL's existing null behavior with a Rust-like result type would change the language contract, so the immediate roadmap should preserve that behavior while describing it accurately.

Rust's unsafe boundary identifies contracts that the compiler cannot check and that programmers must uphold. This helps explain why safety depends on more than a surface type annotation. It does not mean that every type-correct Rust program terminates, avoids panics, or satisfies its business requirements. Safe and unsafe contracts.

The applicable lesson is to identify trusted obligations, such as host-provided values and callable summaries, and limit their consequences. Rust's ownership and borrowing machinery answers memory and aliasing questions; importing it wholesale would not repair FEEL's complement, projection, or rule-certainty bugs. R1 and R6 need explicit contracts, while tagged modeling remains a separate option in section 7.6.

5.6 CUE: constraints as a first-class data model

CUE is especially relevant to a decision-modeling language because its specification places types, constraints, and concrete values in a common lattice. Unification with & takes a greatest lower bound; disjunction with | takes a least upper bound. Bounds describe values satisfying comparisons. A small example is:

amount: number & >=0 & <=100

An incompatible additional constraint produces bottom rather than expanding the accepted range to accommodate it. CUE also distinguishes null from bottom; bottom represents evaluation errors in its semantics. CUE language specification.

This makes CUE a useful comparison for declaration meaning and the algebra promised by an API. FEEL's exact declaration path should not silently fill holes to meet an analysis budget. A separate approximate analysis may do so in a documented direction; the numeric modes implement one part of that R1–R4 separation. Likewise, an operation called a least upper bound should meet that contract. join/2 promises a conservative common supertype (2.6).

CUE's unification is not Algorithm W's unification of type variables: here it combines information by taking a lattice meet. Nor does its treatment of bottom transfer directly to FEEL. FEEL may return an ordinary null value together with an observable diagnostic, and its decimal and temporal computations require their own transfer semantics. CUE supplies a useful algebraic comparison, not a substitute runtime specification or a proof of this implementation.

5.7 Elixir and Erlang: separate the research model from the warning tool

The Elixir research discussed in section 3.8 is the closest comparison for semantic subtyping and guard analysis. Its distinction between possible and certain inputs directly informs R5. The released Elixir reference also distinguishes the broad type term() from uncertainty expressed by dynamic(). Those ideas should remain separate from FEEL's declaration stances and its existing internal top type. Versioned Elixir reference.

Erlang's Dialyzer is a different comparison. It detects discrepancies using success typing; its documented purpose includes finding definite type errors and unreachable code. Dialyzer reference.

As section 4.6 explains, a necessary condition for successful return is not a sufficient condition for a reachable call to avoid failure. FEEL can use conservative discrepancy analysis to produce useful diagnostics, but a check-removal decision must account for executions where that check rejects or emits a diagnostic. A clean analysis report, by itself, does not supply that proof. Neither Elixir's design papers nor Dialyzer's purpose should be presented as a guarantee inherited simply because this project runs on the BEAM.

5.8 Elm: explicit failure and validated input boundaries

Elm uses Maybe a to distinguish absence from a present value and Result error value to attach information to failure. Ordinary values are not implicitly nullable. Its guide also illustrates how a custom type can preserve correlations that a record of independently optional fields loses. These are useful comparisons for decision models where “missing,” “invalid,” and “rejected” have different meanings. Elm's Maybe, Result.

Elm's JSON decoders are particularly relevant: external data is checked while constructing the typed value that the program will use. An annotation alone does not establish that the incoming payload has the expected shape. A decoder establishes only the properties it actually checks; checking that a field is an integer does not establish a business-specific range. Elm JSON decoders.

For FEEL, this suggests treating a successful declaration boundary as evidence with a precise scope. The distinction between :enforce, which checks and may convert, and :trust, which relies on the host, should remain visible to analysis. A decoded or validated value may justify stronger assumptions than an unchecked one. R6 should track that difference rather than infer trust from a type name.

Elm's approach does not require replacing FEEL's observable null-and-diagnostic behavior. It suggests better explicit domain models and stronger boundary contracts. Nor does eliminating implicit null establish termination or prove every business rule correct; the relevant comparison is the particular class of failures the representation excludes.

5.9 OCaml: polymorphic inference with restrictions that matter

OCaml makes the Hindley–Milner comparison concrete: reusable polymorphic functions coexist with mutable state, so generalizing every inferred type variable would be unsound. Its value restriction limits generalization, and its relaxed form recovers some polymorphism using covariance. A weak type variable stands for one type to be fixed, rather than a fresh choice at every use. OCaml 5.5: polymorphism and its limitations.

For example, in an interactive session:

let cell = ref None;;
(* cell has a weak option-element type, not a universally quantified one. *)

If one shared cell could independently instantiate its element type at each use, writing a number could be followed by reading it as a string. The restriction prevents that interpretation. FEEL's polymorphism proposal therefore needs a generalization policy that reflects its actual semantics, including captured host callables and any persistent state they expose. It should not copy OCaml's restriction without determining which effects FEEL admits, but it cannot assume that adding type variables alone completes the design.

OCaml also distinguishes ordinary declared variants from polymorphic variants, whose admissible tags can be inferred and constrained without assigning each tag to a single declared datatype. This is a useful comparison for extensible alternatives and row-like information. It is not general complement over arbitrary values, and tagged alternatives are not interchangeable with FEEL's untagged set unions. Polymorphic variants.

Finally, richer function types do not automatically account for every effect: OCaml 5.5's effect handlers do not statically guarantee that every performed effect is handled; an unhandled effect raises an exception. This makes it a useful counterpoint to Koka in section 4.7. R6 still needs a FEEL-specific account of diagnostics and strict failure, even if the language gains ML-style polymorphism. OCaml effect handlers.

5.10 F#: generic contracts and dimensions of quantities

F# combines automatic generalization with restrictions on which values can be generalized, and its discriminated unions describe alternatives with their associated data. This is a practical reference for reusable inferred contracts and domain models. Sharing the .NET runtime with C# does not make their inference and modeling choices identical. F# generalization, discriminated unions.

Units of measure add a particularly relevant capability for FEEL's business calculations. They can distinguish quantities that have identical numeric ranges but different meanings:

[<Measure>] type USD
[<Measure>] type EUR

let dollars = 10.0M<USD>
let euros = 10.0M<EUR>
// dollars + euros is rejected because the units differ.

F# checks unit combinations statically; the measure annotations are erased at runtime. They do not themselves supply a currency conversion rate or a rounding policy. Units of measure.

This illustrates a gap independent of interval precision. Knowing that both amounts lie between zero and one hundred cannot distinguish dollars from euros. FEEL already distinguishes temporal kinds, but its ordinary named aliases do not establish a general dimensional type system. Units or nominal quantity types could be a useful targeted extension if real models need them. Such an extension would need rules for arithmetic and host boundaries, and would complement the existing interval domain rather than replace it. Erased units would also need a deliberate relationship to FEEL's runtime type inspection; their static distinction cannot simply be assumed observable at runtime.

5.11 C#: nominal identity, nullable warnings, and runtime types

C# supplies a useful contrast to FEEL's structural aliases. Separate record declarations introduce separate types, even when their data fields have the same shape:

record CustomerId(int Value);
record InvoiceId(int Value);

An InvoiceId does not become a CustomerId just because both contain an integer named Value. Record value equality also should not be confused with structural type compatibility. A corresponding FEEL distinction would need more than two names resolving to the same context declaration. C# records.

With nullable-reference analysis enabled, string and string? express different intentions to the compiler, but both have the runtime type System.String. The analysis produces warnings and does not add runtime enforcement of those annotations. This differs from nullable value types: int? is System.Nullable<int>, a distinct constructed value type. Nullable reference types, nullable value types.

That distinction is relevant to the signature and refinement split of 2.1. A static fact, a runtime type representation, and a runtime check may deliberately encode different information. The analyzer must model the operation actually performed; a non-null static claim does not prove that an inspectable runtime descriptor contains a non-null marker. R2 should specify these interfaces explicitly, and R6 should distinguish a warning about violated intent from enforcement of an optimizer assumption.

C# is therefore useful alongside F#, not as a substitute for it. F# contributes generalization and dimensional modeling; C# makes nominal identity and the limits of nullable annotations especially clear. Neither comparison makes the contracts of chapter 2 optional.

5.12 Dafny: a comparison for verification rather than more syntax

Among the further comparisons, Dafny adds a distinctly different perspective. It combines programming with explicit specifications: requires clauses describe preconditions and ensures clauses describe postconditions, with verification obligations connecting callers and implementations. This goes beyond giving an expression a broad result type. Dafny specifications.

For this project, a useful application would be a small verified model of interval inclusion, directed approximation, or polarity-sensitive projection. The objective would be a specific inclusion or preservation theorem, not “the program passed a type checker.” R8 would still need to connect that model to the Elixir implementation, including decimal semantics, null, and diagnostics. A proof about ideal integers or reals cannot silently certify the deployed numeric operations.

This is a stronger next comparison for mathematical correctness than adding more similar mainstream language surveys. It is an optional verification direction after the contracts in R1 are explicit, not a proposal to rewrite the project in Dafny.

6 Recommended target design

Recommendation: a FEEL-compatible structural type system with a small, exact set-theoretic core, bounded abstract interpretation, and explicit contracts for assumptions and observable behavior. Keep the existing numeric and temporal specialization. Make the supported type language reliable before expanding it.

This is a design recommendation derived from the preceding evidence and comparisons. It is not a claim that another language supplies a complete solution or that the current implementation already satisfies these contracts. The main tradeoff is deliberate: accept less inference precision and keep more runtime checks when necessary to make every definitive conclusion trustworthy.

6.1 Decisions to adopt

These choices preserve the project's character: a decision-language implementation with strong value analysis. They do not require adopting the full surface language or inference algorithm of any comparison system.

6.2 The guarantee to aim for

Specify a supported value universe and operational semantics first. Include null, decimal and temporal values, contexts, lists, functions, and the admitted host-value forms. Unsupported host values must be rejected at a defined boundary or represented as opaque values with conservative behavior. Define complement relative to this universe and translate nullable declarations into it explicitly.

The target has five distinct obligations:

For example, let U be the inferred upper bound for expression e under assumptions A. If an admitted execution satisfying A returns v, then v ∈ ⟦U⟧. A separate preservation argument must relate optimized and unoptimized execution, including observable effects. The first property does not imply the second.

This is a conditional soundness target with a precisely stated scope. It promises neither termination nor freedom from ordinary FEEL runtime errors. It also does not promise the most precise inferred type, a principal type scheme for every program, or a decision for every subtype query. The verified default path should establish input assumptions through enforcement; the trusted path must expose which assumptions the host supplies.

6.3 Separate exact meaning, bounded analysis, and proof consumption

Use three internal interfaces with different responsibilities:

The existing Verdict interface already distinguishes :yes, {:no, witness}, and :unknown. Strengthen the justification behind those outcomes and extend the separation to producers and consumers of approximations. A false result from an incomplete Boolean helper must not be promoted to a mathematical counterexample.

For representation, keep exact scalar interval sets without an implicit hull cap and preserve structural union, intersection, and complement as expressions when flattening would lose meaning. Shared nodes and memoized queries are a sensible eventual representation. Start with the smallest change that restores compositional semantics; choose a decision diagram only if measurements justify it. Boolean sharing does not decide relationships between interval, context, or function atoms by itself.

Keep exact normalization and approximation separate even if they share implementation helpers. Negation reverses approximation direction, and function parameters reverse it again. Prefer distinct constructors or tagged results for exact, lower, and upper descriptions, with contracts checked at their boundaries. A single generic constructor must not silently serve all three roles.

The 17-even-point example makes the policy concrete. Its declaration must keep exactly those points. Analysis may use the hull as an upper bound, but a certain set must keep a subset of the points, possibly the empty set if its budget is exhausted. The filled gaps cannot become accepted inputs merely because a representation limit was reached.

Separate display from semantics too. An explanatory type display may abbreviate a large expression. An exported type advertised as a sound upper bound needs a proven inclusion, including through negative and function-parameter positions. If the public syntax cannot express a sufficiently precise safe projection, export a broader valid type or an explicitly unavailable result; do not print an attractive but false contract.

6.4 Establish assumptions at boundaries

Keep enforcement as the default. A checked boundary establishes properties of the value after conversion and enforcement, not automatically of the original host value. The analysis must include any null result, diagnostic, or terminating failure that the boundary can produce. Only continuations that survive the boundary may use the facts it establishes.

For example, an input age constrained to [0..150] may arrive as 200. Enforcement can reject or replace that value according to the established FEEL contract. If execution continues with null, subsequent analysis must include null. If a non-null declaration terminates that execution, there is no continuing value on that path. Merely reporting the violation while keeping 200 does not establish the range for a non-strict continuation.

Make host trust an explicit, separately identified source of facts. :trust may use a declared range without rechecking it, but all dependent guarantees remain conditional on the host honoring that range. The same rule applies to supplied function summaries and claims about purity. An unverified host annotation must not acquire the status of an enforced fact just because it has the same type syntax.

Recommended policy for permissive execution: when a mode keeps invalid inputs and execution continues, analyze those values conservatively unless the caller separately opts into a host contract. Reporting is an observable effect, not evidence of conformance. A guard that actually checks a property can establish it locally; strict termination can exclude a violating continuation where the operational semantics justify that conclusion.

This differs from the current contract described in section 1.6: all stances assume declared kinds, and :audit also uses allowed-value refinements. Introduce the conservative behavior as an explicit profile or versioned API change, keep a documented compatibility path, and test both. Do not silently reinterpret existing stance names. The long-term goal is that runtime handling and the origin of analysis assumptions are separately represented internally, while the public API offers a small set of coherent policies.

Full and core analysis should differ in precision and cost. They should satisfy the same applicable soundness obligations; neither tier should grant permission to use unsupported assumptions.

6.5 Give functions two connected contracts

Keep runtime function membership as a predicate over inspectable signature metadata for the initial target. Specify the metadata construction once and use it in both backends and signature-test inference. Define arity, nullability, parameter variance, result variance, and the relationship to argument conversion in that contract. Metadata describes what inspection observes; it does not by itself verify a host callable's implementation.

Store behavioral call summaries separately. A summary states that, under given argument and environment preconditions, returning calls produce values in an upper bound and may have specified effects. It may preserve a relationship such as “numeric input produces numeric output; string input produces string output.” Such correlated summaries can be more useful than a single broad result union without becoming runtime signature facts.

For (function(x: number) 1), a valid call summary can establish the result 1 on the relevant call paths. If the runtime result descriptor is nullable number, the signature-based test against function<number> -> number! must still agree with that descriptor. Improving call precision must not change the answer to an introspection operation by assumption.

The same separation applies to functions in contexts and lists, exported approximations, built-ins, and callbacks. Unknown host behavior needs conservative result and effect information unless an explicit contract supplies stronger facts. Arbitrary behavioral membership cannot be decided by inspecting a closure or sampling calls.

A more complete algebra of behavioral arrows can be added later, with a chosen model of failure, null, conversion, and effects. It should not be a prerequisite for specifying signature inspection, and its conclusions must cross into metadata reasoning only through specified, valid implications.

6.6 Make rule and optimization conclusions accountable

Carry possible and certain guard inputs through the whole rule pipeline, including aggregation and subtraction of earlier rules. Track the outcomes relevant to FEEL's true, false, and null behavior; false is not automatically the complement of true. Apply the proof conditions in section 3.8 and validate reported witnesses against the original predicates. The explanation for an unknown verdict should distinguish a resource limit, an unsupported operation, and insufficient facts where practical.

The implementation already provides three-outcome facts, origins for stored conditions, and failure-aware inverse reasoning for selected operations (D-194). Extend and validate them: a stored boolean's facts must remain conditional on the context in which it was computed and the identity of the bindings it describes. Negating a predicate must select its false outcome rather than complement an approximate true set. These semantics use the existing closure representation; changing facts into data does not establish their correctness automatically. General certain-input analysis still needs the lower-bound contract in section 3.8, including through resource caps.

For optimization, begin with small internal effect summaries: whether a computation may emit diagnostics, fail, call an effectful host function, or depend on runtime state. These can conservatively block a transformation. They are not a complete trace semantics: a set of possible diagnostic codes cannot justify changing diagnostic order or multiplicity, and a result type cannot justify eliminating a host call.

Each check removal should identify the fact that makes the check redundant, where that fact came from, and why it still holds at that program point. A small derivation record or a transformation-specific contract is enough initially; a general proof-certificate framework is not required. Preserve the check's conversion behavior as well as its rejection and diagnostic behavior. Keep facts tied to binding identity and invalidate facts whose supporting assumptions can change.

This makes the operational policy simple: proven preconditions permit a specific transformation; uncertainty keeps the original behavior. A larger analysis budget may improve precision, but running out of budget must never create permission to optimize.

6.7 Scope the first release and subsequent extensions

The first stable target is the existing supported type language with the semantics and guarantees of section 6.2. Preserve nullable surface syntax, structural aliases, and FEEL's runtime behavior. Keep explicit null, the empty type, and the full universe distinct internally. Existing unions and negation must compose correctly; an additional public intersection syntax can wait if internal intersection already serves the required analysis.

After that release, use the following priorities:

For polymorphism, start with explicit schemes and inference for a restricted class of safe definitions. Do not generalize variables tied to mutable or unknown host state without a valid rule. Specify how schemes relate to runtime signature inspection before exposing them publicly; a quantified static contract is not automatically a decidable runtime predicate. Once subtyping, refinements, and effects are involved, copying Algorithm W or promising universal principal types would overstate the design. Annotations and honest inference limits are acceptable.

The main costs are more explicit internal contracts, some larger exact representations, and occasionally less aggressive optimization. Benchmark those costs against preparation time, memory, runtime, and the rate of unknown answers. The existing decimal and temporal domains should remain specialized components with local invariants. Small formal models of those invariants can strengthen the evidence, provided their connection to the implementation is stated.

Chapter 7 turns this target into staged work. R1–R8 establish the initial guarantees; the later feature backlog is selective. Success means that supported declarations mean what they say and definitive answers are dependable, while precision can improve without changing those promises.

7 Open obligations and extensions

This chapter lists what the guarantees of section 6.2 still need for the supported fragment, and which extensions could follow. The work is grouped as R1–R8; the open parts are the release gate. Restoring valid guarantees has higher impact than enlarging the language.

7.1 Scope and dependency on the target design

The five guarantees in section 6.2 apply to the current supported fragment. R1 makes the contracts explicit; R2–R7 establish them across the affected implementation paths; R8 assembles the validation evidence. New type-language features are outside this gate.

R6 follows the policy in section 6.4: conservative analysis for permissive continuations, with explicitly conditional host-trust behavior kept through a documented migration path. Its API and compatibility work must be estimated separately if it exceeds the assumption audit below. The effort ranges in this chapter do not include every later design extension.

7.2 R1: make approximation direction part of the interface

Write a short semantic specification alongside the existing guide. It defines the value universe, the nullable declaration translation, open and closed contexts, conversion boundaries, function metadata, and the behavior of tests that return null. It distinguishes signature-based membership from behavioral call guarantees, and it establishes these meanings independently of Union.new/1 and Composite.to_union/1.

The numeric approximation modes and the signature and projection distinction are implemented and documented. The remaining inventory extends those contracts to every scalar, structural and proof-producing caller, so that the symmetric approximation of arrows is not reintroduced.

The specification includes the D-209 unary-test contract: a null-producing numeric or duration expression involving ? yields an unknown answer, as dynamic matching specifies. Keep the comparisons between -? and if b then -? else [] with b true, and the analogous ? + 1 forms, on both backends and analysis tiers. Cover further lowering shortcuts against the same runtime contract; a tighter possible-result type alone does not establish equivalence.

Inventory the callers of Union, NumberSet, StringSet and Arrows. Classify each operation as exact, upper-approximating, lower-approximating or a proof query. Choose explicit entry points or tagged representations so that a lower-bound consumer cannot call the ordinary upper-bounding constructor by accident. An exact? flag helps only if every operation propagates it; it cannot recover information already discarded.

The contracts, where S is the intended concrete set and L ⊆ S ⊆ U:

exact_normalize(S) denotes S
lower(S) ⊆ S ⊆ upper(S)
complement bounds:        V \ U ⊆ V \ S ⊆ V \ L
difference bounds:        L_A \ U_B ⊆ A \ B ⊆ U_A \ L_B
arrow bounds:            (U_A → L_B) <: (A → B) <: (L_A → U_B)

The arrow rule applies within the chosen arrow interpretation; it does not equate metadata with behavior. Operations on bounds must preserve the indicated direction. A bounded complement cannot be reused as though it were exact in these formulas.

Verdict distinguishes :yes, a counterexample and :unknown. Its proof-producing paths need an audit as well as its witness validation: a three-way return type cannot make an unsound subtype or emptiness procedure safe. Boolean convenience APIs stay only with a clear contract that false may mean "not proved", and are never used as proof of non-inclusion.

Exit criteria: the function examples of section 2.1 do not bypass a result check on either backend; the 17-point example of section 2.3 reports no false coverage, overlap or deadness; unsupported declared composites are interpreted correctly or rejected explicitly. Each proof consumer has an identified contract and each cap has a documented fallback. Budget exhaustion keeps a check or produces unknown; it never becomes a proof. Runtime declaration checks have an exact supported membership path or an explicit rejection, since treating unknown membership silently as true or false changes the declaration's meaning.

7.3 R2–R4: the shared foundations

R2 — functions. Inspectable arrows are separate from body and call refinements, and runtime signatures decide membership (section 2.1). Open: keep this distinction through higher-order and escaped values, and audit every remaining projection and bounded fallback through contexts, lists, overloads and higher-order parameters. Function parameters reverse polarity, results preserve it, and exclusion reverses it again. The interpreter and the BEAM backend both consume meta.returns (D-219) and use Feel.IR.result_spec/1 to keep an enforced recursive result graph through the surrounding checks; a shared construction would remove the duplication.

R2 acceptance: the examples of sections 2.1 and 2.2 give matching inferred signature predicates and runtime answers; a runtime function conforms to every public type advertised as its sound approximation. Check null and non-null parameters, nested negative positions, built-ins, and both backends. Precise call results stay available where their behavioral justification is valid.

R3 — scalars. Complement and inclusion are exact; union and intersection select :outer, :inner or :exact (section 2.5). Open: audit all callers' approximation directions, the 64-piece string policy and the numeric sets used in temporal domains. Default numeric union and intersection are upper approximations, so the API is not universally exact. When an exact proof query exceeds its budget, keep an exact expression or return unknown. Raising the cap postpones a counterexample and is not a repair. A lower approximation may keep a subset of pieces or become empty, and an upper approximation may fill gaps; the policy has to stay correct when the result is later complemented or subtracted.

R3 acceptance: the 16-point set of section 2.5 is included in itself and exact double complement restores it. Exact Boolean laws hold around 15/16/17 numeric intervals and 63/64/65 string pieces. Approximate operations pass directional containment checks, including compositions with difference and complement. Decimal endpoint openness, domain extrema and temporal image restrictions remain covered.

R4 — structure. Normalization keeps nested exclusions when it builds a declared type, and the nested context and double-negation examples have their specified membership (section 2.4). Guarded recursive data use finite declaration graphs with a separate finite-tree membership oracle (FEEL D-189, DMN DD-22). Open: extend that oracle to generated mutual graphs and broader constructor families; it is not a general recursive inclusion oracle. Generalizing the graph representation to the rest of the set algebra is a separate design question. Audit membership, inclusion and projection so that no path reintroduces a lossy normalization. The FEEL null convention stays explicit when complement laws are applied: ordinary declared negation is not complement over the entire universe. A richer inclusion procedure that cannot decide a supported exact expression may return unknown without changing runtime membership.

R4 acceptance: the examples of section 2.4 have their specified membership. Generated declarations agree with the independent oracle for nulls, absent and present fields, empty and mixed lists, nested negation and resolved names. Function cases use the signature contract of R2. Shrunk failures become permanent regressions.

7.4 R5–R7: consumers and public contracts

R5 — decision rules. DMN adapts wildcards with the prepared table's effective tests and passes scope-dependent cells as :unknown (DD-43). Open: carry lower and upper bounds through TestSets, Refinement, context construction and the union of complete rules in Rules. Fixing only certain/2 is not enough if a later Union.new/1 enlarges its result. Bounds for the true and the false outcome stay separate: FEEL negation does not turn a null outcome into true. The coverage and reachability proof conditions of section 3.8 apply.

Validate uncovered inputs against every original rule, overlap inputs against both claimed rules, and live inputs against the selected rule and all earlier rules under first-match semantics. Validation also checks the original input domain. Unsupported or indeterminate validation yields unknown and never a witness. It does not replace the proof obligations for universal claims such as coverage and deadness.

R5 acceptance: containment may return unknown for the 17-even-point table, but the exact scalar path reports a validated gap, a live second rule with input 1, and disjointness of the two rules. Every definitive verdict on exhaustively evaluated small-domain tables agrees with direct unary-test execution, including null and negated tests. Remaining unknown answers are tracked separately as precision gaps.

R6 — assumptions and effects. Preparation warnings may describe inferred types while the built-in runtime boundary reports actual values; signatures and runtime outcomes are the same across supported tiers (section 2.1). Open: there are no general effect summaries, and the declaration assumptions remain.

Record which facts are guaranteed by enforcement and which depend on the host. Implement the policy of section 6.4: a conservative profile for retained invalid inputs, plus an explicit compatibility path for existing conditional host contracts. The documentation makes declared kinds an assumption even in modes that keep invalid values, and a migration has to preserve that distinction visibly. This is an API decision. For every supported stance and profile, document the guarantee and the behavior when its premises fail.

At each check-removal site, require a value-containment proof under established assumptions and a justification that the check cannot convert a value, emit a diagnostic or terminate a strict run. Start with local summaries that are enough to keep uncertain checks; a full effect language is not needed. Any summary added must describe possible behavior conservatively. A set of diagnostic codes alone does not preserve order, multiplicity, locations or the first strict failure.

R6 acceptance: supported stance and tier combinations have tests with valid bindings, invalid kinds, invalid allowed values and null. Guarantees claimed only under host assumptions are labeled so; guarantees claimed for invalid bindings are tested too. Each optimization has a documented precondition and preserves the observable runtime contract, including conversion.

R7 — equivalence and join. Equal terms are a fast path, and mutual conformance is accepted (section 2.6). Where conformance is bounded, the Boolean contract stays conservative: failure to prove either direction does not establish semantic inequality. Both join/2 entry points document a conservative common supertype. Open: audit callers for reliance on leastness. Offer an exact union or least-upper-bound operation only in a fragment where that guarantee is established. Broader semantic-equivalence validation is part of R8.

R7 acceptance: reordered unions compare equivalent; every returned common supertype contains both operands; any API that claims leastness has an argument and tests for its stated fragment. The arrow example of section 2.6 stays as a documented limit against overstating the contract.

7.5 R8: evidence for optimization and releases

Three validation layers cover different failure modes:

Paranoid compares all diagnostic and error fields recursively. Closure-containing diagnostics compare by FEEL value rules and not by raw closure identity. Its function comparison ignores the implementation closure, so generated returned functions are applied to representative inputs; metadata equality alone does not establish equal behavior. Clocks and entropy stay fixed during differential execution, as the monitor already does. Host effects need controlled test doubles and not repeated uncontrolled execution.

The tier sweep compares core and unoptimized interpreter execution with full and optimized execution, lenient and strict, with full diagnostic equality and paranoid node checks. The focused signature regressions also cross both backends and optimizer settings. The generator extends deliberately, because the corpus does not exhaust declaration stances, result declarations, recursion, extensions or function behavior.

Run the focused suites after each change. At integration, run the repository-wide suite including the sweeps with warnings as errors, inspect the excluded gap cases, and record the exact source revision and exclusions. Boundary generators go into the existing sweep infrastructure, with saved seeds and shrunk failures. Exercise numeric and temporal transfers near zero division, rounding boundaries, overflow and invalid conversions; the exact algebra does not by itself establish the correctness of the transfer functions.

Record proof obligations as well as tests: constructor meaning, exact normalization equivalence, directed approximation, transfer containment, branch facts and each optimization precondition. A proof for a small formal core strengthens the evidence if its relationship to the implementation is stated. Neither a model proof nor a large green suite verifies the whole compiler.

Benchmark preparation time, runtime and peak memory on one corpus before and after a change. Track the frequency of unknown verdicts and retained checks separately from correctness. A precision or performance regression is a reason to improve the algorithm and never a reason to accept an invalid proof.

Release gate: known failure classes are fixed or rejected explicitly; unsupported proof cases stay unknown; no unexplained differences remain in the validation matrix; scope and exclusions are documented. The declarations of section 2.4 are supported, and a newly rejected supported form is unfinished work. Any new proof-dependent optimization needs its own premises and regression evidence. The result is evidence for the stated guarantees and not a proof of unrestricted soundness.

7.6 Closing the remaining expressiveness and precision gaps

The implementation has rule-entry facts for outputs, kind-based arithmetic with unknown operands, unknown negation, repeated-value arithmetic, date-neighbor joins and selected duration failure regions (D-194, D-195, D-196, D-203, D-204, D-207). Month-duration self-division preserves zero and conversion failures. Rejected AST cases, whole-model chain audits and generated mutations are part of the checks (D-199, D-206). These are existing capabilities to preserve. The remaining work extends them:

• Nested functions returned inside containers deliberately lose result precision.
• Recursive relations beyond finite data are not complete: general recursive subtyping and equivalence are not implemented. The DMN backlog tracks broader recursive relations and oracle coverage.
• Repeated duration addition still combines independent intervals; preserving correlation for gapped month- or second-duration sets is precision work, not a known under-approximation.

After the existing feature set meets the gate, extensions are prioritized by actual FEEL models that lose useful information. The estimates are initial implementation or prototype ranges, not estimates for complete language designs. Their dependencies include a stable R1–R8 foundation.

These are independent options, not requirements to imitate every feature of Elixir, Hindley–Milner, or a proof assistant. Recursive types need restrictions and algorithms appropriate to recursion; polymorphism needs schemes and constraint solving; gradual typing needs an uncertainty relation distinct from optimization proofs. General dependent typing would be a separate language-design project.

"Closing the gaps" has two realistic meanings: fully honor the existing supported constructors, and add selected missing capabilities with explicit guarantees. Universal completeness of bounded inference over arbitrary programs is not a deliverable. A precise supported fragment with honest unknown answers is.

8 Primary references

• Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, 55(4), 2008. Background for denotational subtyping and the treatment of arrows.
• Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL, 1977. Background for sound approximation of computations.
• Sam Tobin-Hochstadt and Matthias Felleisen. Logical Types for Untyped Languages. ICFP, 2010. Background for extracting and composing type facts from control flow.
• Giuseppe Castagna, Guillaume Duboc, and José Valim. The Design Principles of the Elixir Type System. The Art, Science, and Engineering of Programming 8(2), article 4, 2024. DOI: 10.22152/programming-journal.org/2024/8/4.
• Giuseppe Castagna and Guillaume Duboc. Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir. Preprint, revision 4, 2 June 2026; first submitted in 2024.
• Elixir. Gradual set-theoretic types, version 1.20.4. Versioned implementation reference, consulted 17 October 2026.
• Luis Damas and Robin Milner. Principal type-schemes for functional programs. POPL, 1982. Accessible transcription.
• Patrick M. Rondon, Ming Kawaguchi, and Ranjit Jhala. Liquid Types. PLDI, 2008.
• Tobias Lindahl and Konstantinos Sagonas. Practical Type Inference Based on Success Typings. PPDP, 2006.
• Simon Marlow, editor. Haskell 2010 Language Report, chapter 4. Reference for datatypes and type classes.
• TypeScript. Type Compatibility. Official account of structural compatibility and its soundness tradeoffs.
• TypeScript. Handbook: The Basics, Narrowing, and Utility Types. Section 5.2 links the additional official type-manipulation and strictness references used in its comparisons.
• Python. Type-system concepts and typing reference. Static types, gradual assignability, and the runtime role of annotations.
• Kotlin. Null safety and Type checks and casts. Nullability, boundary limitations, and smart-cast preconditions.
• Rust. Enums and Option, exhaustive matches, recoverable errors with Result, and safe/unsafe interaction. Explicit alternatives and unchecked contracts.
• CUE. The CUE language specification. The lattice, unification, disjunction, bounds, null, and bottom.
• Erlang/OTP. Dialyzer reference. The purpose of success-typing-based discrepancy analysis.
• Elm. Maybe, Result, and JSON decoders. Explicit failure and validated external data.
• OCaml 5.5. Polymorphism and its limitations, Polymorphic variants, and Effect handlers. Generalization, variant structure, and effect-safety limits.
• F#. Automatic generalization, Discriminated unions, and Units of measure. Reusable contracts and dimensional checking.
• C#. Records, Nullable reference types, and Nullable value types. Type identity, static annotations, and runtime representations.
• Dafny. Reference manual. Explicit specifications and verification obligations.
• Idris. Tutorial introduction. Reference for value-indexed types.
• Koka. Language guide, effect types. Reference for effects alongside return types.
• Object Management Group. Decision Model and Notation 1.6. The normative language context. Implementation behavior and counterexamples in this document are established from the repository and the stated experiments, rather than inferred from this landing page.