cleanup

.aider.chat.history.md

@@ -56997,3 +56997,238 @@ mix test
 > Tokens: 82k sent, 1.6k received. Cost: $0.12 message, $0.26 session.  
 > lib/tilly/bdd.ex  
 > Add file to the chat? (Y)es/(N)o/(D)on't ask again [Yes]: y  
+
+# aider chat started at 2025-06-15 02:19:36
+
+> Newer aider version v0.84.0 is available.  
+> /home/omnissiah/.local/share/uv/tools/aider-chat/bin/python -m pip install --upgrade --upgrade-strategy only-if-needed aider-chat  
+> Run pip install? (Y)es/(N)o [Yes]: n  
+> You can skip this check with --no-gitignore  
+> Add .aider* to .gitignore (recommended)? (Y)es/(N)o [Yes]: n  
+> /home/omnissiah/.local/bin/aider --watch-files --model openrouter/google/gemini-2.5-pro-preview --api-key openrouter=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 --editor n  
+> Error: Read-only file /home/omnissiah/git/pl/CONVENTIONS.md does not exist. Skipping.  
+> Aider v0.83.2  
+> Model: openrouter/google/gemini-2.5-pro-preview with whole edit format  
+> Git repo: .git with 60 files  
+> Repo-map: using 4096 tokens, auto refresh  
+
+#### /map-refresh  
+> The repo map has been refreshed, use /map to view it.  
+
+# aider chat started at 2025-06-15 11:53:21
+
+> You can skip this check with --no-gitignore  
+> Add .aider* to .gitignore (recommended)? (Y)es/(N)o [Yes]: n  
+> /home/omnissiah/.local/bin/aider --watch-files --model openrouter/google/gemini-2.5-pro-preview --api-key openrouter=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 --editor n  
+> Error: Read-only file /home/omnissiah/git/pl/CONVENTIONS.md does not exist. Skipping.  
+> Aider v0.83.2  
+> Model: openrouter/google/gemini-2.5-pro-preview with whole edit format  
+> Git repo: .git with 62 files  
+> Repo-map: using 4096 tokens, auto refresh  
+
+#### /map-refresh  
+> The repo map has been refreshed, use /map to view it.  
+
+#### /add lib/til/tdd.ex  
+> Added lib/til/tdd.ex to the chat  
+
+#### /ask Please help me refine the theory for impementing set-theoritic types with this  
+
+#### Please help me refine the theory for impementing set-theoritic types with this  
+
+<thinking-content-7bbeb8e1441453ad999a0bbba8a46d4b>
+
+**Deconstructing the Core Task**
+
+I'm breaking down the user's request. I'm honing in on "refining the theory" and identifying set-theoretic types as the key area. My focus is to clearly delineate the core task, which is to refine the theoretical underpinnings for set-theoretic types, likely with the aim of improving a TDD/BDD implementation.
+
+
+**Identifying Key Challenges**
+
+I've moved on from the initial dissection and am now zeroing in on the core difficulties. The user's notes highlight two significant hurdles: integrating various types within a single TDD structure, and determining the appropriate content for a node cache. The initial exploration is revealing potential difficulties in managing the complexity of diverse set-theoretic types within a unified framework. The approach contrasts with existing methods that use multiple BDDs.
+
+
+**Evaluating Current Implementations**
+
+I'm now scrutinizing the user's existing codebase. The files indicate a TDD implementation, not a BDD as initially stated, which changes the scope. The user has, perhaps inadvertently, already adopted a CDuce-style approach within `tilly`. Key areas like "ignore_child" are revealing and warrant a deeper dive into the nuances of the current structure.
+
+
+**Re-evaluating the Architecture**
+
+I've refined my thinking about the apparent disconnect in the user's approach. Their `tilly` implementation, which they believe is a BDD implementation, is actually a TDD structure. This suggests they may be overcomplicating the process unnecessarily by creating a new TDD module in the root (`lib/til/tdd.ex`). I believe the existing codebase, which follows a CDuce-like style using separate domain-specific structures, already addresses many of their issues. I'm beginning to formulate a recommendation for an alternative approach, potentially using and extending the 'tilly' code.
+
+
+**Refining the Core Strategy**
+
+I'm solidifying the plan. My focus now is on articulating a concise, actionable recommendation. The core is to leverage and extend the user's existing `tilly` code. Specifically, I'll advise them to rename `lib/til/tdd.ex` to something like `lib/til/type.ex` and to refactor it, rather than trying to reinvent the wheel. The emphasis will be on utilizing and connecting their CDuce-inspired modules to create type descriptors that aggregate BDDs.
+
+
+**Synthesizing a Recommendation**
+
+I'm formulating the core advice for the user. It's become clear that they possess a capable, if slightly misidentified, TDD implementation within the `tilly` module, following a CDuce-style approach. The key suggestion is to embrace and extend this existing structure, advising a shift from the potentially complex idea of a single, overarching TDD, to the modular design already in place.
+
+
+**Synthesizing Key Insights**
+
+I'm organizing my thoughts on the user's work. My current focus is formulating a clear, concise set of recommendations, based on my analysis. I'll advise the user on a refactoring strategy. I'm also incorporating suggestions regarding the core architectural elements, highlighting the benefits of the approach already implemented in the user's `tilly` code.
+
+
+**Outlining the Solution**
+
+I'm now building the response structure. I'm preparing to inform the user about refactoring the provided code to leverage the CDuce-like approach within their `tilly` directory. My goal is to guide them towards a more efficient implementation based on their work, reframing the design as an evolution rather than a reinvention.
+
+
+**Summarizing the Process**
+
+I'm now compiling all the thoughts I've had to provide a clear and actionable response. I've clarified the user's key conceptual hurdles and their existing work, pinpointing a path to integrate their work and address their concerns. The current focus is a synthesis of the core insights into a concise and practical strategy.
+
+
+
+
+</thinking-content-7bbeb8e1441453ad999a0bbba8a46d4b>
+
+Of course. This is a fascinating and powerful area of computer science. Your notes in `lib/til/tdd.ex` show you're already thinking about the right problems (ordering, reduction, caching).
+
+Based on the files you've provided, especially the `tilly/bdd/*` and `tilly/type/store.ex` modules, it seems you have already built a solid foundation that is very close to the CDuce model you mentioned. My main recommendation is to **embrace and build upon your existing `tilly` implementation** rather than starting fresh in `lib/til/tdd.ex`.
+
+Here is a refined theory and a proposed path forward.
+
+### 1. Theory Refinement: The Composite Type Model
+
+Your central question is about a "single TDD" vs. the CDuce model of multiple BDDs. The latter is far more practical and is what your `tilly` code is already structured to do.
+
+**Let's refine the theory:**
+
+A **Type** is not a single BDD/TDD. A **Type** is a *composite descriptor* that maps base types (like `:integer`, `:string`, `:atom`) to the root ID of a BDD that represents the set of values for that base type.
+
+Your `Tilly.Type.Store` is the perfect place to manage these descriptors. A type descriptor would look like this:
+
+```elixir
+# Represents the type: (all integers) OR (the string "hello") OR (the atom :ok)
+%Tilly.Type.Descriptor{
+  id: 123, # A unique ID for this specific type combination
+  structure: %{
+    integer: 45,  # ID of a BDD representing all integers
+    string:  82,  # ID of a BDD representing the set {"hello"}
+    atom:    99   # ID of a BDD representing the set {:ok}
+  }
+}
+```
+
+*   **BDDs handle the details:** Each BDD (e.g., for integers) only needs to order integer values. The string BDD only orders strings. This solves your variable ordering problem.
+*   **The Type Descriptor handles the union:** The top-level type is the union of the sets represented by each BDD in its `structure` map.
+*   **The `Type.Store` handles identity:** By interning these descriptors (which `get_or_intern_descr` does), you achieve your goal: type equality becomes a simple ID comparison.
+
+### 2. Your Existing Code is a TDD, not a BDD
+
+Your `Tilly.BDD.Node.mk_split/4` function takes `positive_child_id`, `ignore_child_id`, and `negative_child_id`. This is the definition of a **Ternary Decision Diagram (TDD)** node, which is more powerful than a standard Binary Decision Diagram (BDD). This is great! TDDs are excellent for representing sequences and patterns, which might be useful later. For now, you can think of them as BDDs where the `ignore` branch is often unused for simple value sets.
+
+### 3. Answering Your Key Questions
+
+With this composite model in mind, let's re-answer your questions from `tdd.ex`:
+
+1.  **Structure of Ordered Variables:** You don't need a single, globally ordered list of all possible variables. Instead, each domain has its own BDD with its own ordering.
+    *   `IntegerBoolOps` defines ordering for integers.
+    *   `StringBoolOps` defines ordering for strings.
+    *   The top-level `Type.Descriptor` combines them.
+
+2.  **Node Cache:** Your intuition is correct, and you've already implemented it! You have two levels of caching:
+    *   **Type Descriptor Interning:** `Tilly.Type.Store` is your cache for the high-level type descriptors. This is the most important one for making `type1 == type2` fast.
+    *   **BDD Node Interning (Hash-Consing):** Within each BDD, you need to ensure that any node `(variable, yes_child, no_child)` is unique. This is how you achieve reduction. You would typically add a `unique_table` (a map) to your BDD context and use a smart constructor.
+
+3.  **Reduction Rules:** Reduction is not a separate step. It's enforced *during construction* by a "smart constructor" for nodes.
+
+    Let's imagine a `mk_split` function in `Tilly.BDD.Node`:
+
+    ```elixir
+    # In Tilly.BDD.Node, or a new BDD context module
+
+    # ctx would contain the unique_table and element store for this BDD
+    def mk_split(ctx, element, positive_child_id, negative_child_id) do
+      # Rule: Eliminate redundant nodes
+      if positive_child_id == negative_child_id do
+        return {ctx, positive_child_id}
+      end
+
+      # Rule: Merge isomorphic subgraphs (via hash-consing)
+      node_key = {:split, element, positive_child_id, negative_child_id}
+      case Map.get(ctx.unique_table, node_key) do
+        nil ->
+          # Not found, create a new node
+          new_node_id = # ... generate new ID
+          new_node = # ... create the node tuple
+          # Add to caches
+          ctx = put_in(ctx.unique_table[node_key], new_node_id)
+          ctx = put_in(ctx.nodes[new_node_id], new_node)
+          {ctx, new_node_id}
+        existing_id ->
+          # Found, return existing node ID
+          {ctx, existing_id}
+      end
+    end
+    ```
+
+### Recommended Plan
+
+1.  **Delete `lib/til/tdd.ex`**. Its purpose is better served by a new, higher-level module.
+
+2.  **Create `lib/til/type.ex`**. This will be the main public API for working with types. It will use `Tilly.Type.Store` and the `Tilly.BDD` modules internally.
+
+    ```elixir
+    # lib/til/type.ex
+    defmodule Til.Type do
+      @moduledoc "Public API for creating and operating on set-theoretic types."
+
+      # Example: Create a type representing the set of integers < 10
+      def int_less_than(typing_ctx, value) do
+        # 1. Use Tilly.BDD with IntegerBoolOps to build the BDD for this set.
+        # 2. Get the root ID of the resulting BDD.
+        # 3. Create a type descriptor: %{integer: bdd_root_id}
+        # 4. Intern this descriptor using Tilly.Type.Store.get_or_intern_descr/2
+        # 5. Return the new typing_ctx and the final type descriptor ID.
+      end
+
+      # Union of two types
+      def union(typing_ctx, type_id_1, type_id_2) do
+        # 1. Get descriptors for both type IDs from the Type.Store.
+        # 2. For each base type (e.g., :integer), get the BDD IDs from both descriptors.
+        # 3. Use the appropriate BDD union function (e.g., from IntegerBoolOps) on the two BDDs.
+        # 4. Collect the resulting BDD IDs into a new descriptor structure.
+        # 5. Intern the new descriptor and return its ID.
+      end
+
+      # intersection, negation, etc. would follow the same pattern.
+    end
+    ```
+
+3.  **Enhance `Tilly.BDD`** with a context/manager that holds the `unique_table` for node reduction, as sketched in the `mk_split` example above.
+
+This approach leverages the excellent foundation you've already built in the `tilly` namespace and provides a clear, scalable path to implementing a powerful type system.
+
+> Tokens: 4.4k sent, 2.5k received. Cost: $0.000000030 message, $0.000000030 session.  
+> lib/til/type.ex  
+> Add file to the chat? (Y)es/(N)o/(A)ll/(S)kip all/(D)on't ask again [Yes]: n  
+> notes  
+>  
+>  
+> ^C again to exit  
+>  
+>  
+> ^C KeyboardInterrupt  
+
+# aider chat started at 2025-06-15 11:55:56
+
+> You can skip this check with --no-gitignore  
+> Add .aider* to .gitignore (recommended)? (Y)es/(N)o [Yes]: n  
+> /home/omnissiah/.local/bin/aider --watch-files --model openrouter/google/gemini-2.5-pro-preview --api-key openrouter=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 --editor n  
+> Error: Read-only file /home/omnissiah/git/pl/CONVENTIONS.md does not exist. Skipping.  
+> Aider v0.83.2  
+> Model: openrouter/google/gemini-2.5-pro-preview with whole edit format  
+> Git repo: .git with 62 files  
+> Repo-map: using 4096 tokens, auto refresh  
+
+#### /context  
+> Aider v0.83.2  
+> Model: openrouter/google/gemini-2.5-pro-preview with context edit format  
+> Git repo: .git with 62 files  
+> Repo-map: using 8192 tokens, always refresh  

