818 lines
30 KiB
Elixir
818 lines
30 KiB
Elixir
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
|