129 KiB
129 KiB
lets review the implementation, approach and design of this logic, why does the test fail - any shortcomings in our implementation, fundamental design flaws ?
doc = """
# Ternary Decision Diagram (TDD) for Set-Theoretic Types in Elixir
## 1. Introduction
This document outlines the design and implementation of a Ternary Decision Diagram (TDD) based system for representing and manipulating set-theoretic types, inspired by systems like CDuce. The goal is to create a robust way to perform type checking, type inference, and other type-level computations for a rich set of datatypes, similar to those found in Elixir.
A TDD is a directed acyclic graph (DAG) used to represent a function `f(v1, v2, ..., vn) -> {true, false, dont_care}`. In our context, it represents a characteristic function for a type: given a value, the TDD determines if the value belongs to the type (`true`), does not belong (`false`), or if the specific predicates tested so far are insufficient or irrelevant for this particular type operation (`dont_care`).
The TDDs are kept **ordered** and **reduced** to ensure a canonical representation for each type, making type equivalence checks (and other operations) efficient.
- **Ordered**: Variables (predicates) appear in the same fixed global order on all paths from the root to a terminal.
- **Reduced**: Isomorphic subgraphs are merged (shared), and nodes whose children would make the test redundant under certain TDD algebra rules are eliminated or simplified.
## 2. Core TDD Structure and Operations
### 2.1. Nodes
There are two kinds of nodes:
1. **Terminal Nodes**:
* `TRUE_TERMINAL` (ID: `1`): Represents the universal set (type `any`). A path ending here means the value (or part of it) satisfies the type constraints along that path.
* `FALSE_TERMINAL` (ID: `0`): Represents the empty set (type `none`). A path ending here means the value fails the type constraints.
2. **Variable Nodes**:
* Represented as a tuple: `{variable_identifier, yes_child_id, no_child_id, dc_child_id}`.
* `variable_identifier`: A unique, globally ordered term identifying the predicate being tested at this node (e.g., "is the value an atom?", "is the integer value < 10?").
* `yes_child_id`: The ID of the next TDD node if the predicate is true.
* `no_child_id`: The ID of the next TDD node if the predicate is false.
* `dc_child_id` (Don't Care): The ID of the next TDD node if the predicate is irrelevant for the current type or operation. The semantic interpretation of `dc` is crucial and aligns with common TDD usage (e.g., for a union operation, `dc(A | B) = dc(A) | dc(B)`).
### 2.2. Node Management (`Tdd` module state)
The `Tdd` module maintains global state (currently via `Process.put/get` for simplicity, ideally a `GenServer`):
* `@nodes`: A map from `node_tuple ({variable, yes_id, no_id, dc_id})` to `node_id`. This ensures that structurally identical nodes are shared (part of the "reduced" property).
* `@node_by_id`: A map from `node_id` to its `node_tuple` or a terminal symbol (`:true_terminal`, `:false_terminal`).
* `@next_id`: The next available integer ID for a new node.
* `@op_cache`: A map for memoizing results of operations like `apply` (binary ops), `negate`, and `simplify_with_constraints`. Keys are typically `{{op_name, id1, id2}, result_id}` or `{{op_name, id1}, result_id}`.
### 2.3. Variable Ordering
A strict global total order of all possible `variable_identifier`s is essential. This is achieved by defining variable identifiers as Elixir tuples, which have a natural sort order.
The proposed structure for variable identifiers is:
`{category_integer, predicate_type_atom, specific_value_or_nested_id}`
Example categories:
* `0`: Primary type discriminators (e.g., `is_atom`, `is_integer`, `is_list`).
* `1`: Atom-specific predicates (e.g., `value == :foo`).
* `2`: Integer-specific predicates (e.g., `value < 10`).
* `4`: Tuple-specific predicates (e.g., `size == 2`, `element 0 has_type X`).
* And so on for other types.
### 2.4. Core Operations
1. **`make_node_raw(variable, yes_id, no_id, dc_id)`**:
* The fundamental private function for creating or retrieving unique structural nodes.
* Implements structural sharing via the `@nodes` table.
* Implements a basic reduction rule: if `yes_id == no_id == dc_id`, the node is redundant, and that common child ID is returned.
2. **`check_assumptions_consistency(assumptions_map)`**:
* A private helper function crucial for semantic reduction.
* Takes a map `%{variable_id => value (true/false/:dc)}` representing current path assumptions.
* Returns `:consistent` or `:contradiction` based on predefined semantic rules of the type system (e.g., `is_atom=true` AND `is_tuple=true` is a contradiction).
* This function will be expanded as more types and predicates are added.
3. **`simplify_with_constraints(tdd_id, assumptions_map)`**:
* A private, memoized, recursive function that takes a `tdd_id` and an `assumptions_map`.
* It produces a new `tdd_id` that is semantically equivalent to the input `tdd_id` under the given assumptions, but potentially simpler.
* **Crucial Behavior**: If `check_assumptions_consistency(assumptions_map)` returns `:contradiction` at any point, `simplify_with_constraints` immediately returns `@false_node_id`.
* If the TDD's variable is already in `assumptions_map`, it follows the constrained path.
* Otherwise, it recursively simplifies children, adding the current node's variable assignment to the assumptions for those deeper calls, and rebuilds the node using `make_node_raw`.
4. **`apply_raw(op_name, op_lambda, u1_id, u2_id)`**:
* The private, memoized, recursive Shannon expansion algorithm for binary set operations (union, intersection).
* `op_lambda` defines the operation on terminal nodes.
* It selects the `top_var` based on the global variable order.
* Recursively calls `apply_raw` on the children.
* Uses `make_node_raw` to construct result nodes.
* This function computes the *structural* result of the operation.
5. **Public API Operations (`sum/2`, `intersect/2`, `negate/1`)**:
* These functions orchestrate the operation:
1. Call the respective `_raw` version (e.g., `apply_raw` for `sum`/`intersect`, `negate_raw` for `negate`).
2. Take the `raw_result_id` from step 1.
3. Return `simplify_with_constraints(raw_result_id, %{})`. This final step ensures that all TDDs exposed through the public API are not only structurally canonical (via `make_node_raw` and `apply_raw`) but also *semantically canonical* (i.e., known impossible paths or contradictions are resolved to `@false_node_id`).
6. **Type Constructors (e.g., `type_atom()`, `type_atom_literal(:foo)`)**:
* These public functions build the TDD for a specific type.
* They use `make_node_raw` to define the basic structure.
* They then return `simplify_with_constraints(raw_id, %{})` to ensure the constructed type is in its simplest semantic form.
7. **`is_subtype(sub_id, super_id)`**:
* Defined as `simplify_with_constraints(intersect(sub_id, negate(super_id)), %{}) == @false_node_id`.
* Since `intersect` and `negate` now return semantically simplified TDDs, if `A ∩ ¬B` represents an empty set, the result of the intersection will be `@false_node_id`.
## 3. Datatype Representation Details
This section outlines how various Elixir-like datatypes are (or will be) represented using TDD variables and constructors. All constructors ensure the final TDD is passed through `simplify_with_constraints(raw_id, %{})`.
### 3.1. Atoms
* **Variables**:
* `@v_is_atom = {0, :is_atom}`: Primary type check.
* `v_atom_eq_A = {1, :value, A}`: Checks if the atom's value is `A`. Order by `A`.
* **Constructors**:
* `type_atom()`: Represents any atom. TDD: `make_node_raw(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)`.
* `type_atom_literal(val)`: Represents a specific atom. TDD: `make_node_raw(@v_is_atom, node_for_val_eq, @false_node_id, @false_node_id)` where `node_for_val_eq = make_node_raw(v_atom_eq_A, @true_node_id, @false_node_id, @false_node_id)`.
* **Semantic Constraints for `check_assumptions_consistency`**:
* If `assumptions_map` contains `{{0, :is_atom}, true}` and `{{0, other_primary_type}, true}` -> contradiction.
* If `assumptions_map` contains `{{1, :value, A}, true}` and `{{1, :value, B}, true}` where `A != B` -> contradiction.
### 3.2. Tuples
* **Variables**:
* `@v_is_tuple = {0, :is_tuple}`: Primary type check.
* `v_tuple_size_eq_N = {4, :size, N}`: Checks if tuple size is `N`. Order by `N`.
* `v_tuple_elem_I_PRED = {4, :element, Index_I, NESTED_PREDICATE_ID}`: Predicate for element at `Index_I`. `NESTED_PREDICATE_ID` is a variable from the global order, applied to the element. (e.g., `{4, :element, 0, {0, :is_atom}}` checks if element 0 is an atom). Order by `Index_I`, then by `NESTED_PREDICATE_ID`.
* **Constructors**:
* `type_tuple()`: Any tuple.
* `type_empty_tuple()`: The tuple `{}`.
* `type_tuple_sized_any(size)`: Any tuple of a given size.
* `type_tuple_specific(element_type_ids_list)`: e.g., for `{atom(), integer()}`. This will involve creating nodes for size, then for each element, applying the TDD for that element's type.
* **Semantic Constraints**:
* `is_tuple=true` vs. other primary types.
* If `{{4, :size, N}, true}` and `{{4, :size, M}, true}` where `N != M` -> contradiction.
* If `{{4, :size, N}, true}` and a predicate `{{4, :element, I, _}, _}` exists where `I >= N` -> potential contradiction or path simplification (element doesn't exist).
### 3.3. Integers (Next to Implement)
* **Variables**:
* `@v_is_integer = {0, :is_integer}` (or a new category, e.g., `2` for integer properties).
* INT_CAT variables (names of variables prefixed with `a b c` to force ordering
* `v_int_lt_N = {INT_CAT, :alt, N}` (value < N).
* `v_int_eq_N = {INT_CAT, :beq, N}`.
* `v_int_gt_N = {INT_CAT, :cgt, N}` (value > N).
* *(Consider also: `lte` (less than or equal), `gte` (greater than or equal) to simplify some range logic, or derive them).*
* **Constructors**:
* `type_integer()`: Any integer.
* `type_int_eq(n)`: A specific integer value.
* `type_int_lt(n)`, `type_int_gt(n)`.
* `type_int_range(min, max, min_inclusive, max_inclusive)`: Integers within a specific range.
* **Semantic Constraints**:
* `is_integer=true` vs. other primary types.
* `eq(N)` and `eq(M)` with `N != M` -> contradiction.
* `eq(N)` and `lt(M)` if `N >= M` -> contradiction.
* `eq(N)` and `gt(M)` if `N <= M` -> contradiction.
* `lt(N)` and `gt(M)` if `N <= M+1` (or `N <= M` if `gt` means `>=`) -> contradiction. (e.g., `x < 5` and `x > 4` has no integer solution).
* *Strategy for complex integer constraints*: Maintain a "current allowed interval" `[min_assumed, max_assumed]` based on `assumptions_map`. If this interval becomes empty or invalid, it's a contradiction. Each new integer assumption (`lt, gt, eq`) refines this interval.
### 3.4. Lists (Implemented)
* **Variables**:
* `@v_is_list = {0, :is_list}`.
* `v_list_is_empty = {5, :is_empty}`.
* *If not empty*:
* `v_list_head_pred = {5, :head, NESTED_PREDICATE_ID}`: Applies a global predicate to the head.
* `v_list_tail_pred = {5, :tail, NESTED_PREDICATE_ID_FOR_TAIL}`: Applies a global predicate (usually list predicates) to the tail.
* **Constructors**:
* `type_list()`: Represents any list.
* `type_empty_list()`: Represents the empty list `[]`.
* `type_cons(head_type_id, tail_type_id)`: Represents a non-empty list `[H|T]` where `H` is of type `head_type_id` and `T` is of type `tail_type_id`.
* **Semantic Constraints**:
* `is_list=true` vs. other primary types.
* If `is_empty=true`, any predicate on the `head` or `tail` is a contradiction.
* Recursive consistency checks on `head` and `tail` sub-types.
### 3.5. Strings & Binaries (Planned)
* **Variables**:
* `@v_is_binary = {0, :is_binary}`.
* `@v_is_string = {0, :is_string}` (can be a check after `is_binary` or a distinct primary type if model demands).
* Size/length predicates: `v_binary_size_eq_N`, `v_string_length_eq_N`.
* Content predicates: `v_string_eq_S`, `v_string_prefix_P`, `v_string_suffix_S`, `v_string_matches_regex_R`.
* **Semantic Constraints**: Size vs content (e.g., `size=1` and `prefix="foo"` is a contradiction). `eq(S1)` and `eq(S2)` if `S1 != S2`.
### 3.6. Maps (Planned - Complex)
* **Variables**:
* `@v_is_map = {0, :is_map}`.
* `v_map_size_eq_N`.
* `v_map_has_key_K`: (K is a canonical representation of an Elixir term).
* *If `has_key_K` is true*:
* `v_map_key_K_value_VAR = {MAP_CAT, :key_value, K, NESTED_PREDICATE_ID}`: Applies a global predicate to the value associated with key K.
* For `%{pattern_key => pattern_value}` types:
* This requires careful thought. Might involve predicates like `v_map_all_keys_matching_TYPE_X_have_values_matching_TYPE_Y`.
* **Semantic Constraints**: `is_map` vs. others. Size vs. `has_key` interactions. Contradictory type requirements for the same key's value.
### 3.7. Functions (Planned - Very Complex)
* Representation of function types (`fun((Arg1Type, Arg2Type, ...) -> ReturnType)`) is a significant challenge for TDDs.
* **Variables (Tentative)**:
* `@v_is_function = {0, :is_function}`.
* `v_fun_arity_eq_A`.
* Predicates for argument types at specific positions (e.g., `v_fun_arg_I_type_VAR`).
* Predicates for return type (e.g., `v_fun_return_type_VAR`).
* Intersection and union of function types involve concepts like contravariance of arguments and covariance of return types. This may require specialized logic beyond simple TDD operations or a very elaborate variable scheme. Often, function types are handled with auxiliary structures in type systems.
## 4. Current Status & Next Steps
* **Implemented**: Atoms, basic Tuples (any, empty, sized_any). Core TDD operations (`sum`, `intersect`, `negate`, `is_subtype`) with semantic simplification framework (`simplify_with_constraints` and `check_assumptions_consistency`).
* **Passing Tests**: A suite of tests for atom/tuple interactions, unions, intersections, negations, and subtyping, including resolution of contradictions like `atom & tuple == none`.
* **Next Immediate Step**: Implement **Integer types** as outlined in section 3.3. This will involve:
1. Defining integer-specific predicates and their global order.
2. Creating integer type constructors.
3. Significantly expanding `check_assumptions_consistency` to handle integer comparisons (`eq`, `lt`, `gt`) and their interactions.
4. Adding comprehensive tests for integers.
## 5. Future Considerations
* **Performance**: For very large TDDs or complex types, the number of nodes and cache sizes can grow. Investigate optimizations if needed.
* **Generality of `check_assumptions_consistency`**: Designing this to be easily extensible and correct for many interacting predicates is challenging. A rule-based system or a more abstract way to define predicate interactions might be beneficial.
* **"Don't Care" (`dc`) branch semantics**: Ensure the `dc` branch is consistently and correctly handled in all operations, especially `simplify_with_constraints` if assumptions can make a variable "don't care". Currently, `simplify_with_constraints` assumes `true/false/:dc` values in the `assumptions_map` if a variable is already constrained.
* **Type Inference**: Using the TDD operations to infer types or solve type constraints.
* **Polymorphism**: Representing and operating on types with free type variables. Typically, free variables are treated as `any` or involve substitution before TDD construction.
This document provides a snapshot of the current TDD system and a roadmap for its extension. The core principle is the combination of structurally canonical ROBDDs (via `make_node_raw` and `apply_raw`) with a semantic simplification layer (`simplify_with_constraints`) that embeds knowledge of the type system's rules.
"""
defmodule Tdd.Core do
@moduledoc """
The core, semantically-unaware TDD graph engine.
This module is responsible for:
- Storing and managing a unique table of TDD nodes.
- Providing a function `make_node/4` that creates nodes while ensuring
structural sharing and basic reduction (redundant nodes).
- Implementing a generic, structural `apply/4` algorithm for binary
operations on TDDs.
It knows nothing about what the variables (`{0, :is_atom}`, etc.) mean.
"""
# --- Terminal Node IDs ---
@false_node_id 0
@true_node_id 1
def true_id, do: @true_node_id
def false_id, do: @false_node_id
defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id
def terminal_id?(id) when is_terminal_id(id), do: true
def terminal_id?(_), do: false
# --- State Management ---
def init do
Process.put(:tdd_nodes, %{})
Process.put(:tdd_node_by_id, %{@false_node_id => false, @true_node_id => true})
Process.put(:tdd_next_id, 2)
Process.put(:tdd_op_cache, %{})
:ok
end
defp get_state do
%{
nodes: Process.get(:tdd_nodes, %{}),
node_by_id: Process.get(:tdd_node_by_id, %{@false_node_id => false, @true_node_id => true}),
next_id: Process.get(:tdd_next_id, 2),
op_cache: Process.get(:tdd_op_cache, %{})
}
end
defp update_state(changes) do
current_state = get_state()
new_state = Map.merge(current_state, changes)
Process.put(:tdd_nodes, new_state.nodes)
Process.put(:tdd_node_by_id, new_state.node_by_id)
Process.put(:tdd_next_id, new_state.next_id)
Process.put(:tdd_op_cache, new_state.op_cache)
end
def clear_op_cache, do: Process.put(:tdd_op_cache, %{})
# --- Public API for the Core Engine ---
def get_node(id) when is_terminal_id(id), do: if(id == @true_node_id, do: true, else: false)
def get_node(id), do: get_state().node_by_id[id]
def get_op_cache(key), do: get_state().op_cache[key]
def put_op_cache(key, value),
do: update_state(%{op_cache: Map.put(get_state().op_cache, key, value)})
@doc """
Creates or retrieves a unique TDD node.
This is the heart of structural canonicalization (the 'R' in ROBDD).
"""
def make_node(variable, yes_id, no_id, dc_id) do
# NEW, MORE POWERFUL REDUCTION RULE:
# If the 'yes' and 'no' paths lead to the same result, the test on this
# variable is redundant. The entire node can be replaced by that result.
cond do
yes_id == no_id ->
yes_id
yes_id == dc_id && no_id == dc_id ->
yes_id
true ->
state = get_state()
node_tuple = {variable, yes_id, no_id, dc_id}
if Map.has_key?(state.nodes, node_tuple) do
state.nodes[node_tuple]
else
new_id = state.next_id
update_state(%{
nodes: Map.put(state.nodes, node_tuple, new_id),
node_by_id: Map.put(state.node_by_id, new_id, node_tuple),
next_id: new_id + 1
})
new_id
end
end
end
@doc """
The generic Shannon expansion algorithm for any binary operation.
This is purely structural and relies on the caller (the semantic layer)
to ensure the inputs and results are meaningful.
"""
def apply(op_name, op_lambda, u1_id, u2_id) do
state = get_state()
cache_key = {op_name, Enum.sort([u1_id, u2_id])}
cond do
Map.has_key?(state.op_cache, cache_key) ->
state.op_cache[cache_key]
is_terminal_id(u1_id) && is_terminal_id(u2_id) ->
res_terminal = op_lambda.(get_node(u1_id), get_node(u2_id))
if res_terminal == true, do: @true_node_id, else: @false_node_id
true ->
u1_details = get_node(u1_id)
u2_details = get_node(u2_id)
result_id =
cond do
u1_details == true or u1_details == false ->
{var2, y2, n2, d2} = u2_details
res_y = apply(op_name, op_lambda, u1_id, y2)
res_n = apply(op_name, op_lambda, u1_id, n2)
res_d = apply(op_name, op_lambda, u1_id, d2)
make_node(var2, res_y, res_n, res_d)
u2_details == true or u2_details == false ->
{var1, y1, n1, d1} = u1_details
res_y = apply(op_name, op_lambda, y1, u2_id)
res_n = apply(op_name, op_lambda, n1, u2_id)
res_d = apply(op_name, op_lambda, d1, u2_id)
make_node(var1, res_y, res_n, d1)
true ->
{var1, y1, n1, d1} = u1_details
{var2, y2, n2, d2} = u2_details
top_var = Enum.min([var1, var2])
res_y =
apply(
op_name,
op_lambda,
if(var1 == top_var, do: y1, else: u1_id),
if(var2 == top_var, do: y2, else: u2_id)
)
res_n =
apply(
op_name,
op_lambda,
if(var1 == top_var, do: n1, else: u1_id),
if(var2 == top_var, do: n2, else: u2_id)
)
res_d =
apply(
op_name,
op_lambda,
if(var1 == top_var, do: d1, else: u1_id),
if(var2 == top_var, do: d2, else: u2_id)
)
make_node(top_var, res_y, res_n, res_d)
end
update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
result_id
end
end
end
defmodule Tdd.PredicateLogic do
@moduledoc "..."
alias Tdd.Variables, as: V
@primary_types [:is_atom, :is_tuple, :is_integer, :is_list]
@primary_type_exclusivity_rules (for type <- @primary_types, into: %{} do
antecedent = {{0, type}, true}
consequents =
for other_type <- @primary_types,
other_type != type,
do: {{{0, other_type}, false}}
{antecedent, consequents}
end)
@rules @primary_type_exclusivity_rules
def saturate(assumptions) do
case apply_static_rules(assumptions) do
{:ok, saturated_facts} -> final_check(saturated_facts)
:contradiction -> :contradiction
{:contradiction, _} -> :contradiction
end
end
defp apply_static_rules(facts) do
Enum.reduce(facts, {:ok, facts}, fn {var, val}, {status, acc_facts} ->
if status == :contradiction do
{:contradiction, %{}}
else
rules_for_fact = Map.get(@rules, {var, val}, [])
# --- THE CORRECTED PATTERN MATCH IS HERE ---
# The data is `{{{Var, Val}}}`. We need to match this shape.
Enum.reduce_while(rules_for_fact, {:ok, acc_facts}, fn {{consequent_var, consequent_val}},
{_st, inner_facts} ->
case Map.get(inner_facts, consequent_var) do
nil -> {:cont, {:ok, Map.put(inner_facts, consequent_var, consequent_val)}}
^consequent_val -> {:cont, {:ok, inner_facts}}
_ -> {:halt, {:contradiction, %{}}}
end
end)
end
end)
end
defp final_check(facts) do
cond do
check_atom_values(facts) == :contradiction -> :contradiction
check_tuple_values(facts) == :contradiction -> :contradiction
check_integer_ranges(facts) == :contradiction -> :contradiction
check_list_structure(facts) == :contradiction -> :contradiction
true -> {:ok, facts}
end
end
defp check_atom_values(facts) do
trues =
Enum.reduce(facts, MapSet.new(), fn
{{1, :value, atom_val}, true}, acc -> MapSet.put(acc, atom_val)
_, acc -> acc
end)
if MapSet.size(trues) > 1, do: :contradiction, else: :ok
end
defp check_tuple_values(facts) do
trues =
Enum.reduce(facts, MapSet.new(), fn
{{4, :size, size_val}, true}, acc -> MapSet.put(acc, size_val)
_, acc -> acc
end)
if MapSet.size(trues) > 1, do: :contradiction, else: :ok
end
defp check_list_structure(facts) do
is_assumed_empty = Map.get(facts, V.v_list_is_empty()) == true
if is_assumed_empty do
has_head_or_tail_pred =
Enum.any?(facts, fn {var, _} ->
case var do
{5, :head, _} -> true
{5, :tail, _} -> true
_ -> false
end
end)
if has_head_or_tail_pred, do: :contradiction, else: :ok
else
:ok
end
end
# --- Integer Logic ---
# THIS IS THE SINGLE, CORRECT DEFINITION TO USE
defp check_integer_ranges(facts) do
if facts[V.v_is_integer()] != true do
:ok
else
if calculate_integer_interval(facts) == :contradiction, do: :contradiction, else: :ok
end
end
@doc """
A general-purpose reasoner that uses the main `saturate` function.
It determines if a predicate is implied true or false by a set of constraints
by checking if adding its opposite leads to a contradiction.
"""
defp _reason_by_contradiction(predicate, constraints) do
# Is `predicate` implied TRUE? (i.e., is `constraints AND NOT predicate` a contradiction?)
cond do
saturate(Map.put(constraints, predicate, false)) == :contradiction ->
true
# Is `predicate` implied FALSE? (i.e., is `constraints AND predicate` a contradiction?)
saturate(Map.put(constraints, predicate, true)) == :contradiction ->
false
true ->
:unknown
end
end
@doc """
Checks if a `predicate` is logically implied (or contradicted) by a
set of `constraints`.
"""
def check_implication(predicate, constraints) do
case predicate do
# --- NEW HANDLER for primary type predicates ---
{0, _} ->
_reason_by_contradiction(predicate, constraints)
# --- EXISTING BASE CASES ---
{1, :value, _} ->
_atom_implication(predicate, constraints)
{2, _, _} ->
_integer_implication(predicate, constraints)
{4, :size, _} ->
_tuple_size_implication(predicate, constraints)
# --- EXISTING RECURSIVE CASES ---
{4, :element, index, inner_predicate} ->
element_constraints =
gather_local_constraints(constraints, &match?({4, :element, ^index, _}, &1))
check_implication(inner_predicate, element_constraints)
{5, :head, inner_predicate} ->
head_constraints =
gather_local_constraints(constraints, &match?({5, :head, _}, &1))
check_implication(inner_predicate, head_constraints)
{5, :tail, inner_predicate} ->
tail_constraints =
gather_local_constraints(constraints, &match?({5, :tail, _}, &1))
check_implication(inner_predicate, tail_constraints)
# --- DEFAULT CASE ---
_ ->
# We don't have specific reasoning logic for this predicate type.
:unknown
end
end
# ===================================================================
# == PRIVATE HELPERS
# ===================================================================
# --- Constraint Isolation Helper ---
@doc """
Gathers, unwraps, and isolates constraints for a specific component.
"""
defp gather_local_constraints(all_constraints, filter_fun) do
for {var, bool_val} <- all_constraints,
filter_fun.(var),
into: %{} do
# Unwrap the predicate for the local check.
# e.g., from `{4, :element, 0, {2, :beq, 5}}` we want `{2, :beq, 5}`
inner_predicate = elem(var, tuple_size(var) - 1)
{inner_predicate, bool_val}
end
end
# --- Base Case Reasoners ---
# Reasoner for integer predicates.
# Renamed from `check_integer_implication` to `_integer_implication` to denote it's a private helper.
defp _integer_implication(predicate, constraints) do
case calculate_integer_interval(constraints) do
:contradiction ->
# A contradiction implies anything.
true
{min_val, max_val} ->
{_p_cat, p_type, p_val} = predicate
cond do
# The current interval [min, max] is a SUBSET of the predicate's interval
(p_type == :alt and is_integer(max_val) and max_val < p_val) or
(p_type == :cgt and is_integer(min_val) and min_val > p_val) or
(p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) ->
true
# The current interval [min, max] is DISJOINT from the predicate's interval
(p_type == :alt and is_integer(min_val) and min_val >= p_val) or
(p_type == :cgt and is_integer(max_val) and max_val <= p_val) or
(p_type == :beq and
((is_integer(min_val) and min_val > p_val) or
(is_integer(max_val) and max_val < p_val))) ->
false
true ->
:unknown
end
end
end
# Reasoner for atom predicates using Enum.reduce
defp _atom_implication(predicate, constraints) do
# The predicate we are testing, e.g., {{1, :value, :foo}, true}
{{1, :value, p_val}, _} = {predicate, true}
# Use Enum.reduce to find all atom values constrained to be true or false.
{true_atoms, false_atoms} =
Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn
# Match a constraint that an atom value MUST be true
{{1, :value, val}, true}, {true_set, false_set} ->
{MapSet.put(true_set, val), false_set}
# Match a constraint that an atom value MUST be false
{{1, :value, val}, false}, {true_set, false_set} ->
{true_set, MapSet.put(false_set, val)}
# Ignore any other kind of constraint
_, acc ->
acc
end)
cond do
# If the predicate's value is explicitly known to be false.
p_val in false_atoms ->
false
# If the predicate's value is explicitly known to be true.
p_val in true_atoms ->
true
# If we know the value MUST be something else (and it's not our predicate's value).
# e.g., constraints say the value is :bar, and we're checking for :foo.
not Enum.empty?(true_atoms) and p_val not in true_atoms ->
false
# Otherwise, we don't have enough information.
true ->
:unknown
end
end
# Reasoner for tuple size predicates using Enum.reduce
defp _tuple_size_implication(predicate, constraints) do
# The predicate we are testing, e.g., {{4, :size, 2}, true}
{{4, :size, p_val}, _} = {predicate, true}
{true_sizes, false_sizes} =
Enum.reduce(constraints, {MapSet.new(), MapSet.new()}, fn
{{4, :size, val}, true}, {true_set, false_set} ->
{MapSet.put(true_set, val), false_set}
{{4, :size, val}, false}, {true_set, false_set} ->
{true_set, MapSet.put(false_set, val)}
_, acc ->
acc
end)
cond do
# If the predicate's size is explicitly known to be false.
p_val in false_sizes ->
false
# If the predicate's size is explicitly known to be true.
p_val in true_sizes ->
true
# If we know the size MUST be something else.
not Enum.empty?(true_sizes) and p_val not in true_sizes ->
false
# Otherwise, we don't know.
true ->
:unknown
end
end
defp check_integer_implication(predicate, constraints) do
if constraints[V.v_is_integer()] != true do
:unknown
else
case calculate_integer_interval(constraints) do
:contradiction ->
true
{min_val, max_val} ->
{_p_cat, p_type, p_val} = predicate
cond do
(p_type == :alt and is_integer(max_val) and max_val < p_val) or
(p_type == :cgt and is_integer(min_val) and min_val > p_val) or
(p_type == :beq and !is_nil(min_val) and min_val == p_val and max_val == p_val) ->
true
(p_type == :alt and is_integer(min_val) and min_val >= p_val) or
(p_type == :cgt and is_integer(max_val) and max_val <= p_val) or
(p_type == :beq and
((is_integer(min_val) and min_val > p_val) or
(is_integer(max_val) and max_val < p_val))) ->
false
true ->
:unknown
end
end
end
end
defp calculate_integer_interval(facts) do
bounds =
Enum.reduce(facts, %{eq: nil, min: nil, max: nil}, fn
{var, true}, acc ->
case var do
{2, :beq, n} ->
if(is_nil(acc.eq) or acc.eq == n, do: %{acc | eq: n}, else: %{acc | eq: :conflict})
{2, :alt, n} ->
%{acc | max: min_opt(acc.max, n - 1)}
{2, :cgt, n} ->
%{acc | min: max_opt(acc.min, n + 1)}
_ ->
acc
end
{var, false}, acc ->
case var do
{2, :alt, n} -> %{acc | min: max_opt(acc.min, n)}
{2, :cgt, n} -> %{acc | max: min_opt(acc.max, n)}
_ -> acc
end
_, acc ->
acc
end)
cond do
bounds.eq == :conflict ->
:contradiction
is_integer(bounds.eq) ->
if (is_nil(bounds.min) or bounds.eq >= bounds.min) and
(is_nil(bounds.max) or bounds.eq <= bounds.max) do
{bounds.eq, bounds.eq}
else
:contradiction
end
is_integer(bounds.min) and is_integer(bounds.max) and bounds.min > bounds.max ->
:contradiction
true ->
{bounds.min, bounds.max}
end
end
defp min_opt(nil, x), do: x
defp min_opt(x, nil), do: x
defp min_opt(x, y), do: min(x, y)
defp max_opt(nil, x), do: x
defp max_opt(x, nil), do: x
defp max_opt(x, y), do: max(x, y)
end
defmodule Tdd do
@moduledoc """
The main public API and semantic layer for the TDD system.
It uses Tdd.Core for graph manipulation and Tdd.PredicateLogic
for reasoning about type system rules.
This layer implements the high-level, type-aware algorithms for
intersection, union, negation, and subtyping.
"""
alias Tdd.Core
alias Tdd.PredicateLogic
alias Tdd.Variables, as: V
# --- System Init ---
def init_tdd_system do
Core.init()
IO.puts("TDD system initialized with new architecture.")
end
# --- Variable Definitions (could be in their own module) ---
defmodule Variables do
def v_is_atom, do: {0, :is_atom}
def v_is_tuple, do: {0, :is_tuple}
def v_is_integer, do: {0, :is_integer}
def v_is_list, do: {0, :is_list}
def v_atom_eq(v), do: {1, :value, v}
def v_int_eq(n), do: {2, :beq, n}
def v_int_lt(n), do: {2, :alt, n}
def v_int_gt(n), do: {2, :cgt, n}
def v_tuple_size_eq(n), do: {4, :size, n}
def v_tuple_elem_pred(i, v), do: {4, :element, i, v}
def v_list_is_empty, do: {5, :is_empty}
def v_list_head_pred(v), do: {5, :head, v}
def v_list_tail_pred(v), do: {5, :tail, v}
def v_list_all_elements_are(id), do: {5, :all_elements, id}
end
# --- Type Constructors (Completed) ---
def type_any, do: Core.true_id()
def type_none, do: Core.false_id()
# Base type constructors
def type_atom, do: Core.make_node(V.v_is_atom(), type_any(), type_none(), type_none())
def type_tuple, do: Core.make_node(V.v_is_tuple(), type_any(), type_none(), type_none())
def type_integer, do: Core.make_node(V.v_is_integer(), type_any(), type_none(), type_none())
def type_list, do: Core.make_node(V.v_is_list(), type_any(), type_none(), type_none())
# --- Atom Constructors ---
def type_atom_literal(val) do
# A specific atom is the intersection of `atom()` and `value == val`.
constraint_node = Core.make_node(V.v_atom_eq(val), type_any(), type_none(), type_none())
intersect(type_atom(), constraint_node)
end
# --- Integer Constructors ---
def type_int_eq(n) do
# A specific integer is the intersection of `integer()` and `value == n`.
constraint_node = Core.make_node(V.v_int_eq(n), type_any(), type_none(), type_none())
intersect(type_integer(), constraint_node)
end
def type_int_lt(n) do
# An integer `< n` is the intersection of `integer()` and `value < n`.
constraint_node = Core.make_node(V.v_int_lt(n), type_any(), type_none(), type_none())
intersect(type_integer(), constraint_node)
end
def type_int_gt(n) do
# An integer `> n` is the intersection of `integer()` and `value > n`.
constraint_node = Core.make_node(V.v_int_gt(n), type_any(), type_none(), type_none())
intersect(type_integer(), constraint_node)
end
# --- Tuple Constructors ---
def type_empty_tuple do
# `{}` is the intersection of `tuple()` and `size == 0`.
constraint_node = Core.make_node(V.v_tuple_size_eq(0), type_any(), type_none(), type_none())
intersect(type_tuple(), constraint_node)
end
def type_tuple_sized_any(size) do
# A tuple of a fixed size is the intersection of `tuple()` and `size == N`.
constraint_node =
Core.make_node(V.v_tuple_size_eq(size), type_any(), type_none(), type_none())
intersect(type_tuple(), constraint_node)
end
def type_tuple(element_type_ids) when is_list(element_type_ids) do
# This is the most complex tuple constructor. It represents a tuple with
# a specific size and specific types for each element.
# e.g., type_tuple([type_atom(), type_integer()]) for `{atom(), integer()}`
num_elements = length(element_type_ids)
# 1. Start with the base constraint: a tuple of the correct size.
base_type = type_tuple_sized_any(num_elements)
# 2. Iteratively intersect with constraints for each element's type.
Enum.reduce(Enum.with_index(element_type_ids), base_type, fn {elem_type_id, index}, acc_tdd ->
# For each element, we create a TDD that represents the constraint on that element.
# `map_tdd_to_component` wraps all predicates of `elem_type_id` inside
# `v_tuple_elem_pred(index, ...)`, effectively focusing the type check
# on just that element of the tuple.
elem_constraint_tdd =
map_tdd_to_component(elem_type_id, &V.v_tuple_elem_pred(index, &1), type_any())
# Intersect the accumulated TDD with the new element constraint.
intersect(acc_tdd, elem_constraint_tdd)
end)
end
# --- List Constructors ---
def type_empty_list do
# `[]` is the intersection of `list()` and `is_empty == true`.
constraint_node = Core.make_node(V.v_list_is_empty(), type_any(), type_none(), type_none())
intersect(type_list(), constraint_node)
end
def type_cons(head_type_id, tail_type_id) do
# A cons cell `[H|T]` is a list that is NOT empty, where the head
# has type H and the tail has type T.
# 1. Base type: a non-empty list.
non_empty_list = intersect(type_list(), negate(type_empty_list()))
# 2. Create the constraint for the head's type.
head_constraint =
map_tdd_to_component(head_type_id, &V.v_list_head_pred/1, type_any())
# 3. Create the constraint for the tail's type.
tail_constraint =
map_tdd_to_component(tail_type_id, &V.v_list_tail_pred/1, type_any())
# 4. Intersect them all together.
non_empty_list
|> intersect(head_constraint)
|> intersect(tail_constraint)
end
def type_list_of(element_type_id) do
# The type `list(T)` is a list where `all_elements` have type T.
# This predicate `{5, :all_elements, T}` is a "macro" predicate that implies
# a recursive check. The logic for handling its interaction with other
# list predicates must be encoded in the `intersect` algorithm itself
# (or more precisely, in `PredicateLogic` if it implies other simple facts).
# For now, we represent it with a single node.
# If T is `any`, then `list(any)` is just `list()`.
if element_type_id == type_any() do
type_list()
else
constraint_node =
Core.make_node(
V.v_list_all_elements_are(element_type_id),
type_any(),
type_none(),
type_none()
)
intersect(type_list(), constraint_node)
end
end
# --- High-Level Operations ---
def intersect(u1_id, u2_id), do: do_op(:intersect, u1_id, u2_id, %{}) |> simplify(%{})
def sum(u1_id, u2_id), do: do_op(:sum, u1_id, u2_id, %{}) |> simplify(%{})
def negate(u_id) do
negate_recursive(u_id, %{})
|> simplify(%{})
end
def is_subtype(sub_id, super_id) do
# A <: B <=> A & ~B == none
IO.inspect("sub_id in is_subtype")
Tdd.print_tdd(sub_id)
IO.inspect("negate(super_id) in is_subtype")
Tdd.print_tdd(negate(super_id))
IO.inspect("intersect(sub_id, negate(super_id)) in is_subtype")
Tdd.print_tdd(intersect(sub_id, negate(super_id)))
intersect(sub_id, negate(super_id)) == type_none()
end
# NEW DEDICATED NEGATE FUNCTION
defp negate_recursive(id, constraints) do
# Memoization
cache_key = {:negate, id, Map.to_list(constraints) |> Enum.sort()}
res =
if cached = Core.get_op_cache(cache_key) do
cached
else
compute_negate(id, constraints)
end
Core.put_op_cache(cache_key, res)
res
end
defp compute_negate(id, constraints) do
case PredicateLogic.saturate(constraints) do
:contradiction ->
# not(contradiction) is not(false) which is true
type_any()
{:ok, saturated_constraints} ->
# First, simplify the node we are about to negate
s_id = simplify(id, saturated_constraints)
case Core.get_node(s_id) do
true ->
type_none()
false ->
type_any()
{var, y, n, d} ->
# Recurse, adding the constraint for each branch
res_y = negate_recursive(y, Map.put(saturated_constraints, var, true))
res_n = negate_recursive(n, Map.put(saturated_constraints, var, false))
res_d = negate_recursive(d, Map.put(saturated_constraints, var, :dc))
Core.make_node(var, res_y, res_n, res_d)
end
end
end
# --- Core Recursive Operation Logic ---
defp do_op(op_name, u1_id, u2_id, constraints) do
# Memoization using the Core cache
cache_key = {op_name, Enum.sort([u1_id, u2_id]), Map.to_list(constraints) |> Enum.sort()}
if cached = Core.get_op_cache(cache_key) do
cached
else
res = compute_op(op_name, u1_id, u2_id, constraints)
Core.put_op_cache(cache_key, res)
res
end
end
defp compute_op(op_name, u1_id, u2_id, constraints) do
case PredicateLogic.saturate(constraints) do
:contradiction ->
# This path is impossible. For an intersection, the result is the empty set.
handle_contradiction(op_name)
{:ok, saturated_constraints} ->
# REMOVED: No more pre-simplifying inputs here.
# We pass the original IDs and the full context to dispatch_op.
n1 = Core.get_node(u1_id)
n2 = Core.get_node(u2_id)
dispatch_op(op_name, u1_id, n1, u2_id, n2, saturated_constraints)
end
end
# If a path is contradictory, what does it mean for the operation?
# For intersection, it's `none`. For union, it depends on the other branch.
# This function is a placeholder for more complex logic if needed.
# For now, `none` for intersect and negate is safe. For `sum`, it's more complex.
defp handle_contradiction(:intersect), do: type_none()
# ¬(false) = true
defp handle_contradiction(:negate), do: type_any()
# a+b, if a is impossible, result is b. Needs other branch info.
defp handle_contradiction(:sum), do: type_none()
# This is the replacement for the "implied value" check in the old `simplify_with_constraints`.
def simplify(id, constraints) do
# Memoization is critical for performance
cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()}
if cached = Core.get_op_cache(cache_key) do
cached
else
# We will call saturate at the beginning of the operation (in compute_op),
# so we can assume constraints are consistent here.
res = compute_simplify(id, constraints)
Core.put_op_cache(cache_key, res)
res
end
end
defp compute_simplify(id, constraints) do
case Core.get_node(id) do
true ->
type_any()
false ->
type_none()
{var, y, n, d} ->
contradiction =
case var do
{5, :head, head_predicate} ->
all_elements_type_id =
Enum.find_value(constraints, fn
{{5, :all_elements, type_id}, true} -> type_id
_ -> nil
end)
if all_elements_type_id do
head_type = predicate_to_tdd(head_predicate)
# Is the required head type compatible with the element type?
intersect(head_type, all_elements_type_id) == type_none()
else
false
end
{5, :tail, tail_predicate} ->
all_elements_type_id =
Enum.find_value(constraints, fn
{{5, :all_elements, type_id}, true} -> type_id
_ -> nil
end)
if all_elements_type_id do
tail_type = predicate_to_tdd(tail_predicate)
# The tail must be a list of the element type.
required_tail_type = type_list_of(all_elements_type_id)
intersect(tail_type, required_tail_type) == type_none()
else
false
end
_ ->
false
end
if contradiction do
# The 'yes' branch is impossible. The node simplifies to its 'no' branch.
simplify(n, constraints)
else
case Map.get(constraints, var) do
true ->
simplify(y, constraints)
false ->
simplify(n, constraints)
:dc ->
simplify(d, constraints)
nil ->
case PredicateLogic.check_implication(var, constraints) do
true ->
simplify(y, constraints)
false ->
simplify(n, constraints)
:unknown ->
res_y = simplify(y, Map.put(constraints, var, true))
res_n = simplify(n, Map.put(constraints, var, false))
res_d = simplify(d, Map.put(constraints, var, :dc))
Core.make_node(var, res_y, res_n, res_d)
end
end
end
end
end
defp dispatch_op(op_name, u1_id, n1, u2_id, n2, constraints) do
# --- Step 1: Simplify the current nodes under the given constraints. ---
# This is the crucial change. We simplify first, before doing anything else.
s1_id = simplify(u1_id, constraints)
s2_id = simplify(u2_id, constraints)
# If simplification resolved either to a terminal, we can take a shortcut.
if Core.terminal_id?(s1_id) or Core.terminal_id?(s2_id) do
apply_terminals(op_name, s1_id, s2_id)
else
# --- Step 2: Get details of the *simplified* nodes and proceed. ---
sn1 = Core.get_node(s1_id)
sn2 = Core.get_node(s2_id)
{var1, y1, n1_child, d1} = sn1
{var2, y2, n2_child, d2} = sn2
top_var = Enum.min([var1, var2])
# Determine children for the recursive call based on top_var.
call_y1 = if(var1 == top_var, do: y1, else: s1_id)
call_y2 = if(var2 == top_var, do: y2, else: s2_id)
call_n1 = if(var1 == top_var, do: n1_child, else: s1_id)
call_n2 = if(var2 == top_var, do: n2_child, else: s2_id)
call_d1 = if(var1 == top_var, do: d1, else: s1_id)
call_d2 = if(var2 == top_var, do: d2, else: s2_id)
# --- Step 3: Recurse with the original do_op entry point ---
res_y = do_op(op_name, call_y1, call_y2, Map.put(constraints, top_var, true))
res_n = do_op(op_name, call_n1, call_n2, Map.put(constraints, top_var, false))
res_d = do_op(op_name, call_d1, call_d2, Map.put(constraints, top_var, :dc))
Core.make_node(top_var, res_y, res_n, res_d)
end
end
defp apply_terminals(op_name, id1, id2) do
lambda = op_lambda(op_name)
n1 = Core.get_node(id1)
n2 = Core.get_node(id2)
# If both are terminals, just apply the op.
if Core.terminal_id?(id1) and Core.terminal_id?(id2) do
if lambda.(n1, n2), do: type_any(), else: type_none()
else
# If only one is a terminal, we must recurse on the other's children.
# This ensures correctness for operations like `A & true -> A`.
non_terminal_id = if(Core.terminal_id?(id1), do: id2, else: id1)
terminal_id = if(Core.terminal_id?(id1), do: id1, else: id2)
{var, y, n, d} = Core.get_node(non_terminal_id)
res_y = apply_terminals(op_name, y, terminal_id)
res_n = apply_terminals(op_name, n, terminal_id)
res_d = apply_terminals(op_name, d, terminal_id)
Core.make_node(var, res_y, res_n, res_d)
end
end
defp op_lambda(:intersect) do
fn
false, _ -> false
_, false -> false
true, v2 -> v2
v1, true -> v1
end
end
defp op_lambda(:sum) do
fn
true, _ -> true
_, true -> true
false, v2 -> v2
v1, false -> v1
end
end
# Helper from original code, still useful for constructors
defp map_tdd_to_component(tdd_id, wrapper_fun, success_id) do
case Core.get_node(tdd_id) do
true ->
success_id
false ->
type_none()
{var, y, n, d} ->
component_var = wrapper_fun.(var)
res_y = map_tdd_to_component(y, wrapper_fun, success_id)
res_n = map_tdd_to_component(n, wrapper_fun, success_id)
res_d = map_tdd_to_component(d, wrapper_fun, success_id)
Core.make_node(component_var, res_y, res_n, res_d)
end
end
@doc """
Converts a single predicate variable into a full TDD type.
This is the key to comparing predicates with other TDD types.
"""
defp predicate_to_tdd(predicate) do
# Memoize for performance, as this might be called repeatedly.
cache_key = {:predicate_to_tdd, predicate}
if cached = Core.get_op_cache(cache_key) do
cached
else
res =
case predicate do
{0, :is_atom} -> type_atom()
{0, :is_tuple} -> type_tuple()
{0, :is_integer} -> type_integer()
{0, :is_list} -> type_list()
{1, :value, val} -> type_atom_literal(val)
{2, :beq, n} -> type_int_eq(n)
{2, :alt, n} -> type_int_lt(n)
{2, :cgt, n} -> type_int_gt(n)
{4, :size, n} -> type_tuple_sized_any(n)
{5, :is_empty} -> type_empty_list()
# A head/tail predicate implies the value is a list AND has that head/tail.
# The inner predicate is what we care about for the type check.
{5, :head, inner_p} -> predicate_to_tdd(inner_p)
{5, :tail, inner_p} -> predicate_to_tdd(inner_p)
{5, :all_elements, type_id} -> type_list_of(type_id)
# A tuple element predicate is about the element, not the tuple itself.
{4, :element, _, inner_p} -> predicate_to_tdd(inner_p)
# Fallback for unknown/complex predicates: assume they can be anything.
_ -> type_any()
end
Core.put_op_cache(cache_key, res)
res
end
end
@doc """
Prints a human-readable representation of a TDD, starting from the given ID.
It recursively prints the structure of the graph.
"""
def print_tdd(id, indent \\ 0) do
prefix = String.duplicate(" ", indent)
# Use Tdd.Core to get node details
details = Core.get_node(id)
IO.puts("#{prefix}ID #{id}: #{inspect(details)}")
case details do
# A variable node
{_var, y, n, d} ->
IO.puts("#{prefix} Yes ->")
print_tdd(y, indent + 1)
IO.puts("#{prefix} No ->")
print_tdd(n, indent + 1)
IO.puts("#{prefix} DC ->")
print_tdd(d, indent + 1)
# Terminal nodes (:true or :false)
true ->
:ok
false ->
:ok
# Handle cases where an ID might not be found
nil ->
IO.puts("#{prefix} Error: Unknown ID #{id}")
end
end
end
# --- Example Usage ---
Tdd.init_tdd_system()
# Basic Types
tdd_foo = Tdd.type_atom_literal(:foo)
tdd_bar = Tdd.type_atom_literal(:bar)
tdd_atom = Tdd.type_atom()
tdd_empty_tuple = Tdd.type_empty_tuple()
tdd_any = Tdd.type_any()
tdd_none = Tdd.type_none()
test = fn name, expected, result ->
current_failures = Process.get(:test_failures, [])
if expected != result do
Process.put(:test_failures, [name | current_failures])
end
status = if expected == result, do: "PASSED", else: "FAILED"
IO.puts("#{name} (Expected: #{expected}) -> Result: #{result} - #{status}")
end
# Basic Types
tdd_foo = Tdd.type_atom_literal(:foo)
tdd_bar = Tdd.type_atom_literal(:bar)
tdd_baz = Tdd.type_atom_literal(:baz)
tdd_atom = Tdd.type_atom()
tdd_empty_tuple = Tdd.type_empty_tuple()
tdd_tuple = Tdd.type_tuple()
# Tuple of size 2, e.g. {any, any}
tdd_tuple_s2 = Tdd.type_tuple_sized_any(2)
tdd_any = Tdd.type_any()
tdd_none = Tdd.type_none()
test_all = fn ->
IO.puts("\n--- TDD for :foo ---")
Tdd.print_tdd(tdd_foo)
IO.puts("\n--- TDD for not :foo ---")
Tdd.print_tdd(Tdd.negate(tdd_foo))
IO.puts("\n--- TDD for atom ---")
Tdd.print_tdd(tdd_atom)
IO.puts("\n--- TDD for not atom ---")
# Expected: make_node(@v_is_atom, @false_node_id, @true_node_id, @true_node_id)
# This represents "anything that is not an atom". The DC branch becomes true because if
# "is_atom" test is irrelevant for "not atom", it means it's part of "not atom".
Tdd.print_tdd(Tdd.negate(tdd_atom))
IO.puts("\n--- TDD for :foo and :bar (should be none) ---")
tdd_foo_and_bar = Tdd.intersect(tdd_foo, tdd_bar)
# Expected ID 0: :false_terminal
Tdd.print_tdd(tdd_foo_and_bar)
IO.puts("\n--- TDD for :foo and atom (should be :foo) ---")
tdd_foo_and_atom = Tdd.intersect(tdd_foo, tdd_atom)
# Expected to be structurally identical to tdd_foo
Tdd.print_tdd(tdd_foo_and_atom)
IO.puts("\n--- Basic Subtyping Tests ---")
test.(":foo <: atom", true, Tdd.is_subtype(tdd_foo, tdd_atom))
test.("atom <: :foo", false, Tdd.is_subtype(tdd_atom, tdd_foo))
test.(":foo <: :bar", false, Tdd.is_subtype(tdd_foo, tdd_bar))
test.(":foo <: :foo", true, Tdd.is_subtype(tdd_foo, tdd_foo))
test.("{} <: tuple", true, Tdd.is_subtype(tdd_empty_tuple, tdd_tuple))
test.("tuple <: {}", false, Tdd.is_subtype(tdd_tuple, tdd_empty_tuple))
test.(":foo <: {}", false, Tdd.is_subtype(tdd_foo, tdd_empty_tuple))
test.("tuple_size_2 <: tuple", true, Tdd.is_subtype(tdd_tuple_s2, tdd_tuple))
test.("tuple <: tuple_size_2", false, Tdd.is_subtype(tdd_tuple, tdd_tuple_s2))
test.("tuple_size_2 <: {}", false, Tdd.is_subtype(tdd_tuple_s2, tdd_empty_tuple))
IO.puts("\n--- Any/None Subtyping Tests ---")
test.("any <: :foo", false, Tdd.is_subtype(tdd_any, tdd_foo))
test.(":foo <: any", true, Tdd.is_subtype(tdd_foo, tdd_any))
test.("none <: :foo", true, Tdd.is_subtype(tdd_none, tdd_foo))
test.(":foo <: none", false, Tdd.is_subtype(tdd_foo, tdd_none))
test.("none <: any", true, Tdd.is_subtype(tdd_none, tdd_any))
test.("any <: none", false, Tdd.is_subtype(tdd_any, tdd_none))
test.("any <: any", true, Tdd.is_subtype(tdd_any, tdd_any))
test.("none <: none", true, Tdd.is_subtype(tdd_none, tdd_none))
IO.puts("\n--- Union related Subtyping ---")
tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
tdd_foo_or_bar_or_baz = Tdd.sum(tdd_foo_or_bar, tdd_baz)
test.(":foo <: (:foo | :bar)", true, Tdd.is_subtype(tdd_foo, tdd_foo_or_bar))
test.(":baz <: (:foo | :bar)", false, Tdd.is_subtype(tdd_baz, tdd_foo_or_bar))
test.("(:foo | :bar) <: atom", true, Tdd.is_subtype(tdd_foo_or_bar, tdd_atom))
test.("atom <: (:foo | :bar)", false, Tdd.is_subtype(tdd_atom, tdd_foo_or_bar))
test.(
"(:foo | :bar) <: (:foo | :bar | :baz)",
true,
Tdd.is_subtype(tdd_foo_or_bar, tdd_foo_or_bar_or_baz)
)
test.(
"(:foo | :bar | :baz) <: (:foo | :bar)",
false,
Tdd.is_subtype(tdd_foo_or_bar_or_baz, tdd_foo_or_bar)
)
# Test against a non-member of the union
test.("(:foo | :bar) <: :baz", false, Tdd.is_subtype(tdd_foo_or_bar, tdd_baz))
IO.puts("\n--- Intersection related Subtyping ---")
# Should be equivalent to tdd_foo
tdd_atom_and_foo = Tdd.intersect(tdd_atom, tdd_foo)
# Should be tdd_none
tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)
test.("(atom & :foo) <: :foo", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_foo))
test.(":foo <: (atom & :foo)", true, Tdd.is_subtype(tdd_foo, tdd_atom_and_foo))
test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
test.("none <: (atom & tuple)", true, Tdd.is_subtype(tdd_none, tdd_atom_and_tuple))
test.("(atom & :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_and_foo, tdd_bar))
# An intersection is a subtype of its components
test.("(atom & :foo) <: atom", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_atom))
# (none <: atom)
test.("(atom & tuple) <: atom", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_atom))
# (none <: tuple)
test.("(atom & tuple) <: tuple", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_tuple))
IO.puts("\n--- Negation related Subtyping (Contrapositives) ---")
# Reminder: ¬A <: ¬B is equivalent to B <: A (contrapositive)
# Test 1: ¬atom <: ¬:foo (Equivalent to :foo <: atom, which is true)
test.("¬atom <: ¬:foo", true, Tdd.is_subtype(Tdd.negate(tdd_atom), Tdd.negate(tdd_foo)))
# Test 2: ¬:foo <: ¬atom (Equivalent to atom <: :foo, which is false)
test.("¬:foo <: ¬atom", false, Tdd.is_subtype(Tdd.negate(tdd_foo), Tdd.negate(tdd_atom)))
# Double negation
test.("¬(¬:foo) <: :foo", true, Tdd.is_subtype(Tdd.negate(Tdd.negate(tdd_foo)), tdd_foo))
test.(":foo <: ¬(¬:foo)", true, Tdd.is_subtype(tdd_foo, Tdd.negate(Tdd.negate(tdd_foo))))
# Disjoint types
test.("atom <: ¬tuple", true, Tdd.is_subtype(tdd_atom, Tdd.negate(tdd_tuple)))
test.("tuple <: ¬atom", true, Tdd.is_subtype(tdd_tuple, Tdd.negate(tdd_atom)))
test.(":foo <: ¬{}", true, Tdd.is_subtype(tdd_foo, Tdd.negate(tdd_empty_tuple)))
IO.puts("\n--- Mixed Types & Complex Subtyping ---")
tdd_atom_or_tuple = Tdd.sum(tdd_atom, tdd_tuple)
tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)
test.(
"(:foo | {}) <: (atom | tuple)",
true,
Tdd.is_subtype(tdd_foo_or_empty_tuple, tdd_atom_or_tuple)
)
test.(
"(atom | tuple) <: (:foo | {})",
false,
Tdd.is_subtype(tdd_atom_or_tuple, tdd_foo_or_empty_tuple)
)
test.(":foo <: (atom | tuple)", true, Tdd.is_subtype(tdd_foo, tdd_atom_or_tuple))
test.("{} <: (atom | tuple)", true, Tdd.is_subtype(tdd_empty_tuple, tdd_atom_or_tuple))
# De Morgan's Law illustration (A | B = ¬(¬A & ¬B))
# (:foo | :bar) <: ¬(¬:foo & ¬:bar)
tdd_not_foo_and_not_bar = Tdd.intersect(Tdd.negate(tdd_foo), Tdd.negate(tdd_bar))
test.(
"(:foo | :bar) <: ¬(¬:foo & ¬:bar)",
true,
Tdd.is_subtype(tdd_foo_or_bar, Tdd.negate(tdd_not_foo_and_not_bar))
)
test.(
"¬(¬:foo & ¬:bar) <: (:foo | :bar)",
true,
Tdd.is_subtype(Tdd.negate(tdd_not_foo_and_not_bar), tdd_foo_or_bar)
)
# Type difference: atom - :foo (represented as atom & ¬:foo)
tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom))
test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo))
# True if :bar is in (atom - :foo)
test.("(atom - :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar))
test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))
# (atom - :foo) | :foo should be atom
tdd_recombined_atom = Tdd.sum(tdd_atom_minus_foo, tdd_foo)
test.("((atom - :foo) | :foo) <: atom", true, Tdd.is_subtype(tdd_recombined_atom, tdd_atom))
test.("atom <: ((atom - :foo) | :foo)", true, Tdd.is_subtype(tdd_atom, tdd_recombined_atom))
# (atom | {}) & (tuple | :foo) must be (:foo | {})
# Represents `atom() | {}`
tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple)
# Represents `tuple() | :foo`
tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo)
intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo)
# Expected result for intersected_complex is tdd_foo_or_empty_tuple
test.(
"(atom | {}) & (tuple | :foo) <: (:foo | {})",
true,
Tdd.is_subtype(intersected_complex, tdd_foo_or_empty_tuple)
)
test.(
"(:foo | {}) <: (atom | {}) & (tuple | :foo)",
true,
Tdd.is_subtype(tdd_foo_or_empty_tuple, intersected_complex)
)
# {} | tuple_size_2 should be a subtype of tuple
tdd_empty_or_s2 = Tdd.sum(tdd_empty_tuple, tdd_tuple_s2)
test.("({} | tuple_size_2) <: tuple", true, Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple))
test.(
"({} | tuple_size_2) <: ({} | tuple_size_2)",
true,
Tdd.is_subtype(tdd_empty_or_s2, tdd_empty_or_s2)
)
test.(
"({} | tuple_size_2) <: tuple_size_2",
false,
Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2)
)
# IO.puts("\n--- TDD structure for (atom - :foo) ---")
# Tdd.print_tdd(tdd_atom_minus_foo)
# IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---")
# Tdd.print_tdd(tdd_recombined_atom)
# IO.puts("\n--- TDD structure for 'atom' for comparison ---")
# Tdd.print_tdd(tdd_atom)
IO.inspect(Process.get(:test_failures, []))
end
defmodule IntegerTests do
def run(test_fn) do
Process.put(:test_failures, [])
# Reset for each test group if needed, or once globally
Tdd.init_tdd_system()
# Integer types
tdd_int = Tdd.type_integer()
tdd_int_5 = Tdd.type_int_eq(5)
tdd_int_7 = Tdd.type_int_eq(7)
# x < 10
tdd_int_lt_10 = Tdd.type_int_lt(10)
# x > 3
tdd_int_gt_3 = Tdd.type_int_gt(3)
# x < 3
tdd_int_lt_3 = Tdd.type_int_lt(3)
# x > 10
tdd_int_gt_10 = Tdd.type_int_gt(10)
tdd_atom_foo = Tdd.type_atom_literal(:foo)
#
# IO.puts("\n--- Integer Type Structures ---")
# IO.puts("Integer:")
# Tdd.print_tdd(tdd_int)
# IO.puts("Int == 5:")
# Tdd.print_tdd(tdd_int_5)
# IO.puts("Int < 10:")
# Tdd.print_tdd(tdd_int_lt_10)
IO.puts("\n--- Integer Subtyping Tests ---")
test_fn.("int_5 <: integer", true, Tdd.is_subtype(tdd_int_5, tdd_int))
test_fn.("integer <: int_5", false, Tdd.is_subtype(tdd_int, tdd_int_5))
test_fn.("int_5 <: int_7", false, Tdd.is_subtype(tdd_int_5, tdd_int_7))
test_fn.("int_5 <: int_5", true, Tdd.is_subtype(tdd_int_5, tdd_int_5))
test_fn.("int_5 <: atom_foo", false, Tdd.is_subtype(tdd_int_5, tdd_atom_foo))
test_fn.("int_lt_10 <: integer", true, Tdd.is_subtype(tdd_int_lt_10, tdd_int))
test_fn.("integer <: int_lt_10", false, Tdd.is_subtype(tdd_int, tdd_int_lt_10))
# 5 < 10
test_fn.("int_5 <: int_lt_10", true, Tdd.is_subtype(tdd_int_5, tdd_int_lt_10))
test_fn.("int_lt_10 <: int_5", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_5))
test_fn.("int_gt_3 <: integer", true, Tdd.is_subtype(tdd_int_gt_3, tdd_int))
# 5 > 3
test_fn.("int_5 <: int_gt_3", true, Tdd.is_subtype(tdd_int_5, tdd_int_gt_3))
test_fn.("int_gt_3 <: int_5", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_5))
# x < 3 implies x < 10
test_fn.("int_lt_3 <: int_lt_10", true, Tdd.is_subtype(tdd_int_lt_3, tdd_int_lt_10))
# x > 10 implies x > 3
test_fn.("int_gt_10 <: int_gt_3", true, Tdd.is_subtype(tdd_int_gt_10, tdd_int_gt_3))
test_fn.("int_lt_10 <: int_lt_3", false, Tdd.is_subtype(tdd_int_lt_10, tdd_int_lt_3))
test_fn.("int_gt_3 <: int_gt_10", false, Tdd.is_subtype(tdd_int_gt_3, tdd_int_gt_10))
IO.puts("\n--- Integer Intersection Tests (should resolve to none for contradictions) ---")
intersect_5_7 = Tdd.intersect(tdd_int_5, tdd_int_7)
test_fn.("int_5 & int_7 == none", true, intersect_5_7 == Tdd.type_none())
# IO.puts("Structure of int_5 & int_7 (should be ID 0):")
# Tdd.print_tdd(intersect_5_7)
# x < 3 AND x > 10
intersect_lt3_gt10 = Tdd.intersect(tdd_int_lt_3, tdd_int_gt_10)
test_fn.("int_lt_3 & int_gt_10 == none", true, intersect_lt3_gt10 == Tdd.type_none())
# IO.puts("Structure of int_lt_3 & int_gt_10 (should be ID 0):")
# Tdd.print_tdd(intersect_lt3_gt10)
# x < 10 AND x > 3 (e.g. 4,5..9)
intersect_lt10_gt3 = Tdd.intersect(tdd_int_lt_10, tdd_int_gt_3)
test_fn.("int_lt_10 & int_gt_3 != none", true, intersect_lt10_gt3 != Tdd.type_none())
# IO.puts("Structure of int_lt_10 & int_gt_3 (should be non-empty):")
# Tdd.print_tdd(intersect_lt10_gt3)
# Test a value within this intersection
test_fn.(
"int_5 <: (int_lt_10 & int_gt_3)",
true,
Tdd.is_subtype(tdd_int_5, intersect_lt10_gt3)
)
# x == 5 AND x < 3
intersect_5_lt3 = Tdd.intersect(tdd_int_5, tdd_int_lt_3)
test_fn.("int_5 & int_lt_3 == none", true, intersect_5_lt3 == Tdd.type_none())
IO.puts("\n--- Integer Union Tests ---")
union_5_7 = Tdd.sum(tdd_int_5, tdd_int_7)
test_fn.("int_5 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_5, union_5_7))
test_fn.("int_7 <: (int_5 | int_7)", true, Tdd.is_subtype(tdd_int_7, union_5_7))
test_fn.("int_lt_3 <: (int_5 | int_7)", false, Tdd.is_subtype(tdd_int_lt_3, union_5_7))
# IO.puts("Structure of int_5 | int_7:")
# Tdd.print_tdd(union_5_7)
# (int < 3) | (int > 10)
union_disjoint_ranges = Tdd.sum(tdd_int_lt_3, tdd_int_gt_10)
test_fn.(
"int_eq(0) <: (int < 3 | int > 10)",
true,
Tdd.is_subtype(Tdd.type_int_eq(0), union_disjoint_ranges)
)
test_fn.(
"int_eq(5) <: (int < 3 | int > 10)",
false,
Tdd.is_subtype(Tdd.type_int_eq(5), union_disjoint_ranges)
)
test_fn.(
"int_eq(12) <: (int < 3 | int > 10)",
true,
Tdd.is_subtype(Tdd.type_int_eq(12), union_disjoint_ranges)
)
IO.inspect(Process.get(:test_failures, []))
end
end
defmodule TupleTests do
import Tdd
def run(test_fn) do
Process.put(:test_failures, [])
# Re-init the system for a clean slate for these tests
Tdd.init_tdd_system()
IO.puts("\n--- Running TupleTests ---")
# --- Basic Types for convenience ---
t_atom = type_atom()
t_int = type_integer()
t_foo = type_atom_literal(:foo)
t_bar = type_atom_literal(:bar)
t_int_5 = type_int_eq(5)
t_int_6 = type_int_eq(6)
t_int_pos = type_int_gt(0)
t_any = type_any()
t_none = type_none()
# any tuple
t_tuple = type_tuple()
t_empty_tuple = type_empty_tuple()
# --- Specific Tuple Types ---
# {atom(), integer()}
tup_atom_int = type_tuple([t_atom, t_int])
# {:foo, 5}
tup_foo_5 = type_tuple([t_foo, t_int_5])
# {pos_integer(), atom()}
tup_pos_atom = type_tuple([t_int_pos, t_atom])
# {atom(), any}
tup_atom_any = type_tuple([t_atom, t_any])
# {any, integer()}
tup_any_int = type_tuple([t_any, t_int])
# a tuple of size 2, {any, any}
tup_s2_any = type_tuple_sized_any(2)
# a tuple of size 3, {any, any, any}
tup_s3_any = type_tuple_sized_any(3)
# {integer(), atom()}
tup_int_atom = type_tuple([t_int, t_atom])
# {{:foo}}
tup_nested_foo = type_tuple([type_tuple([t_foo])])
# {{atom()}}
tup_nested_atom = type_tuple([type_tuple([t_atom])])
# {any, none} -> this should resolve to none
tup_with_none = type_tuple([t_any, t_none])
IO.puts("\n--- Section: Basic Subtyping ---")
test_fn.("{:foo, 5} <: {atom, int}", true, is_subtype(tup_foo_5, tup_atom_int))
test_fn.("{atom, int} <: {:foo, 5}", false, is_subtype(tup_atom_int, tup_foo_5))
test_fn.("{:foo, 5} <: {pos_int, atom}", false, is_subtype(tup_foo_5, tup_pos_atom))
test_fn.("{pos_int, atom} <: {atom, int}", false, is_subtype(tup_pos_atom, tup_atom_int))
test_fn.("{atom, int} <: tuple()", true, is_subtype(tup_atom_int, t_tuple))
test_fn.("tuple() <: {atom, int}", false, is_subtype(t_tuple, tup_atom_int))
IO.puts("\n--- Section: Size-related Subtyping ---")
test_fn.("{atom, int} <: tuple_size_2_any", true, is_subtype(tup_atom_int, tup_s2_any))
test_fn.("tuple_size_2_any <: {atom, int}", false, is_subtype(tup_s2_any, tup_atom_int))
test_fn.("{atom, int} <: tuple_size_3_any", false, is_subtype(tup_atom_int, tup_s3_any))
test_fn.("tuple_size_2_any <: tuple_size_3_any", false, is_subtype(tup_s2_any, tup_s3_any))
test_fn.("{} <: tuple()", true, is_subtype(t_empty_tuple, t_tuple))
test_fn.("{} <: tuple_size_2_any", false, is_subtype(t_empty_tuple, tup_s2_any))
IO.puts("\n--- Section: Intersection ---")
# {atom, any} & {any, int} -> {atom, int}
intersect1 = intersect(tup_atom_any, tup_any_int)
test_fn.("({atom,any} & {any,int}) == {atom,int}", true, intersect1 == tup_atom_int)
# {atom, int} & {int, atom} -> none
intersect2 = intersect(tup_atom_int, tup_int_atom)
test_fn.("({atom,int} & {int,atom}) == none", true, intersect2 == t_none)
# tuple_size_2 & tuple_size_3 -> none
intersect3 = intersect(tup_s2_any, tup_s3_any)
test_fn.("(tuple_size_2 & tuple_size_3) == none", true, intersect3 == t_none)
# tuple() & {atom, int} -> {atom, int}
intersect4 = intersect(t_tuple, tup_atom_int)
test_fn.("(tuple() & {atom,int}) == {atom,int}", true, intersect4 == tup_atom_int)
IO.puts("\n--- Section: Union ---")
# {:foo, 5} | {pos_int, atom}
union1 = sum(tup_foo_5, tup_pos_atom)
test_fn.("{:foo, 5} <: ({:foo, 5} | {pos_int, atom})", true, is_subtype(tup_foo_5, union1))
test_fn.(
"{pos_int, atom} <: ({:foo, 5} | {pos_int, atom})",
true,
is_subtype(tup_pos_atom, union1)
)
test_fn.(
"{atom, int} <: ({:foo, 5} | {pos_int, atom})",
false,
is_subtype(tup_atom_int, union1)
)
# {atom, any} | {any, int} -> a complex type, let's check subtyping against it
union2 = sum(tup_atom_any, tup_any_int)
# {atom, int} is in both parts of the union.
test_fn.("{atom, int} <: ({atom,any} | {any,int})", true, is_subtype(tup_atom_int, union2))
# {:foo, :bar} is only in {atom, any}.
test_fn.(
"{:foo, :bar} <: ({atom,any} | {any,int})",
true,
is_subtype(type_tuple([t_foo, t_bar]), union2)
)
# {5, 6} is only in {any, int}.
test_fn.(
"{5, 6} <: ({atom,any} | {any,int})",
true,
is_subtype(type_tuple([t_int_5, t_int_6]), union2)
)
# {5, :foo} is in neither part of the union.
test_fn.(
"{5, :foo} <: ({atom,any} | {any,int})",
false,
is_subtype(type_tuple([t_int_5, t_foo]), union2)
)
IO.puts("\n--- Section: Negation and Type Difference ---")
# atom is disjoint from tuple, so atom <: ¬tuple
test_fn.("atom <: ¬tuple", true, is_subtype(t_atom, negate(t_tuple)))
# A specific tuple should not be a subtype of the negation of a more general tuple type it belongs to
test_fn.("{atom, int} <: ¬tuple()", false, is_subtype(tup_atom_int, negate(t_tuple)))
# {int, atom} is a subtype of ¬{atom, int} because their elements differ
test_fn.("{int, atom} <: ¬{atom, int}", true, is_subtype(tup_int_atom, negate(tup_atom_int)))
# tuple_size_3 is a subtype of ¬tuple_size_2 because their sizes differ
test_fn.("tuple_size_3 <: ¬tuple_size_2", true, is_subtype(tup_s3_any, negate(tup_s2_any)))
# Type difference: tuple_size_2 - {atom, any} -> should be {¬atom, any} for size 2 tuples.
diff1 = intersect(tup_s2_any, negate(tup_atom_any))
# {integer, integer} has a first element that is not an atom, so it should be in the difference.
tup_int_int = type_tuple([t_int, t_int])
test_fn.("{int, int} <: (tuple_size_2 - {atom, any})", true, is_subtype(tup_int_int, diff1))
test_fn.(
"{atom, int} <: (tuple_size_2 - {atom, any})",
false,
is_subtype(tup_atom_int, diff1)
)
IO.puts("\n--- Section: Nested Tuples ---")
test_fn.("{{:foo}} <: {{atom}}", true, is_subtype(tup_nested_foo, tup_nested_atom))
test_fn.("{{atom}} <: {{:foo}}", false, is_subtype(tup_nested_atom, tup_nested_foo))
# Intersection of disjoint nested types: {{:foo}} & {{:bar}}
intersect_nested = intersect(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
test_fn.("{{:foo}} & {{:bar}} == none", true, intersect_nested == t_none)
# Union of nested types
union_nested = sum(tup_nested_foo, type_tuple([type_tuple([t_bar])]))
test_fn.("{{:foo}} <: ({{:foo}} | {{:bar}})", true, is_subtype(tup_nested_foo, union_nested))
test_fn.(
"{{:bar}} <: ({{:foo}} | {{:bar}})",
true,
is_subtype(type_tuple([type_tuple([t_bar])]), union_nested)
)
test_fn.(
"{{atom}} <: ({{:foo}} | {{:bar}})",
false,
is_subtype(tup_nested_atom, union_nested)
)
IO.puts("\n--- Section: Edge Cases (any, none) ---")
# A type `{any, none}` should not be possible. The value `none` cannot exist.
# The simplification logic should reduce this to `type_none`.
test_fn.("{any, none} == none", true, tup_with_none == t_none)
# Intersection with a tuple containing none should result in none
intersect_with_none_tuple = intersect(tup_atom_int, tup_with_none)
test_fn.("{atom,int} & {any,none} == none", true, intersect_with_none_tuple == t_none)
# Union with a tuple containing none should be a no-op
union_with_none_tuple = sum(tup_atom_int, tup_with_none)
test_fn.("{atom,int} | {any,none} == {atom,int}", true, union_with_none_tuple == tup_atom_int)
# --- Original tests from problem description for regression ---
IO.puts("\n--- Specific Tuple Subtyping Test (Original) ---")
test_fn.(
"{1, :foo} <: {int_gt_0, :foo | :bar}",
true,
is_subtype(
type_tuple([type_int_eq(1), type_atom_literal(:foo)]),
type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
)
)
test_fn.(
"{0, :foo} <: {int_gt_0, :foo | :bar}",
false,
is_subtype(
type_tuple([type_int_eq(0), type_atom_literal(:foo)]),
type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
)
)
test_fn.(
"{1, :kek} <: {int_gt_0, :foo | :bar}",
false,
is_subtype(
type_tuple([
type_int_eq(1),
type_atom_literal(:kek)
]),
type_tuple([type_int_gt(0), sum(type_atom_literal(:foo), type_atom_literal(:bar))])
)
)
IO.inspect(Process.get(:test_failures, []), label: "TupleTests failures")
end
end
defmodule ListTests do
import Tdd
def run(test_fn) do
Process.put(:test_failures, [])
Tdd.init_tdd_system()
IO.puts("\n--- Running ListTests ---")
# --- Basic Types ---
t_atom = type_atom()
t_int = type_integer()
t_foo = type_atom_literal(:foo)
t_bar = type_atom_literal(:bar)
t_any = type_any()
t_none = type_none()
# --- List Types ---
t_list = type_list()
t_empty_list = type_empty_list()
# [atom | list]
t_cons_atom_list = type_cons(t_atom, t_list)
# [:foo | []]
t_cons_foo_empty = type_cons(t_foo, t_empty_list)
# [atom | []]
t_cons_atom_empty = type_cons(t_atom, t_empty_list)
# [any | []]
t_cons_any_empty = type_cons(t_any, t_empty_list)
# [integer | list]
t_cons_int_list = type_cons(t_int, t_list)
IO.puts("\n--- Section: Basic List Subtyping ---")
test_fn.("[] <: list", true, is_subtype(t_empty_list, t_list))
test_fn.("list <: []", false, is_subtype(t_list, t_empty_list))
test_fn.("[atom|list] <: list", true, is_subtype(t_cons_atom_list, t_list))
test_fn.("list <: [atom|list]", false, is_subtype(t_list, t_cons_atom_list))
test_fn.("[] <: [atom|list]", false, is_subtype(t_empty_list, t_cons_atom_list))
test_fn.("[atom|list] <: []", false, is_subtype(t_cons_atom_list, t_empty_list))
test_fn.("list <: atom", false, is_subtype(t_list, t_atom))
test_fn.("atom <: list", false, is_subtype(t_atom, t_list))
IO.puts("\n--- Section: Cons Subtyping (Covariance) ---")
# Head is a subtype
test_fn.("[:foo|[]] <: [atom|[]]", true, is_subtype(t_cons_foo_empty, t_cons_atom_empty))
test_fn.("[atom|[]] <: [:foo|[]]", false, is_subtype(t_cons_atom_empty, t_cons_foo_empty))
# Tail is a subtype
test_fn.("[atom|[]] <: [atom|list]", true, is_subtype(t_cons_atom_empty, t_cons_atom_list))
test_fn.("[atom|list] <: [atom|[]]", false, is_subtype(t_cons_atom_list, t_cons_atom_empty))
# Both are subtypes
test_fn.("[:foo|[]] <: [atom|list]", true, is_subtype(t_cons_foo_empty, t_cons_atom_list))
# Neither is a subtype
test_fn.("[atom|list] <: [:foo|[]]", false, is_subtype(t_cons_atom_list, t_cons_foo_empty))
# A list of length 1 is a subtype of a list of any element of length 1
test_fn.("[atom|[]] <: [any|[]]", true, is_subtype(t_cons_atom_empty, t_cons_any_empty))
IO.puts("\n--- Section: List Intersection ---")
# [atom|list] & [integer|list] -> should be none due to head conflict
intersect1 = intersect(t_cons_atom_list, t_cons_int_list)
test_fn.("[atom|list] & [integer|list] == none", true, intersect1 == t_none)
# [any|[]] & [atom|list] -> should be [atom|[]]
intersect2 = intersect(t_cons_any_empty, t_cons_atom_list)
test_fn.("([any|[]] & [atom|list]) == [atom|[]]", true, intersect2 == t_cons_atom_empty)
# [] & [atom|list] -> should be none because one is empty and one is not
intersect3 = intersect(t_empty_list, t_cons_atom_list)
test_fn.("[] & [atom|list] == none", true, intersect3 == t_none)
IO.puts("\n--- Section: List Union ---")
# [] | [atom|[]]
union1 = sum(t_empty_list, t_cons_atom_empty)
test_fn.("[] <: ([] | [atom|[]])", true, is_subtype(t_empty_list, union1))
test_fn.("[atom|[]] <: ([] | [atom|[]])", true, is_subtype(t_cons_atom_empty, union1))
test_fn.(
"[integer|[]] <: ([] | [atom|[]])",
false,
is_subtype(type_cons(t_int, t_empty_list), union1)
)
# [:foo|[]] | [:bar|[]]
union2 = sum(t_cons_foo_empty, type_cons(t_bar, t_empty_list))
# This union is a subtype of [atom|[]]
test_fn.("([:foo|[]] | [:bar|[]]) <: [atom|[]]", true, is_subtype(union2, t_cons_atom_empty))
test_fn.("[atom|[]] <: ([:foo|[]] | [:bar|[]])", false, is_subtype(t_cons_atom_empty, union2))
IO.puts("\n--- Section: List Negation ---")
# list is a subtype of not(atom)
test_fn.("list <: ¬atom", true, is_subtype(t_list, negate(t_atom)))
# A non-empty list is a subtype of not an empty list
test_fn.("[atom|list] <: ¬[]", true, is_subtype(t_cons_atom_list, negate(t_empty_list)))
# [integer|list] is a subtype of not [atom|list]
test_fn.(
"[integer|list] <: ¬[atom|list]",
true,
is_subtype(t_cons_int_list, negate(t_cons_atom_list))
)
IO.inspect(Process.get(:test_failures, []), label: "ListTests failures")
end
end
defmodule ListOfTests do
import Tdd
def run(test_fn) do
Process.put(:test_failures, [])
Tdd.init_tdd_system()
IO.puts("\n--- Running ListOfTests ---")
# --- Basic Types ---
t_atom = type_atom()
t_int = type_integer()
t_pos_int = type_int_gt(0)
t_int_5 = type_int_eq(5)
# --- list(X) Types ---
t_list_of_int = type_list_of(t_int)
t_list_of_pos_int = type_list_of(t_pos_int)
t_list_of_atom = type_list_of(t_atom)
# --- Specific List Types ---
t_list = type_list()
t_empty_list = type_empty_list()
# [5]
t_list_one_int = type_cons(t_int_5, t_empty_list)
# [:foo]
t_list_one_atom = type_cons(type_atom_literal(:foo), t_empty_list)
# [5, :foo]
t_list_int_and_atom = type_cons(t_int_5, type_cons(type_atom_literal(:foo), t_empty_list))
IO.puts("\n--- Section: Basic list(X) Subtyping ---")
test_fn.("list(integer) <: list()", true, is_subtype(t_list_of_int, t_list))
test_fn.("list() <: list(integer)", false, is_subtype(t_list, t_list_of_int))
test_fn.("[] <: list(integer)", true, is_subtype(t_empty_list, t_list_of_int))
test_fn.("[5] <: list(integer)", true, is_subtype(t_list_one_int, t_list_of_int))
test_fn.("[:foo] <: list(integer)", false, is_subtype(t_list_one_atom, t_list_of_int))
test_fn.("[5, :foo] <: list(integer)", false, is_subtype(t_list_int_and_atom, t_list_of_int))
test_fn.(
"[5, :foo] <: list(any)",
true,
is_subtype(t_list_int_and_atom, type_list_of(type_any()))
)
IO.puts("\n--- Section: Covariance of list(X) ---")
test_fn.(
"list(pos_integer) <: list(integer)",
true,
is_subtype(t_list_of_pos_int, t_list_of_int)
)
test_fn.(
"list(integer) <: list(pos_integer)",
false,
is_subtype(t_list_of_int, t_list_of_pos_int)
)
IO.puts("\n--- Section: Intersection of list(X) ---")
# list(integer) & list(pos_integer) should be list(pos_integer)
intersect1 = intersect(t_list_of_int, t_list_of_pos_int)
test_fn.(
"(list(int) & list(pos_int)) == list(pos_int)",
true,
intersect1 == t_list_of_pos_int
)
# list(integer) & list(atom) should be just [] (empty list is the only common member)
# The system simplifies this intersection to a type that only accepts the empty list.
intersect2 = intersect(t_list_of_int, t_list_of_atom)
test_fn.("[] <: (list(int) & list(atom))", true, is_subtype(t_empty_list, intersect2))
test_fn.("[5] <: (list(int) & list(atom))", false, is_subtype(t_list_one_int, intersect2))
test_fn.("[:foo] <: (list(int) & list(atom))", false, is_subtype(t_list_one_atom, intersect2))
# It should be equivalent to `type_empty_list`
test_fn.("(list(int) & list(atom)) == []", true, intersect2 == t_empty_list)
IO.puts("\n--- Section: Intersection of list(X) with cons ---")
# list(integer) & [:foo | []] -> should be none
intersect3 = intersect(t_list_of_int, t_list_one_atom)
test_fn.("list(integer) & [:foo] == none", true, intersect3 == type_none())
# list(integer) & [5 | []] -> should be [5 | []]
intersect4 = intersect(t_list_of_int, t_list_one_int)
test_fn.("list(integer) & [5] == [5]", true, intersect4 == t_list_one_int)
# list(integer) & [5, :foo] -> should be none
intersect5 = intersect(t_list_of_int, t_list_int_and_atom)
test_fn.("list(integer) & [5, :foo] == none", true, intersect5 == type_none())
IO.inspect(Process.get(:test_failures, []), label: "ListOfTests failures")
end
end
defmodule AdhocTest do
import Tdd
def run(test_fn) do
# --- Basic Types ---
t_int = type_integer()
t_pos_int = type_int_gt(0)
# --- list(X) Types ---
t_list_of_int = type_list_of(t_int)
t_list_of_pos_int = type_list_of(t_pos_int)
print_tdd(t_list_of_int)
print_tdd(t_list_of_pos_int )
# --- Specific List Types ---
intersect1 = intersect(t_list_of_int, t_list_of_pos_int)
print_tdd(intersect1)
print_tdd(14)
print_tdd(16)
test_fn.(
"(list(int) & list(pos_int)) == list(pos_int)",
true,
intersect1 == t_list_of_pos_int
)
end
end
# test_all.()
# IntegerTests.run(test)
# TupleTests.run(test)
# ListTests.run(test)
# ListOfTests.run(test)
AdhocTest.run(test)
==============================================================================
==============================================================================
==============================================================================
==============================================================================
==============================================================================
==============================================================================
==============================================================================
Excellent and very thorough submission. This is a professional-grade implementation of a complex concept, and the design document is clear and well-structured. The core idea of separating the structural engine (Tdd.Core) from the semantic layer (Tdd and Tdd.PredicateLogic) is exactly the right approach.
Let's break down the review into the parts you asked for: why the test fails, implementation shortcomings, and fundamental design flaws.
1. Why the Test Fails: The Root Cause
The failing test is (list(int) & list(pos_int)) == list(pos_int) in ListOfTests (and AdhocTest).
This test fails because of a fundamental design flaw in how list_of(T) types are represented and handled by the intersection logic.
The Problem:
- Representation: You've chosen to represent the
list_of(T)constraint with a special variable:{5, :all_elements, element_type_id}. The crucial part is that theelement_type_id(an integer) is part of the variable itself. - Distinct Variables: This means the variable for
list(integer)is{5, :all_elements, <id_for_integer>}and the variable forlist(positive_integer)is{5, :all_elements, <id_for_positive_integer>}. Because the type IDs are different, the TDD system sees these as two completely separate, unrelated predicates. - Structural Intersection: The
intersectoperation is structural. When it intersectslist(int)andlist(pos_int), it sees two different predicate nodes. It correctly follows the Shannon expansion and creates a new TDD that essentially says: "the type must be a list ANDall_elementsmust beintegerANDall_elementsmust bepositive_integer". - Lack of Semantic Simplification: The resulting TDD has two test nodes (
{5, :all_elements, ...}) on its main path. Thelist(pos_int)TDD only has one. Although they are logically equivalent (sincepos_int <: int), they are not structurally identical. Your system currently has no semantic rule inPredicateLogicorsimplifyto perform this reduction:({5, :all_elements, T1}, true)and({5, :all_elements, T2}, true)should simplify to({5, :all_elements, intersect(T1, T2)}, true).
Because the system cannot perform this semantic simplification, the resulting TDD from the intersection is not canonical, and the == check against the canonical list(pos_int) TDD fails.
2. Analysis of the Design and Implementation
This single failing test reveals a deeper pattern of challenges with this design. Let's analyze the broader shortcomings and flaws.
Flaw 1: "Macro" Predicates with Embedded IDs (The Root Cause Generalized)
This is the most critical design flaw. You use predicates that embed a TDD id inside the variable tuple itself. This appears in:
{5, :all_elements, element_type_id}{4, :element, Index, NESTED_PREDICATE_ID}{5, :head, NESTED_PREDICATE_ID}{5, :tail, NESTED_PREDICATE_ID}
This approach has several severe problems:
- Breaks Canonicity: The global ordering of variables is the bedrock of a canonical TDD/BDD. Since
ids are generated sequentially, the variable order now depends on the creation order of types. If you createlist(pos_int)beforelist(int)in one test run, and in a different order in another, the TDD variables will have a different sort order, potentially leading to different (but logically equivalent) TDD structures. This completely undermines the goal of having a single canonical form. - Semantic Blindness: As seen in the failing test, the core
applyandsimplifylogic cannot reason about the relationship between two such variables. It can't know thatis_subtype(id1, id2)implies a relationship. - Combinatorial Explosion of Variables: You are creating a new variable in the global order for every single
list_of(T)type. This leads to an unnecessarily large and sparse variable set.
Solution / Better Design: A more robust design avoids embedding IDs in variables. A predicate should represent a property of the value being tested, not a property of another TDD.
-
For Tuples/Lists: Instead of
v_list_head_pred({0, :is_atom}), the variable should just be{5, :head}. The children of this node would then be TDDs that operate on the head element itself. This is a concept known as "Functional BDDs" or using context-shifting operators. It's much more complex to implement. -
A Pragmatic Fix (within your current architecture): You must significantly enhance
PredicateLogic.check_implicationandTdd.simplifyto be aware of these macro predicates. For example,simplifywould need a rule that says: "If my constraints already include{{5, :all_elements, T1}, true}and I encounter a node for{{5, :all_elements, T2}, ...}, I must check the relationship betweenT1andT2."# In Tdd.simplify, when examining a node with var = {5, :all_elements, T2} # find any existing all_elements constraints existing_constraint = Enum.find(constraints, &match?({{5, :all_elements, _}, true}, &1)) if existing_constraint do {{5, :all_elements, t1_id}, true} = existing_constraint intersection_type = intersect(t1_id, t2) if intersection_type == type_none() do # Contradiction: this path is impossible. Simplify the 'no' branch. return simplify(n, constraints) end endThis is complex, requires careful management of the constraint set, and is a patch on the fundamental design issue, but it would fix the immediate problem.
Flaw 2: Incomplete Simplification Logic
The simplify function is the heart of semantic reduction, but it's missing key logic.
-
list_ofvscons: The interaction logic you added forlist_of(T)with:headand:tailis a great start. It correctly identifies contradictions (e.g.,list(integer) & [:foo | _] == none). However, it doesn't handle the non-contradictory case correctly.- The Bug: When checking
list(integer) & [5 | list(atom)], your current logic would find no contradiction in the head (5is an integer). It would then check the tail,list(atom), against theall_elementsconstraintlist(integer). Your code doesintersect(tail_type, required_tail_type)which isintersect(list(atom), list(integer)). This correctly results intype_empty_list. However, this should result in a contradiction for any non-empty tail, but your code only prunes the branch if the intersection is exactlytype_none().type_empty_list()is nottype_none(). This interaction is very subtle and needs to be more robust.
- The Bug: When checking
-
Integer Range Logic:
PredicateLogic.check_integer_rangesandcalculate_integer_intervalare well-implemented and correctly find contradictions within a set of assumptions. However,check_implicationfor integers is incomplete. It correctly checks if a predicate is implied (true) or contradicted (false), but it doesn't handle overlapping ranges correctly during intersection. For example,intersect(lt(10), lt(5))should simplify tolt(5). Your currentintersectwill create a TDD with two nodes (<10and<5), becausecheck_implicationreports:unknownfor<5given<10.
Shortcoming 3: Over-reliance on Memoization with Complex Keys
Your memoization keys often include a sorted list of the entire constraints map:
cache_key = {:simplify, id, Map.to_list(constraints) |> Enum.sort()}
This is correct for ensuring correctness, but it can be inefficient. As the path in the TDD gets deeper, the constraints map grows, making cache keys large and cache hits less likely than they could be. More advanced systems often find ways to canonicalize the constraint set itself or use structural hashing on the fly. For your scale, this is acceptable, but it's a potential performance bottleneck.
3. Summary of Recommendations
-
Fix the Failing Test (and the Core Flaw):
- The Best Long-Term Fix: Redesign your variables to remove embedded TDD IDs. This is a major undertaking.
- The Pragmatic Short-Term Fix: Enhance
Tdd.simplifyand/orTdd.PredicateLogic.saturateto handle the interaction between multiple "macro" predicates. The logic should be:- When multiple
{{5, :all_elements, T_i}, true}constraints exist, compute the intersection of allT_i. Replace the multiple constraints with a single one for the new intersection type. If the intersection isnone, the path is a contradiction. - Apply the same logic for tuple elements.
- When multiple
-
Improve Integer Logic: In
PredicateLogic._integer_implication, when you have a constraint like{min: nil, max: 9}(fromlt(10)) and you are checking the implication oflt(5), you can see thatlt(5)is not fully implied but also not contradicted. To simplifylt(10) & lt(5), theintersectlogic needs to recognize that the result is simplylt(5). This requires more powerful reasoning than just checking for:contradiction. Thesaturatefunction is the right place for this: it should refine the bounds in the constraint set. -
Refine
dc(Don't Care) Semantics: The design doc mentions thedcbranch, and the code includes it, but its semantic meaning isn't fully leveraged. In many TDD papers,negate({v,y,n,d})is defined as{v, negate(y), negate(n), negate(d)}. Yournegate_recursiveimplementation correctly does this. The key is to ensure the base types are constructed correctly. Fortype_atom(), you have{v_is_atom, any, none, none}. Negating this gives{v_is_atom, none, any, any}, which is correct for¬atom. This part of your implementation seems sound.
Conclusion
You have built a powerful and well-architected system that is very close to working correctly. The core issue is a design choice about how to represent recursive/nested types that, while seemingly intuitive, breaks the assumptions that the canonical apply algorithm relies on.
By focusing on adding the missing semantic rules to your PredicateLogic and simplify functions to handle these "macro" predicates, you can fix the failing tests and make the system significantly more robust without having to re-architect the entire variable scheme. This is an excellent foundation to build upon.
==============================================================================
==============================================================================
==============================================================================
Lets design how a migration to a redesigned TDD with no type ids in variables would look like, what would it entail and if/how it would simplify implementation.
==============================================================================
==============================================================================
Of course. This is an excellent question because it gets to the heart of the system's design. Migrating away from variables-with-IDs is a significant but highly beneficial architectural change.
Here is a detailed design for that migration, outlining what it would entail and how it dramatically simplifies the implementation.
The New Design Philosophy: "Contextualized Predicates"
The core problem with the old design is that a variable like {5, :head, <id_of_atom_type>} conflates two separate concepts:
- The Context: "We are now testing the head of a list."
- The Predicate: "Is this value an atom?"
The new design separates these. The TDD for a component (like a tuple element or a list head) will be built using the same fundamental set of variables as a top-level type, but those variables will be systematically namespaced or prefixed to indicate their context.
1. The New Variable Structure
Variables will be tuples that naturally sort into the correct global order. The context becomes a prefix to the base predicate.
-
Base Predicates (as before):
{0, :is_atom}{2, :beq, 5}{4, :size, 2}
-
New Contextualized Predicates:
{:element, 0, {0, :is_atom}}- "Is the 0th element of the tuple an atom?"{:element, 1, {2, :beq, 5}}- "Is the 1st element of the tuple equal to 5?"{:head, {0, :is_atom}}- "Is the head of the list an atom?"{:tail, {0, :is_list}}- "Is the tail of the list a list?" (Note: the predicate here is{0, :is_list}, not{5, ...})
This structure has a critical advantage: Elixir's default tuple sorting creates a stable, predictable, and canonical global variable order.
{:element, 0, ...}variables will always come before{:element, 1, ...}.{:element, ...}variables can be ordered before or after{:head, ...}based on the atom sorting.- Most importantly, the variable no longer depends on a runtime-generated ID.
2. The New Design for Recursive Types (list_of(T))
The "prefixing" strategy above works perfectly for fixed-size structures like tuples. For recursive types like list_of(T), which have unbounded depth, prefixing every possible element ({:head, ...}, {:tail, {:head, ...}}, etc.) would create an infinite TDD.
This requires a different, more powerful representation. Instead of embedding a type ID, we make the child of the node be the type TDD.
-
New "Applicator" Variable: We introduce a new kind of variable that acts as an instruction.
{5, :for_all_elements}
-
New Node Interpretation in
Tdd.Core: A node with this variable is interpreted differently.{var, yes_id, no_id, dc_id}- If
var == {5, :for_all_elements}, thenyes_idis the TDD ID of the type that all elements must conform to. Thenoanddcbranches are not used for this special node type and could betype_anyortype_none.
-
How
intersectWorks: This is the magic.- Let
L1 = type_list_of(T1)andL2 = type_list_of(T2). - Their TDDs will look like:
L1_tdd:is_list? -> yes -> { {5, :for_all_elements}, T1_id, any, any }L2_tdd:is_list? -> yes -> { {5, :for_all_elements}, T2_id, any, any }
- When the
applyalgorithm inTdd.Coregets to these nodes, it sees they share the exact same variable{5, :for_all_elements}. - It will then recursively call
applyon their children:intersect(T1_id, T2_id). - The result is a new node
{ {5, :for_all_elements}, intersect(T1, T2), any, any }.
- Let
This is exactly the behavior needed to solve the failing test: intersect(list(int), list(pos_int)) will correctly and structurally produce list(intersect(int, pos_int)), which is list(pos_int).
Migration Plan: What it Entails
Step 1: Redefine Variable Generation
The function map_tdd_to_component is the central place to change.
Old Code:
# wrapper_fun was &V.v_list_head_pred/1, which returned {5, :head, var}
component_var = wrapper_fun.(var)
New Code:
defp map_tdd_to_component(tdd_id, context_prefix, success_id) do
# ...
# e.g., context_prefix = :head
component_var = {context_prefix, var} # or {:element, index, var}
# ...
end
The type constructors (type_tuple, type_cons) will now pass atom contexts like :head, :tail, or {:element, index} to map_tdd_to_component.
Step 2: Rewrite Tdd.PredicateLogic for Simplicity
This is where the biggest simplification occurs. The logic no longer needs to know about specific predicate categories (5 for lists, 4 for tuples). It can be written recursively.
Old saturate logic:
- Had to check for
{{0, :is_atom}, true}and{{0, :is_tuple}, true}. - Had to check for
{{1, :value, A}, true}and{{1, :value, B}, true}. - All checks were on a flat map of constraints.
New saturate logic:
def saturate(constraints) do
# 1. Group constraints by their context prefix.
# The key `_` (or `nil`) holds the top-level constraints.
grouped_by_context =
Enum.group_by(constraints, fn
{{context, _inner_var}, _val} when is_atom(context) -> context
{{context, _index, _inner_var}, _val} when context == :element -> {context, _index}
_ -> :top_level
end)
# 2. Check for contradictions at the top level first.
case check_flat_consistency(grouped_by_context[:top_level] || []) do
:contradiction -> :contradiction
{:ok, saturated_top_level} ->
# 3. Recursively check consistency for each sub-context.
# This re-uses the exact same logic!
Enum.reduce_while(grouped_by_context, {:ok, saturated_top_level}, fn
(:top_level, _), acc -> {:cont, acc} # Already handled
({_context, sub_constraints}), acc ->
case saturate(sub_constraints) do # Recursive call!
:contradiction -> {:halt, :contradiction}
{:ok, _} -> {:cont, acc}
end
end)
end
end
# check_flat_consistency is what your old `saturate` did, but it's
# now a simpler helper that only works on a flat list of simple predicates.
The check_implication function benefits from the same recursive structure. The code becomes shorter, more general, and vastly easier to reason about and extend.
Step 3: Update Type Constructors
type_tuple(element_types)now usesmap_tdd_to_componentwith prefixes like{:element, 0},{:element, 1}, etc.type_cons(head_type, tail_type)now usesmap_tdd_to_componentwith prefixes:headand:tail.type_list_of(element_type)is completely rewritten to use the new "applicator" node design.
# New list_of constructor
def type_list_of(element_type_id) do
# A list where all elements have this type is the union of
# the empty list and a list that satisfies the property.
applicator_node = Core.make_node({5, :for_all_elements}, element_type_id, type_any(), type_any())
prop_list = intersect(type_list(), applicator_node)
# The actual type is "it's empty OR it's a non-empty list with this property"
# This part is subtle. For intersection, the simple `applicator_node` is sufficient.
# A full representation would be `sum(type_empty_list(), intersect(non_empty_list, applicator_node))`
# For now, let's focus on the intersection-friendly form.
intersect(type_list(), applicator_node)
end
Step 4: Update simplify
The simplify function also becomes more elegant. When it encounters a contextualized variable like v = {:head, inner_var}, it can simplify the children by passing the inner_var constraint down into a sub-context, which PredicateLogic now understands natively.
How the Implementation is Simplified
-
Canonicity Guaranteed: The primary goal is achieved. TDDs will have a single, canonical representation because the variable order is now stable and independent of creation order.
Tdd.intersect(A, B) == Tdd.intersect(B, A)becomes trivial. -
Drastic Simplification of
PredicateLogic:- No More Magic Numbers: The logic no longer has hardcoded knowledge of category numbers (
0,1,4,5). - Logic Reuse: The same consistency-checking logic is applied at the top level and recursively to every component (
head,tail,element[i]). This eliminates huge amounts of redundant, error-prone code. - Extensibility: Adding a new kind of container or context (e.g., map keys/values) becomes a matter of defining a new context prefix, not rewriting the core reasoning engine.
- No More Magic Numbers: The logic no longer has hardcoded knowledge of category numbers (
-
Correctness of Operations: The
intersect(list(int), list(pos_int))problem is solved structurally and elegantly by the new "applicator" node design, without requiring complex, special-cased semantic rules insimplify. The genericapplyalgorithm handles it automatically. -
Improved Debugging: A variable like
{:element, 1, {2, :lt, 10}}is far more self-describing and human-readable than{4, :element, 1, {2, :alt, 10}}was, and vastly better than{4, :element, 1, <id_57>}would have been.
Trade-offs
- Initial Refactoring Effort: This is a significant architectural change that touches
Tdd.Core(to recognize applicator nodes),Tdd.PredicateLogic, and all type constructors. - Variable Complexity: The variable tuples themselves become more deeply nested. This is a minor cost for the massive gain in clarity and canonicity.
In summary, this migration moves the "context" information from an ad-hoc part of the variable's value into a systematic, structural prefix. This allows the semantic reasoning engine (PredicateLogic) to become simpler, more general, and recursive, while simultaneously fixing fundamental correctness and canonicity issues with operations on complex types. It is a textbook example of how a better data representation simplifies the algorithms that operate on it.
==============================================================================
==============================================================================
@ functions -> intersections between functions in elixir need to work differently I think - multiple function heads can match on different types of arguments. When a function is applied, we cannot have a single general type for the function, but need to find the part of the intersection that matches the arguments -> and use this function head.
@ polymorphism -> if this approach Youve outlined is only limited to good what'd be a state of the art approach ?
==============================================================================
Excellent points. You've correctly identified the nuances of Elixir's multiple function clauses and are pushing for the true state-of-the-art in polymorphism. Let's dive deep into both.
Part 1: Functions in Elixir and Set-Theoretic Types
You are absolutely right. A single Elixir function name like my_func is not a single function type but a union of function types, where each clause corresponds to one type in the union.
Let's say you have:
def my_func(x) when is_atom(x), do: :a
def my_func(x) when is_integer(x), do: :i
This is not a single fun(any -> atom()). It is (fun(atom -> :a)) | (fun(integer -> :i)). This is often called an overloaded function or a disjoint function union.
The TDD system you've designed is perfectly suited to represent this!
How it Works with Your TDD Design
-
Representing a Single Clause: Each function clause is a simple function type.
def my_func(x) when is_atom(x)isfun(atom() -> any()). Let's call its TDDF_atom.def my_func(x) when is_integer(x)isfun(integer() -> any()). Let's call its TDDF_int.
-
Representing the Whole Function: The entire
my_funcis the union of these types.Tdd_my_func = Tdd.sum(F_atom, F_int)
This model correctly captures the semantics.
Intersection of Overloaded Functions
Now, what does it mean to intersect two such functions? Let's say we have another function:
def other_func(x) when is_integer(x), do: "hello"
def other_func(x) when is_binary(x), do: "world"
This is the type (fun(integer -> string)) | (fun(binary -> string)). Let's call its TDD Tdd_other_func.
The intersection Tdd.intersect(Tdd_my_func, Tdd_other_func) means: "What is the set of functions that conform to both my_func's type signature and other_func's?"
This is ((fun(atom->any)) | (fun(int->any))) & ((fun(int->string)) | (fun(binary->string))).
Distributing the intersection over the union gives:
(fun(atom->any) & fun(int->string))->fun((atom|int) -> (any&string))(fun(atom->any) & fun(binary->string))->fun((atom|binary) -> (any&string))(fun(int->any) & fun(int->string))->fun((int|int) -> (any&string))which simplifies tofun(int -> string)(fun(int->any) & fun(binary->string))->fun((int|binary) -> (any&string))
The result is a complex union of function types. This is where the simple fun(A1|A2 -> R1&R2) meet operation shows its limits.
A more accurate model for intersection of overloaded functions is to find the domain of overlap. A value can be passed to the "intersected function" if and only if it's accepted by both original functions. The return type is the intersection of the return types for that specific domain.
my_funcacceptsatom | integer.other_funcacceptsinteger | binary.- The overlapping domain is
(atom | integer) & (integer | binary) = integer. - For an
integerinput:my_funcreturnsany.other_funcreturnsstring.- The intersection return type is
any & string = string.
- Therefore, the semantic intersection is
fun(integer -> string).
How to Implement This with TDDs:
You would need a specialized apply_function_intersect(f1_id, f2_id) function. It cannot be generic.
- Deconstruct
f1andf2into their union components (e.g.,(fun(A1->R1) | fun(A2->R2))). This is hard with a TDD representation. - For each pair of components
(fun(Ai->Ri))fromf1and(fun(Bj->Sj))fromf2: a. Calculate the domain intersection:D_ij = intersect(Ai, Bj). b. IfD_ijis notnone, calculate the return type intersection:R_ij = intersect(Ri, Sj). c. The result for this pair isfun(D_ij -> R_ij). - The final result is the
sumof allfun(D_ij -> R_ij)from step 2c.
Conclusion for Functions: Your observation is spot on. Elixir functions are unions of types. The TDD can represent this union, but operating on them (like intersect) requires highly specialized, non-generic logic that understands the specific semantics of function overloading and variance. The TDD becomes a data structure to represent the argument/return types, but the main algorithm is custom.
Part 2: State-of-the-Art Polymorphism
Your "limited to good" assessment is fair. The constraint-generation approach is powerful but can be improved. The state-of-the-art revolves around a concept called Bidirectional Type Checking and integrating the constraint solver more deeply.
The State-of-the-Art Approach: "Semantic Subtyping" with Bidirectional Checking
Instead of making the TDD operations (intersect, sum) generate constraints, we keep them purely about concrete types. Polymorphism is handled by the type checker/inference engine itself, which uses the TDDs as a tool.
The core algorithm is is_subtype(sub_id, super_id). We redefine it to handle polymorphism.
Let's call it check(Value, Type) and infer(Expression).
Key Idea:
When we check Value :: Type, if Type is polymorphic (contains free type variables like a), we don't try to build a TDD for list(a). Instead, we check the value against the type's structure and gather constraints on the type variables as we go.
Example: Checking [1, 2, 3] :: list(a)
-
check([1, 2, 3], list(a))- The
checkfunction forlist(a)first checks that[1, 2, 3]is indeed a list. The TDD operationis_subtype(type_of([1,2,3]), type_list())passes. - Now, it must check the elements. It iterates through
[1, 2, 3]. - For element
1: It recursively callscheck(1, a). - For element
2: It recursively callscheck(2, a). - For element
3: It recursively callscheck(3, a).
- The
-
check(Value, a)(whereais a type variable)- This is the crucial step. This function doesn't return
true/false. It generates a constraint. check(1, a)infers the type of1isinteger(). It generates the constraint:integer <: a.check(2, a)generatesinteger <: a.check(3, a)generatesinteger <: a.
- This is the crucial step. This function doesn't return
-
Constraint Solving
- After checking the whole expression, we have a set of constraints:
{ integer <: a, integer <: a, integer <: a }. - We pass this set to a constraint solver. The solver finds the "principal type" or the most general solution.
- The solution to
integer <: aisa = integer. (Or more generally,acould beanyornumber, butintegeris the tightest bound, which is what we want).
- After checking the whole expression, we have a set of constraints:
Why is this State-of-the-Art?
-
Separation of Concerns: The TDD engine remains a pure, powerful engine for reasoning about concrete set-theoretic types. It does one thing and does it well. The type checker/inference engine handles the separate concern of polymorphism and constraint generation.
-
Bidirectionality: The system has two modes:
- Inference Mode (
infer): "What is the most specific type of this expression?"infer([1, 2, 3])would use the TDDsumoperation to producetype_list_of(type_int_eq(1) | type_int_eq(2) | type_int_eq(3)). The TDD engine is perfect for this. - Checking Mode (
check): "Does this expression conform to this (potentially polymorphic) type?" This is where constraints are generated.
- Inference Mode (
-
Higher-Rank Polymorphism: This approach scales naturally to higher-rank types (e.g.,
fun(f :: (a -> a)) -> ...). When checking an argument against(a -> a), you introduce a local, scoped type variableaand check that the provided function works for any choice ofa. -
Integration with TDDs: The TDDs are the "oracle" that the constraint generator consults.
- When solving constraints like
Type1 <: aandType2 <: a, the solver needs to find the least upper bound (LUB) or join ofType1andType2. This isTdd.sum(Type1, Type2)! - When solving
a <: Type1anda <: Type2, the solver needs the greatest lower bound (GLB) or meet. This isTdd.intersect(Type1, Type2)!
- When solving constraints like
The TDD engine becomes the computational backend for the constraint solver.
Summary of State-of-the-Art Design
-
TDD Engine:
- Uses the "Contextualized Predicates" design.
- Represents and operates on concrete (monomorphic) types ONLY.
- Provides
intersect(meet/GLB),sum(join/LUB),negate, andis_subtype(for concrete types). - The engine itself knows nothing about polymorphism.
-
Type Checker / Inference Engine (The "Brain"):
- Is built on top of the TDD engine.
- Implements a bidirectional algorithm (
checkandinfer). - When it encounters a polymorphic type in
checkmode, it traverses the type's structure and the expression's structure in parallel. - It uses
inferto get the concrete type of parts of the expression. - It generates constraints on type variables (e.g.,
Tdd_id_of_int <: a).
-
Constraint Solver:
- Receives a set of constraints from the Type Checker.
- Uses the TDD engine's
sumandintersectoperations to solve for the type variables. - Reports success or a type error if constraints are unsatisfiable (e.g.,
integer <: aandatom <: aare generated, soamust beinteger | atom. But if latera <: integeris required, this leads tointeger | atom <: integer, whichis_subtypewill report as false -> contradiction).
This layered architecture is robust, modular, and mirrors the design of systems like TypeScript, Flow, and other modern typed languages. It lets each component do what it's best at.
==============================================================================
==============================================================================
@ functions -> I don't think what You've outlined I need
def t(int) when is_integer(int), do: :integer
def t(binary) when is_binary(int), do: :binary
def t(other) do: nil
the return types of t are 3 separate literal atoms. When someone applies t(1) the type of the return should be literal :integer
==============================================================================
You are absolutely right. My previous explanation was too focused on the general case of function type intersection and didn't fully capture the precise, practical need you've described for Elixir. Your example clarifies the goal perfectly: type analysis should be able to determine the exact return type based on the exact input type, respecting Elixir's clause matching rules.
This isn't about intersecting two different functions; it's about specializing a single overloaded function's type for a given input type.
Let's design a system that does exactly this. It's a fantastic application of the TDD engine.
The Goal: A specialize Function
What we need is a function with this signature:
specialize(function_type_id, input_argument_type_id) -> return_type_id
Given a TDD for an overloaded function and a TDD for an input argument, it should return the TDD for the corresponding output.
Example Usage:
specialize(Tdd_t, Tdd_integer) -> Tdd_literal_integer_atomspecialize(Tdd_t, Tdd_binary) -> Tdd_literal_binary_atomspecialize(Tdd_t, Tdd_atom) -> Tdd_nil(since:atomwill match theotherclause)specialize(Tdd_t, Tdd_int_or_bin) -> Tdd_integer_atom_or_binary_atom
Representing an Overloaded Function
First, we need a better way to represent the function t. As we discussed, it's a union of function types, but a simple TDD sum loses the crucial link between a specific input domain and its specific return type.
The ideal representation is not a single TDD, but a list of pairs, where each pair represents one function clause:
# This is a meta-level data structure, not a single TDD.
function_t_clauses = [
{Tdd.type_integer(), Tdd.type_atom_literal(:integer)}, # fun(integer -> :integer)
{Tdd.type_binary(), Tdd.type_atom_literal(:binary)}, # fun(binary -> :binary)
{Tdd.type_any(), Tdd.type_atom_literal(nil)} # fun(any -> nil)
]
Crucial Rule: This list must be ordered exactly like Elixir's function clauses. The first match wins. The final any clause is the catch-all.
The specialize Algorithm
Now, we can implement specialize(function_clauses, input_arg_type_id).
def specialize(function_clauses, input_arg_type_id) do
# We start with the full set of possible inputs we're considering.
# As we find matches, we'll subtract the matched portion from this set.
remaining_input_type = input_arg_type_id
# This will accumulate the possible return types from all matched clauses.
# We start with `none` because no matches have been found yet.
total_return_type = Tdd.type_none()
for {clause_input_domain, clause_return_type} <- function_clauses do
# If there are no more possible inputs to match, we can stop early.
if remaining_input_type == Tdd.type_none() do
break
end
# Step 1: Find the portion of our input that matches this specific clause.
# This is the core TDD operation.
# e.g., if remaining_input is `integer() | atom()` and clause_domain is `integer()`,
# the matching_part is `integer()`.
matching_part = Tdd.intersect(remaining_input_type, clause_input_domain)
# Step 2: Check if there was any overlap.
if matching_part != Tdd.type_none() do
# If there was a match, the return type for this part is this clause's return type.
# We add it to our total set of possible return types.
total_return_type = Tdd.sum(total_return_type, clause_return_type)
# Step 3: VERY IMPORTANT - Remove the matched part from the remaining inputs.
# This ensures that a given input type can only match ONE clause (the first one).
# remaining_input = remaining_input - matching_part
# which is equivalent to: remaining_input & ~matching_part
remaining_input_type = Tdd.intersect(remaining_input_type, Tdd.negate(matching_part))
end
end
# The final result is the union of all possible return types from the matching clauses.
total_return_type
end
Let's Trace the Algorithm
Case 1: specialize(clauses, Tdd.type_int_eq(5))
-
remaining_input_type=int(5) -
total_return_type=none -
Clause 1:
{integer, :integer}matching_part=intersect(int(5), integer)->int(5)(sinceint(5)is a subtype ofinteger)matching_partis notnone.total_return_type=sum(none, :integer)->:integerremaining_input_type=intersect(int(5), negate(int(5)))->none
-
Loop sees
remaining_input_typeisnoneand breaks. -
Return:
Tdd.type_atom_literal(:integer). Correct!
Case 2: specialize(clauses, Tdd.sum(type_int_eq(10), type_binary()))
-
remaining_input_type=int(10) | binary() -
total_return_type=none -
Clause 1:
{integer, :integer}matching_part=intersect(int(10)|binary, integer)->int(10)matching_partis notnone.total_return_type=sum(none, :integer)->:integerremaining_input_type=intersect(int(10)|binary, negate(int(10)))->binary()(The integer part was "consumed" by the match)
-
Clause 2:
{binary, :binary}remaining_input_typeis nowbinary().matching_part=intersect(binary, binary)->binary()matching_partis notnone.total_return_type=sum(:integer, :binary)->:integer | :binaryremaining_input_type=intersect(binary, negate(binary))->none
-
Loop sees
remaining_input_typeisnoneand breaks. -
Return:
Tdd.sum(type_atom_literal(:integer), type_atom_literal(:binary)). Correct! The type system knows that if you pass inint(10) | binary(), the possible return values are:integeror:binary.
Advantages of this Design
- Precision: It perfectly models Elixir's first-match policy for function clauses.
- Composability: It's built entirely from the core TDD primitives (
intersect,sum,negate,== type_none()). You don't need to change the TDD engine itself, only add this higher-level algorithm. - Correctness: It correctly handles partial and overlapping input types, producing a precise union of possible return types.
- Handles Guards: The
whenguards in Elixir are just part of the domain type.def f(x) when is_integer(x) and x > 0simply means the domain isTdd.intersect(type_integer(), type_int_gt(0)). The model handles this for free.
This specialize function is precisely what's needed for practical, sound type analysis of Elixir code. It bridges the gap between the general, set-theoretic world of the TDDs and the specific, ordered-clause semantics of the language.==============================================================================
==============================================================================
============================================================================== alright, would that play nice with out approach to polymorphism ? ==============================================================================
==============================================================================
Excellent question. Let's analyze how this new, precise specialize function for overloaded functions interacts with the state-of-the-art bidirectional approach to polymorphism we discussed.
The short answer is: Yes, it plays together beautifully. They are complementary parts of a complete type system, each handling a different aspect of the problem.
Here's the detailed breakdown of how they work in concert.
The Roles of Each Component
Let's recap the roles in our state-of-the-art system:
-
TDD Engine: The "calculator" for concrete types. Knows
intersect,sum,negate. It is pure and dumb about polymorphism and function application. -
specializeAlgorithm: The "Elixir function expert." It knows how to calculate the return type of an overloaded function for a given concrete input type. It uses the TDD engine as its calculator. -
Bidirectional Type Checker (
check/infer): The "brain" of the operation. It handles polymorphism, generates constraints, and orchestrates the other two components.
How They Interact: A Complete Trace
Let's trace a complex, polymorphic example from end to end.
The Code to Analyze:
# The overloaded function `t` from before.
def t(int) when is_integer(int), do: :integer
def t(binary) when is_binary(binary), do: :binary
def t(other), do: nil
# A polymorphic function `process` that uses `t`.
# @spec process(list(a)) :: list(return_type_of_t_for_a)
def process(list) do
Enum.map(list, &t/1)
end
# The specific call we want to type-check.
process([1, "hello"])
The goal is to infer the return type of process([1, "hello"]). The expected result should be list(:integer | :binary).
Step-by-Step Execution:
-
infer(process([1, "hello"]))- The type checker sees a function call. It needs to know the type of
processand the type of its argument[1, "hello"]. - It first calls
infer([1, "hello"]). - The TDD engine is used here.
infer(1)istype_int_eq(1).infer("hello")istype_string_literal("hello"). - The inferred type of the list is
list_of(sum(type_int_eq(1), type_string_literal("hello"))). Let's call this concrete input list typeT_InputList.
- The type checker sees a function call. It needs to know the type of
-
Lookup Type of
process- The checker looks up the polymorphic type spec for
process:fun(list(a) -> list(return_type_of_t_for_a)). - This type signature contains a free type variable,
a. It also contains a dependent type in the return signature. We will model this as a constraint. The type isfun(list(a) -> b) where b = list(specialize(t, a)).
- The checker looks up the polymorphic type spec for
-
Unification / Constraint Generation
- The checker now has to match the call
process(T_InputList)with the signaturefun(list(a) -> b). - This triggers
check(T_InputList, list(a)). - As we designed before, this generates a constraint.
T_InputListmust be a subtype oflist(a). - This implies that the elements of
T_InputListmust be a subtype ofa. - The element type of
T_InputListissum(type_int_eq(1), type_string_literal("hello")). - So, the first constraint generated is:
C1: sum(type_int_eq(1), type_string_literal("hello")) <: a.
- The checker now has to match the call
-
Solving for the Return Type
- The signature tells us the return type
bdepends ona. We have the constraintb = list(specialize(t, a)). - The constraint solver now takes over. It has one job: find the most specific types for
aandbthat satisfy the constraints. - From
C1, the most specific solution foraisa = sum(type_int_eq(1), type_string_literal("hello")). Let's call thisT_a.
- The signature tells us the return type
-
Invoking the
specializeAlgorithm- Now the solver must compute
b. It uses the second constraint:b = list(specialize(t, T_a)). - This is the moment of contact! The high-level polymorphic checker invokes our
specializefunction. - It calls
specialize(function_t_clauses, T_a).T_aisint(1) | string("hello").- The trace proceeds exactly as in my previous answer:
- The
integerclause matches theint(1)part, adding:integerto the return union. - The
binaryclause matches thestring("hello")part (assuming string is a binary), adding:binaryto the return union. - The result from
specializeissum(type_atom_literal(:integer), type_atom_literal(:binary)). Let's call thisT_return_elements.
- The
- Now the solver must compute
-
Final Result Construction
- The solver now knows
b = list(T_return_elements). - The final inferred type for
process([1, "hello"])islist(sum(type_atom_literal(:integer), type_atom_literal(:binary))).
- The solver now knows
The result is list(:integer | :binary). Success!
How it "Plays Nice" - The Synergy
- Orthogonality: The
specializefunction provides a key semantic capability (how to resolve overloaded functions) without needing to know anything about polymorphism. It operates on concrete TDDs. The bidirectional checker handles polymorphism without needing to know the specific rules of Elixir function resolution; it just needs a way to ask "what happens when I call this function with this type?" - Pluggable Semantics: The
specializealgorithm is a "semantic oracle" for the polymorphic type checker. The checker generates a concrete question (specialize(t, T_a)), andspecializeprovides a concrete answer by using the TDD engine. - No Leaky Abstractions: The TDD engine remains pure. The
specializefunction contains the domain-specific logic for Elixir. Thecheck/inferengine contains the domain-specific logic for polymorphism. They are clean, well-defined layers. - Dependent Types: This interaction is a form of a dependent type system, where the return type depends on the value (or in this case, the type) of an input argument. The combination of a polymorphic checker and the
specializefunction is exactly what's needed to model this.
In conclusion, not only do they play nice, they are essential partners. The polymorphic checker provides the framework for handling type variables, and the specialize function provides the concrete, language-specific meaning required to resolve the constraints generated by that framework.==============================================================================
==============================================================================
==============================================================================
==============================================================================
==============================================================================
==============================================================================
==============================================================================