.aider.input.history

@@ -4158,3 +4158,27 @@
 
 # 2025-06-13 18:48:07.920080
 +y
+
+# 2025-06-15 02:19:44.496228
++n
+
+# 2025-06-15 02:23:11.675263
++/map-refresh
+
+# 2025-06-15 11:53:28.432969
++n
+
+# 2025-06-15 11:54:06.645621
++/map-refresh
+
+# 2025-06-15 11:54:11.240897
++/add lib/til/tdd.ex
+
+# 2025-06-15 11:54:52.625145
++/ask Please help me refine the theory for impementing set-theoritic types with this 
+
+# 2025-06-15 11:55:46.654825
++n
+
+# 2025-06-15 11:56:09.668461
++/context

.gitignore

@@ -24,3 +24,5 @@ pl-*.tar
 
 # Temporary files, for example, from tests.
 /tmp/
+
+.aider.tags.cache.v4/

g1

@@ -0,0 +1,318 @@
+```
+defmodule Tdd do
+  @moduledoc """
+  Ternary decision diagram, used for representing set-theoritic types, akin to cduce.
+  There are 2 types of nodes: 
+  - terminal nodes (true, false) 
+  - variable nodes 
+
+  variable nodes consist of:
+  - the variable being tested 
+  - yes: id of the node if the result of the test is true 
+  - no: id of the node if the result of the test is false 
+  - dc: id of the node if the result of the test is irrelevant for the current operation
+
+  the TDD needs to be ordered and reduced (ROBDD)
+  - 'ordered' if different variables appear in the same order on all paths from the root. 
+  - 'reduced' if the following two rules have been applied to its graph:
+    - Merge any isomorphic subgraphs.
+    - Eliminate any node whose two children are isomorphic.
+
+  Working notes:
+  - structure of the ordered variables:
+    Im thinking of structuring all possible types inside 1 TDD, in contrast to cduce, which uses a `desrc` structure that contains several TDDs (one for each domain, like ints, atoms, functions, etc.), and descr is a union between them.
+    For this, I need to come up with a variable structure that'll be ordered. 
+    My set types will need to represent types like: atoms, strings, ints, maps, tuples, functions, kinds? 
+    Moreso, those types themselves consist of smaller subsets of types like:
+    - int < 10 
+    - int in [1, 2, 3]
+    - string > "prefix_" 
+    - atom == false
+    - atom == false or atom == true or atom == nil
+    - map == %{"id" => string} and %{string => any | nil}
+    - etc.
+    Dont know how to represent them and make them ordered.
+  - node cache:
+     I don't yet know what it should contain, I suspect ids of nodes (TDDs) after reduction. This way a comparison between 2 types is just a pointer (id) check in the node cache. But not yet sure.
+  - reduction rules: not sure how to approach them 
+
+  """
+
+  def node(elem, yes, no, dc = _dont_care) do
+  end
+
+  def sum(one, two) do
+  end
+
+  def intersect(one, two) do
+  end
+
+  def negate(one, two) do
+  end
+end
+```
+Please help me refine the theory for impementing set-theoritic types with this 
+
+
+========================================================================================================================
+
+
+Okay, this is a fascinating and ambitious project! Building a TDD-based type system like CDuce is a significant undertaking. Let's refine the theory.
+
+You've got the core ideas right: terminals, variable nodes, and the need for ordering and reduction. The `dc` (don't care) child is the main differentiator from BDDs and key to TDDs' power in certain applications.
+
+Let's break down your working notes and expand on them.
+
+**1. Structure of Ordered Variables (The Core Challenge)**
+
+Your intuition to have a single TDD for all types is interesting. CDuce uses one TDD *per domain* (atoms, integers, etc.) and then a `descr` (descriptor) which is a union of these. A single TDD means your variable ordering must be global and able to discriminate across all these domains first, then within them.
+
+**Proposed Hierarchical Variable Ordering:**
+
+The variables in your TDD will represent *predicates* about a value. The order is crucial.
+
+*   **Level 0: Base Type Discriminators:** These variables test the fundamental Erlang/Elixir type of a value.
+    *   `is_atom?`
+    *   `is_integer?`
+    *   `is_float?`
+    *   `is_string?` (Elixir strings are UTF-8 binaries)
+    *   `is_binary?` (General binaries)
+    *   `is_list?`
+    *   `is_tuple?`
+    *   `is_map?`
+    *   `is_function?`
+    *   `is_pid?`
+    *   `is_reference?`
+    *   *Order*: Define a canonical order for these (e.g., alphabetical, or by commonality). Let's say `is_atom` < `is_binary` < `is_float` < ...
+
+*   **Level 1+: Type-Specific Predicates:** Once a base type is determined (e.g., the `yes` branch of `is_integer?` is taken), subsequent variables test properties specific to that type.
+
+    *   **For Atoms:**
+        *   `value_is(specific_atom)`: e.g., `value_is(true)`, `value_is(false)`, `value_is(nil)`, `value_is(:foo)`.
+        *   *Order*: Canonical order of the atoms themselves (e.g., `false` < `nil` < `true` < other atoms alphabetically).
+        *   This implies a potentially large number of variables if you want to distinguish many specific atoms. Often, you care about a few (booleans, nil) and "any other atom".
+
+    *   **For Integers:**
+        *   `value < N`, `value == N` (less common as a direct variable, usually derived), `value_in_range(A,B)`.
+        *   CDuce uses a finite partitioning of the integer line. For example, variables could be `value < 0`, `value < 10`, `value < MAX_INT_SMALL_ENOUGH_FOR_OPTIMIZATION`.
+        *   *Order*: `value < N1` < `value < N2` if `N1 < N2`.
+
+    *   **For Strings/Binaries:**
+        *   `length_is(L)` or `length_in_range(L1,L2)`
+        *   `prefix_is(prefix_string)`
+        *   `matches_regex(regex_pattern)` (Regexes can be complex to integrate directly as simple TDD variables due to their expressive power. CDuce has specific handling for regular expression types on sequences).
+        *   *Order*: By length, then by prefix lexicographically, etc.
+
+    *   **For Tuples:**
+        *   `arity_is(N)`
+        *   `element_at(Index)_is_type(TypeRef)`: This is recursive. `TypeRef` would be the ID of another TDD representing the type of the element.
+        *   *Order*: `arity_is(0)` < `arity_is(1)` < ... then `element_at(0)_is_type(T)` < `element_at(1)_is_type(T')`. The `TypeRef` itself would need to be part of the variable ordering if you allow different type tests for the same element index.
+
+    *   **For Maps:** This is the most complex.
+        *   `has_key(KeyAtomOrString)`
+        *   `value_for_key(Key)_is_type(TypeRef)`
+        *   `all_keys_are_type(KeyTypeRef)`
+        *   `all_values_are_type(ValueTypeRef)`
+        *   CDuce has specialized structures for map patterns. You might need variables like `matches_map_pattern(PatternID)`.
+        *   *Order*: By key name, then by tests on those keys.
+
+    *   **For Functions:**
+        *   `arity_is(N)`
+        *   `accepts_args_types(ArgTypesTupleRef)`
+        *   `returns_type(ReturnTypeRef)`
+        *   *Order*: By arity, then by argument types, then return type.
+
+**The "Variable" Itself:**
+A "variable" in your TDD node won't be just a name; it'll be an identifier that maps to a specific predicate function and its parameters. E.g., `var_id = 101` might mean `fn val -> is_integer(val) and val < 10 end`. You'll need a global, ordered registry of these predicate variables.
+
+**2. Node Cache (`unique_table`)**
+
+Yes, this is crucial for the "reduced" property.
+*   It's a hash table mapping `(variable_id, yes_node_id, no_node_id, dc_node_id)` to a unique `node_id`.
+*   **Terminals:**
+    *   `true_node_id` (e.g., 1): Represents the "any" type or universal set.
+    *   `false_node_id` (e.g., 0): Represents the "empty" type or bottom type.
+    These are the leaves of your TDD.
+*   When you create a node, you first check this table. If an identical node (same variable and children) exists, you reuse its ID. Otherwise, you create a new one, assign it a new ID, and store it.
+*   This ensures that any isomorphic subgraphs are merged (Reduction Rule 1).
+
+**3. Reduction Rules**
+
+You've listed the ROBDD rules. Let's adapt them for TDDs:
+
+*   **Merge any isomorphic subgraphs:** Handled by the `unique_table` as described above. Two subgraphs are isomorphic if they are structurally identical (same variables in same places leading to same terminals or further isomorphic subgraphs).
+*   **Eliminate any node whose three children are isomorphic:** If `yes_id == no_id == dc_id` for a variable node `v`, then the test `v` is irrelevant for distinguishing the type further down this path. The node `(v, child_id, child_id, child_id)` should be replaced by `child_id`. This rule is applied *before* looking up/inserting into the `unique_table`.
+
+**The Role of `dc` (Don't Care):**
+
+The `dc` child is what makes it a TDD. It typically means the variable being tested is irrelevant or its value doesn't affect membership for a particular path or operation.
+
+*   **In Type Representation:**
+    *   If you're representing the type "integer", and your current variable is `is_atom?`:
+        *   `yes` child would be `false_node_id` (an integer is not an atom).
+        *   `no` child would lead to further tests for integers (or `true_node_id` if "integer" is all you're specifying).
+        *   `dc` child: This is tricky for pure representation. If the variable `is_atom?` *must* be evaluated, then `dc` might also be `false_node_id`.
+    *   However, `dc` becomes powerful when combining types or dealing with partially specified types. If a type expression doesn't constrain variable `v`, its `dc` branch relative to `v` might be taken.
+    *   Consider the type `any`. For any variable `v`, the node would be `(v, true_node_id, true_node_id, true_node_id)`. By reduction rule 2, this simplifies to just `true_node_id`.
+    *   Consider the type `none` (empty set). For any variable `v`, node is `(v, false_node_id, false_node_id, false_node_id)`, reduces to `false_node_id`.
+
+*   **In Operations (`sum`, `intersect`, `negate`):** The `dc` child is heavily used in the `apply` algorithm.
+    When `apply(op, tdd1, tdd2)`:
+    *   If `var(tdd1) == var(tdd2)`: Recurse on `(op, tdd1.yes, tdd2.yes)`, `(op, tdd1.no, tdd2.no)`, `(op, tdd1.dc, tdd2.dc)`.
+    *   If `var(tdd1) < var(tdd2)` (in global order): `tdd2` doesn't explicitly test `var(tdd1)`. So, `var(tdd1)` is effectively "don't care" for `tdd2`.
+        The operation proceeds by testing `var(tdd1)`:
+        *   `yes_child = apply(op, tdd1.yes, tdd2)`
+        *   `no_child = apply(op, tdd1.no, tdd2)`
+        *   `dc_child = apply(op, tdd1.dc, tdd2)` (This is where TDD differs significantly from BDD's apply).
+        The new node is `mknode(var(tdd1), yes_child, no_child, dc_child)`.
+    *   Symmetric case for `var(tdd2) < var(tdd1)`.
+
+**4. `mknode(variable_id, yes_id, no_id, dc_id)` function:**
+
+This is your core constructor.
+
+```elixir
+defmodule Tdd do
+  # Store nodes in an array/map, IDs are indices/keys
+  # @nodes %{0 => :false_terminal, 1 => :true_terminal, ...}
+  # @unique_table %{{var_id, yes_id, no_id, dc_id} => node_id}
+  # @variables %{var_id => {predicate_fun, predicate_params, global_order_index}}
+
+  @true_id 1
+  @false_id 0
+
+  # Internal state for unique table, nodes, variable definitions
+  # This would typically be in a GenServer or an ETS table in a real system
+  # For simplicity, let's imagine it's passed around or module attributes are used carefully.
+
+  # Example variable IDs (you'd have a system for this)
+  # @var_is_atom 10
+  # @var_is_integer 11
+  # @var_int_lt_10 20
+
+  def get_true(), do: @true_id
+  def get_false(), do: @false_id
+
+  # Pseudo-code for mknode
+  def node(variable_id, yes_id, no_id, dc_id) do
+    # Reduction Rule 2: Eliminate node whose children are isomorphic
+    if yes_id == no_id and no_id == dc_id do
+      # If all children are the same, this variable provides no discrimination
+      # for this path. The node is redundant.
+      return yes_id
+    end
+
+    # Check unique_table (conceptually)
+    # entry = {variable_id, yes_id, no_id, dc_id}
+    # if Map.has_key?(@unique_table, entry) do
+    #   return @unique_table[entry]
+    # else
+    #   new_node_id = generate_new_id()
+    #   @nodes = Map.put(@nodes, new_node_id, {variable_id, yes_id, no_id, dc_id})
+    #   @unique_table = Map.put(@unique_table, entry, new_node_id)
+    #   return new_node_id
+    # end
+    # Actual implementation would use a GenServer or ETS for state
+    :not_implemented_yet # Placeholder
+  end
+end
+```
+
+**5. Operations (`sum`, `intersect`, `negate`)**
+
+These are built using a generic `apply` function, often memoized (using a `computed_table`).
+
+`apply(op_lambda, tdd1_id, tdd2_id)`:
+1.  **Handle terminal cases:**
+    *   `op_lambda.(@false_id, @false_id)`, `op_lambda.(@false_id, @true_id)`, etc.
+    *   Some ops have identities/annihilators:
+        *   Union: `T | true = true`, `T | false = T`.
+        *   Intersection: `T & false = false`, `T & true = T`.
+2.  **Check `computed_table`:** `cache_key = {op_lambda_id, tdd1_id, tdd2_id}`. If result exists, return it.
+3.  **Recursive step:**
+    *   Fetch node data for `tdd1_id` and `tdd2_id`. Let them be `N1`, `N2`.
+    *   Let `v1 = N1.variable_id`, `v2 = N2.variable_id`.
+    *   Compare `v1` and `v2` based on global variable order.
+        *   **If `v1 == v2`**:
+            `res_yes = apply(op_lambda, N1.yes, N2.yes)`
+            `res_no  = apply(op_lambda, N1.no, N2.no)`
+            `res_dc  = apply(op_lambda, N1.dc, N2.dc)`
+            `result = mknode(v1, res_yes, res_no, res_dc)`
+        *   **If `v1 < v2` (in order)**:
+            `res_yes = apply(op_lambda, N1.yes, tdd2_id)`
+            `res_no  = apply(op_lambda, N1.no, tdd2_id)`
+            `res_dc  = apply(op_lambda, N1.dc, tdd2_id)`
+            `result = mknode(v1, res_yes, res_no, res_dc)`
+        *   **If `v1 > v2` (in order)**: (symmetric to above)
+            `res_yes = apply(op_lambda, tdd1_id, N2.yes)`
+            `res_no  = apply(op_lambda, tdd1_id, N2.no)`
+            `res_dc  = apply(op_lambda, tdd1_id, N2.dc)`
+            `result = mknode(v2, res_yes, res_no, res_dc)`
+4.  Store `result` in `computed_table` for `cache_key`.
+5.  Return `result`.
+
+**`negate(tdd_id)`:**
+This is simpler, an `apply_unary` operation.
+1.  If `tdd_id == @true_id`, return `@false_id`.
+2.  If `tdd_id == @false_id`, return `@true_id`.
+3.  Check `computed_table_for_negation`.
+4.  Fetch node `N`.
+    `res_yes = negate(N.yes)`
+    `res_no  = negate(N.no)`
+    `res_dc  = negate(N.dc)`
+    `result = mknode(N.variable_id, res_yes, res_no, res_dc)`
+5.  Store and return `result`.
+
+**Concrete Example: Type `atom(:foo) | atom(:bar)`**
+
+Variables (simplified order): `is_atom`, `atom_is_foo`, `atom_is_bar`.
+1.  TDD for `atom(:foo)`:
+    *   `v_is_atom = mknode(:is_atom, v_atom_is_foo, @false_id, @false_id)`
+    *   `v_atom_is_foo = mknode(:atom_is_foo, @true_id, @false_id, @false_id)`
+    (Assuming if not atom, or atom but not foo, it's false. `dc` is false as these tests are always relevant here).
+2.  TDD for `atom(:bar)`:
+    *   `v_is_atom_2 = mknode(:is_atom, v_atom_is_bar, @false_id, @false_id)`
+    *   `v_atom_is_bar = mknode(:atom_is_bar, @true_id, @false_id, @false_id)`
+
+Now, `sum(tdd_foo, tdd_bar)` using logical OR (`||`):
+Top variable is `:is_atom` for both.
+`res_yes = apply(||, v_atom_is_foo, v_atom_is_bar)`
+`res_no  = apply(||, @false_id, @false_id)` -> `@false_id`
+`res_dc  = apply(||, @false_id, @false_id)` -> `@false_id`
+
+Consider `apply(||, v_atom_is_foo, v_atom_is_bar)`:
+Variables are `:atom_is_foo` and `:atom_is_bar`. Assume `:atom_is_foo < :atom_is_bar`.
+Current var is `:atom_is_foo` (from `v_atom_is_foo`).
+`ry = apply(||, v_atom_is_foo.yes, v_atom_is_bar)`
+     `= apply(||, @true_id, v_atom_is_bar)` -> `@true_id` (since `true || X = true`)
+`rn = apply(||, v_atom_is_foo.no, v_atom_is_bar)`
+     `= apply(||, @false_id, v_atom_is_bar)` -> `v_atom_is_bar` (since `false || X = X`)
+`rd = apply(||, v_atom_is_foo.dc, v_atom_is_bar)`
+     `= apply(||, @false_id, v_atom_is_bar)` -> `v_atom_is_bar`
+
+So, `res_yes = mknode(:atom_is_foo, @true_id, v_atom_is_bar, v_atom_is_bar)`.
+This node effectively means: "If it's :foo, then true. Else (if not :foo), then it depends on whether it's :bar (from `v_atom_is_bar`). If :atom_is_foo is don't care, it also depends on :bar."
+The reduction rule for `no_id == dc_id` isn't standard for BDDs but might make sense for TDDs if "not X" and "X is irrelevant" lead to the same sub-condition. CDuce's BDDs don't have this `dc` child directly in nodes, it's more implicit in their algorithm.
+If we stick to standard ROBDD `apply` ideas slightly modified for three children, `dc` handling when variables differ is key.
+
+**Key Data Structures to Manage:**
+
+1.  **Node Storage:** A list, array, or map to store the actual nodes. An ID is an index/key into this.
+    *   `nodes = %{0 => {:terminal, :false}, 1 => {:terminal, :true}, 2 => {:node, var_id1, yes2, no2, dc2}, ...}`
+2.  **Unique Table:** `(variable_id, yes_id, no_id, dc_id) -> node_id`. This is for structural sharing and reduction rule 1.
+    *   `unique_table = %{{var_id1, yes2, no2, dc2} => 2, ...}`
+3.  **Variable Definitions:** A way to map `variable_id` to its actual predicate logic and its position in the global order.
+    *   `variables = %{var_id1 => %{name: :is_atom, order_idx: 0, predicate: &is_atom/1}, ...}`
+4.  **Computed Tables (Memoization for Operations):**
+    *   For binary ops: `{(op_name, id1, id2) -> result_id}`
+    *   For unary ops: `{(op_name, id1) -> result_id}`
+
+**Summary of Refinements:**
+
+1.  **Global Hierarchical Variable Ordering:** Discriminate base types first, then type-specific properties. All variables (predicates) need a unique ID and a place in this global order.
+2.  **`mknode` is Central:** It implements reduction rule 2 (all children same -> return child) and uses the `unique_table` (reduction rule 1).
+3.  **`apply` Algorithm:** This is the workhorse for `sum`, `intersect`, etc. Its logic for handling cases where variables differ across operands is where the TDD structure (and `dc` child) truly shows its behavior. The `dc` child of a node `N1=(v,y,n,d)` would be used in `apply(op, N1.dc, N2)` if `v < var(N2)` and the `dc` path for `v` is taken.
+4.  **`dc` Child Interpretation:** In the `apply` algorithm, if `var(T1) < var(T2)`, `T2` doesn't test `var(T1)`. So, `T2` is passed "as is" when considering `T1.yes`, `T1.no`, and `T1.dc`. The resulting node for `var(T1)` will have its children determined by these recursive calls. The `dc` child in a node structure `(v, Y, N, D)` represents the type if the predicate `v` is "skipped" or considered irrelevant for that path.
+5.  **State Management:** You'll need a robust way to manage the shared state of nodes, unique table, and computed tables (e.g., a GenServer or ETS tables).
+
+This is a complex system. Start simple: implement the `mknode` with unique table for just atoms and booleans. Then add `negate`. Then `sum` or `intersect`. Gradually add more complex variable types. Good luck!

g2.md

@@ -0,0 +1,216 @@
+```
+defmodule Tdd do
+  @moduledoc """
+  Ternary decision diagram, used for representing set-theoritic types, akin to cduce.
+  There are 2 types of nodes: 
+  - terminal nodes (true, false) 
+  - variable nodes 
+
+  variable nodes consist of:
+  - the variable being tested 
+  - yes: id of the node if the result of the test is true 
+  - no: id of the node if the result of the test is false 
+  - dc: id of the node if the result of the test is irrelevant for the current operation
+
+  the TDD needs to be ordered and reduced (ROBDD)
+  - 'ordered' if different variables appear in the same order on all paths from the root. 
+  - 'reduced' if the following two rules have been applied to its graph:
+    - Merge any isomorphic subgraphs.
+    - Eliminate any node whose two children are isomorphic.
+
+  Working notes:
+  - structure of the ordered variables:
+    Im thinking of structuring all possible types inside 1 TDD, in contrast to cduce, which uses a `desrc` structure that contains several TDDs (one for each domain, like ints, atoms, functions, etc.), and descr is a union between them.
+    For this, I need to come up with a variable structure that'll be ordered. 
+    My set types will need to represent types like: atoms, strings, ints, maps, tuples, functions, kinds, free polymorphic variables 
+    Moreso, those types themselves consist of smaller subsets of types like:
+    - int < 10 
+    - int in [1, 2, 3]
+    - string > "prefix_" 
+    - atom == false
+    - atom == false or atom == true or atom == nil
+    - map == %{"id" => string} and %{string => any | nil}
+    - polymorphic types ???
+    - etc.
+    Dont know how to represent them and make them ordered.
+  - node cache:
+    I suspect ids of nodes (TDDs) after reduction. This way a comparison between 2 types is just a pointer (id) check in the node cache. But not yet sure.
+  - reduction rules: not sure how to approach them 
+
+  """
+
+  def node(elem, yes, no, dc = _dont_care) do
+  end
+
+  def sum(one, two) do
+  end
+
+  def intersect(one, two) do
+  end
+
+  def negate(one, two) do
+  end
+end
+```
+Please help me refine the theory for impementing set-theoritic types with this.
+Lets focus on ordering of variables in the TDD
+
+========================================================================================================================
+
+Okay, this is a fascinating and ambitious goal! Building a single, ordered, reduced TDD for all Elixir/Erlang types is a significant challenge, especially with the rich structure of types like maps and functions. Let's break down the ordering of variables.
+
+The core idea for ordering in a BDD/TDD is to have a **total global order** on all possible "questions" (predicates) you can ask about a value.
+
+**High-Level Strategy for Ordering Variables**
+
+1.  **Primary Type Discriminators First:** The most fundamental question is "What basic kind of thing is this?"
+2.  **General Properties Next:** After knowing the primary type, ask about general properties (e.g., size, length).
+3.  **Specific Value/Content Properties:** Then, delve into specific values or structural content.
+4.  **Recursive Structure for Nested Types:** For types like tuples and maps, the predicates about their elements/values will effectively be recursive, but the ordering system must flatten this into a global order.
+
+**Proposed Variable Ordering Scheme**
+
+Let's define "variables" as unique identifiers for predicates. We need a way to sort these identifiers. A good way is to use tuples, where Elixir's natural tuple sorting provides the order.
+
+**Category 0: Primary Type Discriminators**
+These are the most fundamental. They will have the lowest sort order.
+Order them alphabetically by the type name.
+*   `v_is_atom = {0, :is_atom}`
+*   `v_is_binary = {0, :is_binary}`
+*   `v_is_float = {0, :is_float}`
+*   `v_is_function = {0, :is_function}`
+*   `v_is_integer = {0, :is_integer}`
+*   `v_is_list = {0, :is_list}`
+*   `v_is_map = {0, :is_map}`
+*   `v_is_pid = {0, :is_pid}`
+*   `v_is_port = {0, :is_port}`
+*   `v_is_reference = {0, :is_reference}`
+*   `v_is_string = {0, :is_string}` (*Note: Elixir strings are UTF-8 binaries. You might treat them as a subtype of binary or a distinct primary type in your model. For simplicity here, let's assume distinct for now, or you'd have predicates like `{0, :is_binary_utf8}` after `{0, :is_binary}`*)
+*   `v_is_tuple = {0, :is_tuple}`
+
+**Category 1: Atom-Specific Predicates**
+If `is_atom` is true, what specific atom is it?
+Order by the atom itself.
+*   `v_atom_eq_false = {1, :value, false}`
+*   `v_atom_eq_nil = {1, :value, nil}`
+*   `v_atom_eq_true = {1, :value, true}`
+*   `v_atom_eq_specific_A = {1, :value, :an_atom}` (e.g., `:an_atom` comes after `true`)
+*   ... (all known/relevant atoms in your system, ordered canonically)
+
+**Category 2: Integer-Specific Predicates**
+If `is_integer` is true:
+You need a canonical way to represent integer conditions.
+*   Equality: `v_int_eq_N = {2, :eq, N}` (e.g., `{2, :eq, 0}`, `{2, :eq, 10}`)
+    *   Order by N.
+*   Less than: `v_int_lt_N = {2, :lt, N}` (e.g., `{2, :lt, 0}`, `{2, :lt, 10}`)
+    *   Order by N.
+*   Greater than: `v_int_gt_N = {2, :gt, N}` (e.g., `{2, :gt, 0}`, `{2, :gt, 10}`)
+    *   Order by N.
+*   Set membership for finite sets: `v_int_in_SET = {2, :in, Enum.sort(SET)}` (e.g. `{2, :in, [1,2,3]}`)
+    *   Order by the canonical (sorted list) representation of SET.
+    *   *This gets complex. Often, BDDs for integers use bit-level tests, but for set-theoretic types, range/specific value tests are more natural.* You might limit this to a predefined, finite set of "interesting" integer predicates.
+
+**Category 3: String-Specific Predicates**
+If `is_string` is true:
+*   Equality: `v_string_eq_S = {3, :eq, S}` (e.g., `{3, :eq, "foo"}`)
+    *   Order by S lexicographically.
+*   Length: `v_string_len_eq_L = {3, :len_eq, L}`
+    *   Order by L.
+*   Prefix: `v_string_prefix_P = {3, :prefix, P}`
+    *   Order by P lexicographically.
+*   (Suffix, regex match, etc., can be added with consistent ordering rules)
+
+**Category 4: Tuple-Specific Predicates**
+If `is_tuple` is true:
+1.  **Size first:**
+    *   `v_tuple_size_eq_N = {4, :size, N}` (e.g., `{4, :size, 0}`, `{4, :size, 2}`)
+        *   Order by N.
+2.  **Element types (recursive structure in variable identifier):**
+    For a tuple of a *given size*, we then check its elements. The predicate for an element will re-use the *entire variable ordering scheme* but scoped to that element.
+    *   `v_tuple_elem_I_PRED = {4, :element, index_I, NESTED_PREDICATE_ID}`
+        *   Order by `index_I` first.
+        *   Then order by `NESTED_PREDICATE_ID` (which itself is one of these `{category, type, value}` tuples).
+    *   Example: Is element 0 an atom? `v_el0_is_atom = {4, :element, 0, {0, :is_atom}}`
+    *   Example: Is element 0 the atom `:foo`? `v_el0_is_foo = {4, :element, 0, {1, :value, :foo}}`
+    *   Example: Is element 1 an integer? `v_el1_is_int = {4, :element, 1, {0, :is_integer}}`
+    This ensures that all questions about element 0 come before element 1, and for each element, the standard hierarchy of questions is asked.
+
+**Category 5: Map-Specific Predicates**
+If `is_map` is true: This is the most complex.
+1.  **Size (optional, but can be useful):**
+    *   `v_map_size_eq_N = {5, :size, N}`
+        *   Order by N.
+2.  **Key Presence:**
+    *   `v_map_has_key_K = {5, :has_key, K}` (e.g., `{5, :has_key, "id"}`, `{5, :has_key, :name}`)
+        *   Order by K (canonically, e.g., strings before atoms, then lexicographically/atom-order).
+3.  **Key Value Types (recursive structure):**
+    For a *given key K* that is present:
+    *   `v_map_key_K_value_PRED = {5, :key_value, K, NESTED_PREDICATE_ID}`
+        *   Order by K (canonically).
+        *   Then order by `NESTED_PREDICATE_ID`.
+    *   Example: Does map have key `:id` and is its value a string?
+        *   First variable: `v_map_has_id = {5, :has_key, :id}`
+        *   If yes, next variable: `v_map_id_val_is_str = {5, :key_value, :id, {0, :is_string}}`
+4.  **Predicates for "all other keys" / "pattern keys":**
+    This is needed for types like `%{String.t() => integer()}`.
+    *   `v_map_pattern_key_PRED_value_PRED = {5, :pattern_key, KEY_TYPE_PREDICATE_ID, VALUE_TYPE_PREDICATE_ID}`
+    *   Example: For `%{String.t() => integer()}`:
+        *   Key type predicate: `{0, :is_string}`
+        *   Value type predicate for such keys: `{0, :is_integer}`
+        *   Variable ID: `{5, :pattern_key, {0, :is_string}, {0, :is_integer}}`
+    *   These pattern key predicates should likely be ordered *after* specific key predicates. The exact sorting of `KEY_TYPE_PREDICATE_ID` needs careful thought (e.g. `(0, :is_atom)` before `(0, :is_string)`).
+
+**Category 6: List-Specific Predicates**
+If `is_list` is true:
+1.  **Is Empty:**
+    *   `v_list_is_empty = {6, :is_empty}`
+2.  **Head/Tail Structure (if not empty, recursive):**
+    This mirrors how types like `nonempty_list(H, T)` are defined.
+    *   `v_list_head_PRED = {6, :head, NESTED_PREDICATE_ID}`
+    *   `v_list_tail_PRED = {6, :tail, NESTED_PREDICATE_ID}` (Note: `NESTED_PREDICATE_ID` for tail would again be list predicates like `{6, :is_empty}` or `{6, :head, ...}`)
+    *   Example: Head is an atom: `{6, :head, {0, :is_atom}}`
+    *   Example: Tail is an empty list: `{6, :tail, {6, :is_empty}}`
+    *   All head predicates come before all tail predicates.
+
+**Category 7: Function-Specific Predicates**
+If `is_function` is true:
+1.  **Arity:**
+    *   `v_fun_arity_eq_A = {7, :arity, A}`
+        *   Order by A.
+2.  **Argument Types (very complex, may need simplification for TDDs):**
+    *   `v_fun_arg_I_PRED = {7, :arg, index_I, NESTED_PREDICATE_ID}`
+3.  **Return Type (also complex):**
+    *   `v_fun_return_PRED = {7, :return, NESTED_PREDICATE_ID}`
+    *   Function types are often represented by separate structures or simplified in TDDs due to their higher-order nature. Full function type checking within this TDD variable scheme would be extremely elaborate.
+
+**Binary, Float, Pid, Port, Reference Predicates:**
+These would get their own categories (e.g., 8, 9, 10...).
+*   **Floats:** `{X, :is_float}` -> `{X, :eq, F}`, `{X, :lt, F}`, etc.
+*   **Binaries:** `{Y, :is_binary}` -> `{Y, :size, S}`, `{Y, :matches_pattern, Pat}` (e.g. `<<h :: size(8), _ :: binary>>`)
+
+**Polymorphic Variables (`alpha`, `beta`, etc.)**
+Polymorphic variables are part of the *type language*, not properties of concrete values. A TDD represents a set of *concrete values*.
+*   When you construct a TDD for a type like `list(alpha)`, where `alpha` is free, `alpha` essentially means `any`. So, for predicates concerning list elements, they would all go to their `dc` (don't care) branches, ultimately leading to `true`.
+*   If `alpha` is bound (e.g., in `(alpha -> alpha) where alpha = integer`), you first resolve `alpha` to `integer` and then build the TDD for `(integer -> integer)`.
+*   So, "free polymorphic variables" don't become TDD variables themselves. They influence which branches are taken during TDD construction for types containing them, often mapping to `any` or `dc` paths.
+
+**"Kinds"**
+The "kind" of a type (e.g., `Type.Atom`, `Type.Integer`) is meta-information. The TDD *represents* a type. The variables within the TDD are about properties of *values* that belong to that type. You wouldn't have a TDD variable `is_kind_atom?`. Instead, the TDD for the type `atom` would start with the `v_is_atom = {0, :is_atom}` variable.
+
+**The `dc` (Don't Care) Branch**
+The `dc` branch for a variable `v` in a node means that for the type being represented, the outcome of the test `v` is irrelevant to membership *given the path taken to reach this node*.
+*   For type `any`, all variables would effectively go to `dc`, all leading to the `true_terminal`.
+*   For type `integer`, the test `v_is_atom`:
+    *   `yes` branch -> `false_terminal` (an atom is not an integer)
+    *   `no` branch -> continues to test `v_is_integer`, etc.
+    *   `dc` branch: This is the tricky part in TDDs for types. In some formulations, `dc(N)` is `yes(N) U no(N)`. If a type truly doesn't care about `v_is_atom` (e.g., `any`), then `yes`, `no`, and `dc` might all point to the same child representing `any` for subsequent tests.
+    *   For `ROBDD` reduction with `dc`, if `yes_child == no_child == dc_child`, the node is redundant. If `yes_child == no_child`, the test `v` is locally irrelevant, and the node might be simplified (parent points to `yes_child`, and the `dc` path needs careful handling depending on the TDD algebra). Standard BDD reduction (if `yes_child == no_child`, eliminate node) assumes only two children. You'll need TDD-specific reduction rules.
+
+**Summary of Ordering Logic:**
+1.  Use tuples as variable identifiers: ` {category_num, predicate_type_atom, value_or_nested_id}`.
+2.  Sort these tuples using Elixir's default tuple comparison. This establishes the global order.
+3.  `category_num` provides the coarsest level of ordering.
+4.  Within a category, `predicate_type_atom` provides the next level.
+5.  Finally, `value_or_nested_id` provides the finest level, potentially recursively applying the same ordering logic for nested structures.
+
+This structured approach to variable identifiers is crucial for the "ordered" property of your ROBDD. When implementing `apply` operations (union, intersect, negate), you'll always compare the variable IDs of the current nodes from the two TDDs and operate on the one that comes first in the global order.

lib/til/tdd.ex

@@ -0,0 +1,51 @@
+defmodule Tdd do
+  @moduledoc """
+  Ternary decision diagram, used for representing set-theoritic types, akin to cduce.
+  There are 2 types of nodes: 
+  - terminal nodes (true, false) 
+  - variable nodes 
+
+  variable nodes consist of:
+  - the variable being tested 
+  - yes: id of the node if the result of the test is true 
+  - no: id of the node if the result of the test is false 
+  - dc: id of the node if the result of the test is irrelevant for the current operation
+
+  the TDD needs to be ordered and reduced (ROBDD)
+  - 'ordered' if different variables appear in the same order on all paths from the root. 
+  - 'reduced' if the following two rules have been applied to its graph:
+    - Merge any isomorphic subgraphs.
+    - Eliminate any node whose two children are isomorphic.
+
+  Working notes:
+  - structure of the ordered variables:
+    Im thinking of structuring all possible types inside 1 TDD, in contrast to cduce, which uses a `desrc` structure that contains several TDDs (one for each domain, like ints, atoms, functions, etc.), and descr is a union between them.
+    For this, I need to come up with a variable structure that'll be ordered. 
+    My set types will need to represent types like: atoms, strings, ints, maps, tuples, functions, kinds? 
+    Moreso, those types themselves consist of smaller subsets of types like:
+    - int < 10 
+    - int in [1, 2, 3]
+    - string > "prefix_" 
+    - atom == false
+    - atom == false or atom == true or atom == nil
+    - map == %{"id" => string} and %{string => any | nil}
+    - etc.
+    Dont know how to represent them and make them ordered.
+  - node cache:
+     I don't yet know what it should contain, I suspect ids of nodes (TDDs) after reduction. This way a comparison between 2 types is just a pointer (id) check in the node cache. But not yet sure.
+  - reduction rules: not sure how to approach them 
+
+  """
+
+  def node(elem, yes, no, dc = _dont_care) do
+  end
+
+  def sum(one, two) do
+  end
+
+  def intersect(one, two) do
+  end
+
+  def negate(one, two) do
+  end
+end

lib/til/type.ex

@@ -0,0 +1,817 @@
+defmodule Tilly.X.Type do
+  @moduledoc """
+  Core type system definitions for Tilly — a Lisp that transpiles to Elixir,
+  using set-theoretic types represented as Ternary Decision Diagrams (TDDs).
+
+  Supports:
+    - Set-theoretic types (union, intersection, negation)
+    - Structural polymorphism with `forall`
+    - Type constraints (e.g., Enumerable(~a))
+    - Structural map types
+  """
+
+  # === Monotype TDD Representation ===
+
+  defmodule TDD do
+    @moduledoc """
+    Represents a ternary decision diagram node for types.
+    """
+
+    defstruct [:decision, :yes, :no, :maybe]
+
+    @type t :: %__MODULE__{
+            decision: Tilly.Type.Decision.t(),
+            yes: TDD.t() | :any | :none,
+            no: TDD.t() | :any | :none,
+            maybe: TDD.t() | :any | :none
+          }
+  end
+
+  # === Type Variable ===
+
+  defmodule Var do
+    @moduledoc """
+    Represents a type variable in a polymorphic type.
+    """
+
+    defstruct [:name, constraints: []]
+
+    @type t :: %__MODULE__{
+            name: String.t(),
+            constraints: [Tilly.Type.Constraint.t()]
+          }
+  end
+
+  # === Structural Map Type ===
+
+  defmodule TDDMap do
+    @moduledoc """
+    Structural representation of a map type, with per-key typing and optional openness.
+    """
+
+    defstruct fields: [], rest: nil
+
+    @type t :: %__MODULE__{
+            fields: [{TDD.t(), TDD.t()}],
+            rest: TDD.t() | nil
+          }
+  end
+
+  @doc """
+  Checks if t1 is a subtype of t2 under the current substitution.
+  t1 <: t2  iff  t1 & (not t2) == None
+  """
+  def is_subtype(raw_t1, raw_t2, sub) do
+    # Use the apply_sub we defined/refined previously
+    t1 = tdd_substitute(raw_t1, sub)
+    t2 = tdd_substitute(raw_t2, sub)
+
+    # Handle edge cases with Any and None for robustness
+    cond do
+      # None is a subtype of everything
+      t1 == tdd_none() ->
+        true
+
+      # Everything is a subtype of Any
+      t2 == tdd_any() ->
+        true
+
+      # Any is not a subtype of a specific type (unless that type is also Any)
+      t1 == tdd_any() and t2 != tdd_any() ->
+        false
+
+      # A non-None type cannot be a subtype of None
+      t2 == tdd_none() and t1 != tdd_none() ->
+        false
+
+      true ->
+        # The core set-theoretic check: t1 \ t2 == None
+        tdd_diff(t1, t2) == tdd_none()
+
+        # Alternatively: Type.tdd_and(t1, t2) == t1 (but this can be tricky with complex TDDs if not canonical)
+        # The difference check is generally more direct for subtyping.
+    end
+  end
+
+  # === Type Decisions (Predicates) ===
+
+  defmodule Decision do
+    @moduledoc """
+    A type-level decision predicate used in a TDD node.
+    """
+
+    @type t ::
+            :is_atom
+            | :is_integer
+            | :is_float
+            | :is_binary
+            | :is_list
+            | :is_tuple
+            | :is_map
+            | :is_function
+            | :is_pid
+            | :is_reference
+            | {:literal, term()}
+            | {:tuple_len, pos_integer()}
+            | {:key, TDD.t()}
+            | {:has_struct_key, atom()}
+            | {:var, String.t()}
+  end
+
+  # === Type Constraints (structural predicates) ===
+
+  defmodule Constraint do
+    @moduledoc """
+    Represents a structural constraint on a type variable,
+    similar to a typeclass in Haskell or trait in Rust, but structural.
+    """
+
+    defstruct [:kind, :arg]
+
+    @type kind ::
+            :enumerable
+            | :collectable
+            | :struct_with_keys
+            | :custom
+
+    @type t :: %__MODULE__{
+            kind: kind(),
+            arg: String.t() | TDD.t() | any()
+          }
+  end
+
+  # === Polymorphic Types (forall + constraints) ===
+
+  defmodule PolyTDD do
+    @moduledoc """
+    Represents a polymorphic type with optional structural constraints.
+    """
+
+    defstruct [:vars, :body]
+
+    @type t :: %__MODULE__{
+            vars: [Var.t()],
+            body: TDD.t()
+          }
+  end
+
+  # === Constants for base types ===
+
+  @doc "A TDD representing the universal type (any value)"
+  def tdd_any, do: :any
+
+  @doc "A TDD representing the empty type (no values)"
+  def tdd_none, do: :none
+
+  @doc "Creates a TDD for a literal value"
+  def tdd_literal(value) do
+    %TDD{
+      decision: {:literal, value},
+      yes: :any,
+      no: :none,
+      maybe: :none
+    }
+  end
+
+  @doc "Creates a TDD for a base predicate (e.g., is_atom)"
+  def tdd_pred(pred) when is_atom(pred) do
+    %TDD{
+      decision: pred,
+      yes: :any,
+      no: :none,
+      maybe: :none
+    }
+  end
+
+  @doc "Creates a TDD for a type variable reference"
+  def tdd_var(name) when is_binary(name) do
+    %TDD{
+      decision: {:var, name},
+      yes: :any,
+      no: :none,
+      maybe: :none
+    }
+  end
+
+  @doc """
+  Performs type variable substitution in a TDD,
+  replacing variables found in the given `env` map.
+  """
+  def tdd_substitute(:any, _env), do: :any
+  def tdd_substitute(:none, _env), do: :none
+
+  def tdd_substitute(%TDD{decision: {:var, name}}, env) when is_map(env) do
+    Map.get(env, name, %TDD{decision: {:var, name}, yes: :any, no: :none, maybe: :none})
+  end
+
+  def tdd_substitute(%TDD{} = tdd, env) do
+    %TDD{
+      decision: tdd.decision,
+      yes: tdd_substitute(tdd.yes, env),
+      no: tdd_substitute(tdd.no, env),
+      maybe: tdd_substitute(tdd.maybe, env)
+    }
+  end
+
+  @doc """
+  Performs substitution in a polymorphic type, replacing all vars
+  in `vars` with given TDDs from `env`.
+  """
+  def poly_substitute(%PolyTDD{vars: vars, body: body}, env) do
+    var_names = Enum.map(vars, & &1.name)
+    restricted_env = Map.take(env, var_names)
+    tdd_substitute(body, restricted_env)
+  end
+
+  # === Constraints ===
+
+  @doc """
+  Checks whether a TDD satisfies a built-in structural constraint,
+  such as Enumerable or String.Chars.
+  """
+  def satisfies_constraint?(tdd, %Constraint{kind: :enumerable}) do
+    tdd_is_of_kind?(tdd, [:list, :map, :bitstring])
+  end
+
+  def satisfies_constraint?(tdd, %Constraint{kind: :string_chars}) do
+    tdd_is_of_kind?(tdd, [:bitstring, :atom])
+  end
+
+  def satisfies_constraint?(_tdd, %Constraint{kind: :custom}) do
+    raise "Custom constraints not implemented yet"
+  end
+
+  # Default fallback: constraint not recognized
+  def satisfies_constraint?(_tdd, %Constraint{kind: kind}) do
+    raise ArgumentError, "Unknown constraint kind: #{inspect(kind)}"
+  end
+
+  @doc """
+  Checks if a TDD is semantically a subtype of any of the specified kinds.
+  Used to approximate constraint satisfaction structurally.
+  """
+  def tdd_is_of_kind?(:any, _), do: true
+  def tdd_is_of_kind?(:none, _), do: false
+
+  def tdd_is_of_kind?(%TDD{decision: pred} = tdd, kinds) do
+    if pred in kinds do
+      # Decision directly confirms kind
+      tdd.yes != :none
+    else
+      # Otherwise we conservatively say "no" unless the TDD is union-like
+      false
+    end
+  end
+
+  # === Decision  ===
+  defmodule Decision do
+    @moduledoc """
+    A type-level decision predicate used in a TDD node.
+    """
+
+    @type t ::
+            :is_atom
+            | :is_integer
+            | :is_float
+            | :is_binary
+            | :is_list
+            | :is_tuple
+            | :is_map
+            # General "is a function"
+            | :is_function
+            | :is_pid
+            | :is_reference
+            | {:literal, term()}
+            | {:tuple_len, pos_integer()}
+            # Type of a map key (used in structural map checks)
+            | {:key, TDD.t()}
+            | {:has_struct_key, atom()}
+            # A type variable name, e.g., "~a"
+            | {:var, String.t()}
+            # New
+            | {:is_function_sig, param_types :: [TDD.t()], return_type :: TDD.t()}
+  end
+
+  @doc "Creates a TDD for a specific function signature"
+  def tdd_function_sig(param_types, return_type)
+      when is_list(param_types) and (is_struct(return_type, TDD) or return_type in [:any, :none]) do
+    %TDD{
+      decision: {:is_function_sig, param_types, return_type},
+      # A value matches if it's a function of this signature
+      yes: :any,
+      no: :none,
+      # Maybe it's some other function
+      maybe: %TDD{decision: :is_function, yes: :any, no: :none, maybe: :none}
+    }
+  end
+
+  # ... (existing tdd_or, tdd_and, tdd_not, tdd_diff) ...
+
+  @doc """
+  Performs type variable substitution in a TDD,
+  replacing variables found in the given `env` map (var_name -> TDD).
+  """
+  def tdd_substitute(:any, _env), do: :any
+  def tdd_substitute(:none, _env), do: :none
+
+  def tdd_substitute(%TDD{decision: {:var, name}} = tdd, env) when is_map(env) do
+    # If var 'name' is in env, substitute it. Otherwise, keep the var.
+    Map.get(env, name, tdd)
+  end
+
+  def tdd_substitute(%TDD{decision: {:is_function_sig, params, ret_type}} = tdd, env) do
+    # Substitute within the signature parts
+    substituted_params = Enum.map(params, &tdd_substitute(&1, env))
+    substituted_ret_type = tdd_substitute(ret_type, env)
+
+    # Reconstruct the TDD node, keeping yes/no/maybe branches as they are fixed for this predicate.
+    # Note: If canonicalization (mk_tdd) were used, this would go through it.
+    %TDD{tdd | decision: {:is_function_sig, substituted_params, substituted_ret_type}}
+  end
+
+  def tdd_substitute(%TDD{decision: {:key, key_type_tdd}} = tdd, env) do
+    # Substitute within the key type TDD
+    substituted_key_type = tdd_substitute(key_type_tdd, env)
+    %TDD{tdd | decision: {:key, substituted_key_type}}
+  end
+
+  # Generic case for other decisions: substitute in branches
+  def tdd_substitute(%TDD{} = tdd, env) do
+    %TDD{
+      # Assume decision itself doesn't contain substitutable vars unless handled above
+      decision: tdd.decision,
+      yes: tdd_substitute(tdd.yes, env),
+      no: tdd_substitute(tdd.no, env),
+      maybe: tdd_substitute(tdd.maybe, env)
+    }
+  end
+
+  @doc """
+  Performs substitution in a polymorphic type's body,
+  using the provided `env` (var_name -> TDD).
+  This substitutes *free* variables in the PolyTDD's body, not its quantified variables.
+  To instantiate quantified variables, use `Tilly.Inference.instantiate/3`.
+  """
+  def poly_substitute_free_vars(%PolyTDD{vars: _quantified_vars, body: body} = poly_tdd, env) do
+    # We only substitute variables in the body that are NOT the quantified ones.
+    # `env` should ideally not contain keys that are names of quantified variables of this PolyTDD.
+    # For simplicity, if env has a quantified var name, it will be shadowed by the quantified var itself.
+    # A more robust approach might filter env based on quantified_vars.
+    substituted_body = tdd_substitute(body, env)
+    %PolyTDD{poly_tdd | body: substituted_body}
+  end
+
+  @doc "Finds all free type variable names in a TDD."
+  def free_vars(:any), do: MapSet.new()
+  def free_vars(:none), do: MapSet.new()
+
+  def free_vars(%TDD{decision: {:var, name}}) do
+    MapSet.new([name])
+  end
+
+  def free_vars(%TDD{decision: {:is_function_sig, params, ret_type}}) do
+    param_fvs = Enum.map(params, &free_vars/1) |> Enum.reduce(MapSet.new(), &MapSet.union/2)
+    ret_fvs = free_vars(ret_type)
+    MapSet.union(param_fvs, ret_fvs)
+    # Note: yes/no/maybe branches for this node are typically :any/:none or simple predicates,
+    # but if they could contain vars, they'd need to be included.
+    # Current tdd_function_sig has fixed branches.
+  end
+
+  def free_vars(%TDD{decision: {:key, key_type_tdd}}) do
+    free_vars(key_type_tdd)
+    # Similar note about yes/no/maybe branches.
+  end
+
+  def free_vars(%TDD{yes: yes, no: no, maybe: maybe}) do
+    MapSet.union(free_vars(yes), MapSet.union(free_vars(no), free_vars(maybe)))
+  end
+
+  # Helper for PolyTDD free vars (vars free in body that are not quantified)
+  def free_vars_in_poly_tdd_body(%PolyTDD{vars: quantified_vars_list, body: body}) do
+    quantified_names = Enum.map(quantified_vars_list, & &1.name) |> MapSet.new()
+    body_fvs = free_vars(body)
+    MapSet.difference(body_fvs, quantified_names)
+  end
+end
+
+defmodule Tilly.Inference do
+  alias Tilly.Type
+  alias Tilly.Type.{TDD, Var, PolyTDD, Constraint}
+
+  @typedoc "Type environment: maps variable names (atoms) to their types (TDD or PolyTDD)"
+  @type type_env :: %{atom() => TDD.t() | PolyTDD.t()}
+
+  @typedoc "Substitution map: maps type variable names (strings) to TDDs"
+  @type substitution :: %{String.t() => TDD.t()}
+
+  @typedoc "Constraints collected during inference: {type_var_name, constraint}"
+  @type collected_constraints :: [{String.t(), Constraint.t()}]
+
+  @typedoc """
+  Result of inference for an expression:
+  - inferred_type: The TDD or PolyTDD type of the expression.
+  - var_counter: The updated counter for generating fresh type variables.
+  - substitution: The accumulated substitution map.
+  - constraints: Constraints that need to be satisfied.
+  """
+  @type infer_result ::
+          {inferred_type :: TDD.t() | PolyTDD.t(), var_counter :: non_neg_integer(),
+           substitution :: substitution(), constraints :: collected_constraints()}
+
+  # --- Helper for Fresh Type Variables ---
+  defmodule FreshVar do
+    @doc "Generates a new type variable name and increments the counter."
+    @spec next(non_neg_integer()) :: {String.t(), non_neg_integer()}
+    def next(counter) do
+      new_var_name = "~t" <> Integer.to_string(counter)
+      {new_var_name, counter + 1}
+    end
+  end
+
+  # --- Core Inference Function ---
+
+  @doc "Infers the type of a Tilly expression."
+  @spec infer(
+          expr :: term(),
+          env :: type_env(),
+          var_counter :: non_neg_integer(),
+          sub :: substitution()
+        ) ::
+          infer_result()
+  def infer({:lit, val}, _env, var_counter, sub) do
+    type =
+      cond do
+        # More precise: Type.tdd_literal(val)
+        is_atom(val) -> Type.tdd_pred(:is_atom)
+        # Type.tdd_literal(val)
+        is_integer(val) -> Type.tdd_pred(:is_integer)
+        # Type.tdd_literal(val)
+        is_float(val) -> Type.tdd_pred(:is_float)
+        # Type.tdd_literal(val)
+        is_binary(val) -> Type.tdd_pred(:is_binary)
+        # Add other literals as needed
+        # Fallback for other kinds of literals
+        true -> Type.tdd_literal(val)
+      end
+
+    {type, var_counter, sub, []}
+  end
+
+  def infer({:var, name}, env, var_counter, sub) when is_atom(name) do
+    case Map.get(env, name) do
+      nil ->
+        raise "Unbound variable: #{name}"
+
+      %TDD{} = tdd_type ->
+        {Type.tdd_substitute(tdd_type, sub), var_counter, sub, []}
+
+      %PolyTDD{} = poly_type ->
+        {instantiated_type, new_var_counter, new_constraints} =
+          instantiate(poly_type, var_counter)
+
+        # Apply current substitution to the instantiated type
+        # (in case fresh vars from instantiation are already in sub from elsewhere)
+        final_type = Type.tdd_substitute(instantiated_type, sub)
+        {final_type, new_var_counter, sub, new_constraints}
+    end
+  end
+
+  def infer({:fn, param_atoms, body_expr}, env, var_counter, sub) when is_list(param_atoms) do
+    # 1. Create fresh type variables for parameters
+    {param_tdd_vars, extended_env, counter_after_params} =
+      Enum.reduce(param_atoms, {[], env, var_counter}, fn param_name,
+                                                          {vars_acc, env_acc, c_acc} ->
+        {fresh_var_name, next_c} = FreshVar.next(c_acc)
+        param_tdd_var = Type.tdd_var(fresh_var_name)
+        {[param_tdd_var | vars_acc], Map.put(env_acc, param_name, param_tdd_var), next_c}
+      end)
+
+    param_types = Enum.reverse(param_tdd_vars)
+
+    # 2. Infer body with extended environment and current substitution
+    {body_type_raw, counter_after_body, sub_after_body, body_constraints} =
+      infer(body_expr, extended_env, counter_after_params, sub)
+
+    # 3. Apply the substitution from body inference to parameter types
+    #    This is because unification within the body might refine what the param types can be.
+    final_param_types = Enum.map(param_types, &Type.tdd_substitute(&1, sub_after_body))
+    # Already applied in infer usually
+    final_body_type = Type.tdd_substitute(body_type_raw, sub_after_body)
+
+    # 4. Construct function type
+    fun_type = Type.tdd_function_sig(final_param_types, final_body_type)
+    {fun_type, counter_after_body, sub_after_body, body_constraints}
+  end
+
+  def infer({:app, fun_expr, arg_exprs}, env, var_counter, sub) when is_list(arg_exprs) do
+    # 1. Infer function expression
+    {fun_type_raw, c1, s1, fun_constraints} = infer(fun_expr, env, var_counter, sub)
+    # Apply substitutions so far
+    fun_type_template = Type.tdd_substitute(fun_type_raw, s1)
+
+    # 2. Infer argument expressions
+    {arg_types_raw, c2, s2, args_constraints_lists} =
+      Enum.map_reduce(arg_exprs, {c1, s1}, fn arg_expr, {c_acc, s_acc} ->
+        {arg_t, next_c, next_s, arg_c} = infer(arg_expr, env, c_acc, s_acc)
+        # Pass along type and its constraints
+        {{arg_t, arg_c}, {next_c, next_s}}
+      end)
+
+    actual_arg_types = Enum.map(arg_types_raw, fn {t, _cs} -> Type.tdd_substitute(t, s2) end)
+    all_arg_constraints = Enum.flat_map(arg_types_raw, fn {_t, cs} -> cs end) ++ fun_constraints
+
+    # 3. Unify/Match function type with arguments
+    #    `fun_type_template` is the type of the function (e.g., {:var, "~f"} or an actual fn_sig)
+    #    `s2` is the current global substitution.
+    {return_type_final, c3, s3, unification_constraints} =
+      unify_apply(fun_type_template, actual_arg_types, c2, s2)
+
+    {return_type_final, c3, s3, all_arg_constraints ++ unification_constraints}
+  end
+
+  def infer({:let, [{var_name, val_expr}], body_expr}, env, var_counter, sub) do
+    # 1. Infer the type of the value expression
+    {val_type_raw, c1, s1, val_constraints} = infer(val_expr, env, var_counter, sub)
+
+    # 2. Apply current substitution and generalize the value's type
+    #    Generalization happens *before* adding to env, over variables free in val_type but not env.
+    #    The substitution `s1` contains all refinements up to this point.
+    val_type_substituted = Type.tdd_substitute(val_type_raw, s1)
+    generalized_val_type = generalize(val_type_substituted, env, s1)
+
+    # 3. Extend environment and infer body
+    extended_env = Map.put(env, var_name, generalized_val_type)
+    # Use s1 for body too
+    {body_type_raw, c2, s2, body_constraints} = infer(body_expr, extended_env, c1, s1)
+
+    # The final substitution s2 incorporates s1 and any changes from body.
+    # The final body_type is already substituted by s2.
+    {body_type_raw, c2, s2, val_constraints ++ body_constraints}
+  end
+
+  # --- Polymorphism: Instantiation and Generalization ---
+
+  @doc "Instantiates a polymorphic type scheme by replacing quantified variables with fresh ones."
+  def instantiate(%PolyTDD{vars: poly_vars_list, body: body_tdd}, var_counter) do
+    # Create substitution map from quantified vars to fresh vars
+    {substitution_to_fresh, new_var_counter, new_constraints} =
+      Enum.reduce(poly_vars_list, {%{}, var_counter, []}, fn %Var{
+                                                               name: q_name,
+                                                               constraints: q_constraints
+                                                             },
+                                                             {sub_acc, c_acc, cons_acc} ->
+        {fresh_name, next_c} = FreshVar.next(c_acc)
+        fresh_tdd_var = Type.tdd_var(fresh_name)
+        # Associate constraints of the quantified var with the new fresh var
+        # Tie constraint to fresh var name
+        fresh_var_constraints = Enum.map(q_constraints, &%Constraint{&1 | arg: fresh_name})
+        {Map.put(sub_acc, q_name, fresh_tdd_var), next_c, cons_acc ++ fresh_var_constraints}
+      end)
+
+    instantiated_body = Type.tdd_substitute(body_tdd, substitution_to_fresh)
+    {instantiated_body, new_var_counter, new_constraints}
+  end
+
+  @doc "Generalizes a TDD type into a PolyTDD if it has free variables not in the environment."
+  def generalize(type_tdd, env, current_sub) do
+    # Apply current substitution to resolve any vars in type_tdd that are already determined
+    type_to_generalize = Type.tdd_substitute(type_tdd, current_sub)
+
+    env_free_vars =
+      env
+      |> Map.values()
+      |> Enum.map(&apply_sub_and_get_free_vars(&1, current_sub))
+      |> Enum.reduce(MapSet.new(), &MapSet.union/2)
+
+    type_free_vars_set = Type.free_vars(type_to_generalize)
+
+    vars_to_quantify_names = MapSet.difference(type_free_vars_set, env_free_vars)
+
+    if MapSet.size(vars_to_quantify_names) == 0 do
+      # No variables to quantify, return as is
+      type_to_generalize
+    else
+      quantified_vars_structs =
+        Enum.map(MapSet.to_list(vars_to_quantify_names), fn var_name ->
+          # For now, generalized variables have no attached constraints here.
+          # Constraints arise from usage and are checked later.
+          %Var{name: var_name, constraints: []}
+        end)
+
+      %PolyTDD{vars: quantified_vars_structs, body: type_to_generalize}
+    end
+  end
+
+  defp apply_sub_and_get_free_vars(%TDD{} = tdd, sub) do
+    Type.tdd_substitute(tdd, sub) |> Type.free_vars()
+  end
+
+  defp apply_sub_and_get_free_vars(%PolyTDD{} = poly_tdd, sub) do
+    # For a PolyTDD in the env, we care about its free variables *after* substitution,
+    # excluding its own quantified variables.
+    # Substitutes free vars in body
+    Type.poly_substitute_free_vars(poly_tdd, sub)
+    |> Type.free_vars_in_poly_tdd_body()
+  end
+
+  # --- Unification (Simplified for now) ---
+
+  @doc """
+  Constrains variables in t1 and t2 to be compatible and updates the substitution.
+  If t1 is Var(~a) and t2 is Type T, then ~a's bound becomes current_bound(~a) & T.
+  If t1 and t2 are concrete, checks their intersection isn't None.
+  Returns new substitution. Throws on error.
+  """
+  def constrain_and_update_sub(raw_t1, raw_t2, sub) do
+    # IO.inspect({:constrain_start, raw_t1, raw_t2, sub}, label: "CONSTRAIN")
+    t1 = tdd_substitute(raw_t1, sub)
+    t2 = tdd_substitute(raw_t2, sub)
+    # IO.inspect({:constrain_applied, t1, t2}, label: "CONSTRAIN")
+
+    cond do
+      # Identical or one is Any (Any & T = T, so effectively no new constraint on T if T is a var already refined from Any)
+      t1 == t2 ->
+        sub
+
+      # Effectively constrains t2 if it's a var
+      t1 == Type.tdd_any() ->
+        constrain_var_with_type(t2, t1, sub)
+
+      # Effectively constrains t1 if it's a var
+      t2 == Type.tdd_any() ->
+        constrain_var_with_type(t1, t2, sub)
+
+      # Case 1: t1 is a variable
+      %TDD{decision: {:var, v_name1}} = t1 ->
+        update_var_bound(v_name1, t2, sub, raw_t1, raw_t2)
+
+      # Case 2: t2 is a variable (and t1 is not)
+      %TDD{decision: {:var, v_name2}} = t2 ->
+        # Note order for error message
+        update_var_bound(v_name2, t1, sub, raw_t2, raw_t1)
+
+      # Case 3: Both are function signatures (concrete)
+      %TDD{decision: {:is_function_sig, params1, ret1}} = t1,
+      %TDD{decision: {:is_function_sig, params2, ret2}} = t2 ->
+        if length(params1) != length(params2) do
+          raise "Type error (constrain): Function arity mismatch between #{inspect(t1)} and #{inspect(t2)}"
+        end
+
+        # For two function *types* to be compatible/substitutable, their parameters are contravariant, return is covariant.
+        # However, if we are "unifying" them to be *the same type structure*, then params are covariant.
+        # Let's assume for now `constrain_and_update_sub` implies they should be "equal or compatible via intersection".
+        # This means their intersection should be non-None, and vars within them get constrained.
+
+        sub_after_params =
+          Enum.zip(params1, params2)
+          |> Enum.reduce(sub, fn {p1, p2}, acc_sub ->
+            # Params are "unified" directly
+            constrain_and_update_sub(p1, p2, acc_sub)
+          end)
+
+        # Return types are "unified" directly
+        constrain_and_update_sub(ret1, ret2, sub_after_params)
+
+      # TODO: Add cases for Tuples, Lists, TDDMap
+      # For tuples: length must match, then constrain_and_update_sub elements pairwise.
+      # %TDD{decision: {:is_tuple, len1}, yes: elements_tdd1} ...
+      # This requires TDDs to encode tuple elements more directly if we want to unify structurally.
+      # Current TDD for tuple is just {:tuple_len, N} or general :is_tuple. We need richer TDDs for structural unification.
+      # For now, this fallback will handle simple tuple predicates.
+
+      # Case 4: Other concrete types.
+      true ->
+        intersection = tdd_and(t1, t2)
+
+        if intersection == Type.tdd_none() do
+          raise "Type error (constrain): Types #{inspect(t1)} (from #{inspect(raw_t1)}) and #{inspect(t2)} (from #{inspect(raw_t2)}) are incompatible (intersection is empty). Current sub: #{inspect(sub)}"
+        end
+
+        # If they are concrete and compatible, `sub` is unchanged at this level.
+        sub
+    end
+
+    defp constrain_var_with_type(%TDD{decision: {:var, v_name}} = var_tdd, other_type, sub) do
+      # raw_t1, raw_t2 are for error msg context
+      update_var_bound(v_name, other_type, sub, var_tdd, other_type)
+    end
+
+    # No var, no sub change here
+    defp constrain_var_with_type(_concrete_type, _other_type, sub), do: sub
+
+    defp update_var_bound(v_name, constraining_type, sub, raw_var_form, raw_constraining_form) do
+      # Default to Any
+      current_bound_v = Map.get(sub, v_name, Type.tdd_any())
+      new_bound_v = Type.tdd_and(current_bound_v, constraining_type)
+
+      if new_bound_v == Type.tdd_none() do
+        original_var_constraint_str =
+          if raw_var_form != constraining_type,
+            do: "(from unifying with #{inspect(raw_constraining_form)})",
+            else: ""
+
+        raise "Type error: Constraining variable #{v_name} with #{inspect(constraining_type)} #{original_var_constraint_str} results in an empty type. Previous bound: #{inspect(current_bound_v)}. Current sub: #{inspect(sub)}"
+      end
+
+      Map.put(sub, v_name, new_bound_v)
+    end
+
+    @doc """
+    Handles the application of a function type to actual argument types.
+    `fun_type_template` is the (possibly variable) type of the function.
+    `actual_arg_types` are the TDDs of the arguments.
+    `var_counter` and `sub` are current state.
+    Returns `{final_return_type, new_counter, new_sub, new_constraints}`.
+    """
+    def unify_apply(fun_type_template, actual_arg_types, var_counter, sub) do
+      # Apply current substitutions to fun_type_template
+      current_fun_type = Type.tdd_substitute(fun_type_template, sub)
+
+      case current_fun_type do
+        %TDD{decision: {:var, fun_var_name}} ->
+          # Function is a type variable. We need to unify it with a newly minted function signature.
+          {param_var_tds, c1} =
+            Enum.map_reduce(actual_arg_types, var_counter, fn _arg, c_acc ->
+              {fresh_name, next_c} = FreshVar.next(c_acc)
+              {Type.tdd_var(fresh_name), next_c}
+            end)
+
+          {return_var_name, c2} = FreshVar.next(c1)
+          return_var_tdd = Type.tdd_var(return_var_name)
+
+          # The new signature that fun_var_name must conform to
+          synthetic_fun_sig_tdd = Type.tdd_function_sig(param_var_tds, return_var_tdd)
+
+          # Unify the function variable with this synthetic signature
+          {s1, cons1} = unify(current_fun_type, synthetic_fun_sig_tdd, sub)
+
+          # Now unify actual arguments with the fresh parameter type variables
+          {s2, cons2_list} =
+            Enum.zip(actual_arg_types, param_var_tds)
+            |> Enum.reduce({s1, []}, fn {actual_arg_t, param_var_t}, {s_acc, c_acc_list} ->
+              {next_s, next_cs} = unify(actual_arg_t, param_var_t, s_acc)
+              {next_s, [next_cs | c_acc_list]}
+            end)
+
+          final_return_type = Type.tdd_substitute(return_var_tdd, s2)
+          {final_return_type, c2, s2, cons1 ++ List.flatten(cons2_list)}
+
+        %TDD{decision: {:is_function_sig, expected_param_types, expected_return_type}} ->
+          # Function is a known signature.
+          if length(actual_arg_types) != length(expected_param_types) do
+            raise "Arity mismatch: expected #{length(expected_param_types)}, got #{length(actual_arg_types)}"
+          end
+
+          # Unify actual arguments with expected parameter types
+          {s1, constraints_from_params_list} =
+            Enum.zip(actual_arg_types, expected_param_types)
+            |> Enum.reduce({sub, []}, fn {actual_arg_t, expected_param_t}, {s_acc, c_acc_list} ->
+              {next_s, param_cs} = unify(actual_arg_t, expected_param_t, s_acc)
+              {next_s, [param_cs | c_acc_list]}
+            end)
+
+          final_return_type = Type.tdd_substitute(expected_return_type, s1)
+          {final_return_type, var_counter, s1, List.flatten(constraints_from_params_list)}
+
+        other_type ->
+          raise "Type error: expected a function, but got #{inspect(other_type)}"
+      end
+    end
+
+    @doc "Top-level type checking function for a Tilly program (list of expressions)."
+    def typecheck_program(exprs, initial_env \\ %{}) do
+      # For a program, we can infer each top-level expression.
+      # For `def`s, they would add to the environment.
+      # For now, let's just infer a single expression.
+      # A real program would involve modules, defs, etc.
+      initial_var_counter = 0
+      initial_substitution = %{}
+
+      # This is a simplified entry point, inferring a single expression
+      # A full program checker would iterate, manage top-level defs, etc.
+      if is_list(exprs) and Enum.count(exprs) == 1 do
+        [main_expr] = exprs
+
+        {raw_type, _counter, final_sub, constraints} =
+          infer(main_expr, initial_env, initial_var_counter, initial_substitution)
+
+        final_type = Type.tdd_substitute(raw_type, final_sub)
+        # Here, you would solve/check `constraints` using `final_sub`
+        # For example:
+        Enum.each(constraints, fn {var_name, constraint_obj} ->
+          var_final_type = Map.get(final_sub, var_name, Type.tdd_var(var_name))
+
+          unless Type.satisfies_constraint?(var_final_type, constraint_obj) do
+            raise "Constraint #{inspect(constraint_obj)} not satisfied for #{var_name} (type #{inspect(var_final_type)})"
+          end
+        end)
+
+        {:ok, final_type, final_sub}
+      else
+        # Placeholder for multi-expression program handling
+        {:error, "Program must be a single expression for now"}
+      end
+    end
+  end
+end