From 0629bbadbd9e2ce9b56dcc6b01c8bb29530d3df1 Mon Sep 17 00:00:00 2001 From: Kacper Marzecki Date: Sun, 15 Jun 2025 11:53:15 +0200 Subject: [PATCH] checkpoint discussion --- .aider.chat.history.md | 17 + .aider.input.history | 6 + lib/til/tdd.ex | 51 +++ lib/til/type.ex | 817 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 891 insertions(+) create mode 100644 lib/til/tdd.ex create mode 100644 lib/til/type.ex diff --git a/.aider.chat.history.md b/.aider.chat.history.md index e80c7df..1cce221 100644 --- a/.aider.chat.history.md +++ b/.aider.chat.history.md @@ -56997,3 +56997,20 @@ 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. diff --git a/.aider.input.history b/.aider.input.history index 419b26d..1b67915 100644 --- a/.aider.input.history +++ b/.aider.input.history @@ -4158,3 +4158,9 @@ # 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 diff --git a/lib/til/tdd.ex b/lib/til/tdd.ex new file mode 100644 index 0000000..c08dfcb --- /dev/null +++ b/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 diff --git a/lib/til/type.ex b/lib/til/type.ex new file mode 100644 index 0000000..3b14ad9 --- /dev/null +++ b/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