Checks if recursive constraint solving has converged.

Convergence is determined by comparing the change in substitutions between iterations.

Arguments

• OldSubst - Previous substitution
• NewSubst - Current substitution
• RecState - Recursive inference state with convergence threshold

Returns

• {converged, FinalSubst} - If convergence achieved
• {not_converged, MergedSubst} - If more iterations needed

Extends a type environment with a new variable binding.

Supports multiple environment representations for different use cases.

Arguments

• Env - Type environment (type_env(), map(), or list())
• Var - Variable name (atom())
• Type - Type expression to bind to the variable

Returns

• Updated environment with the new binding

Supported Environment Types

• type_env(): Full environment with constraints and parent scopes
• map(): Simple map for lightweight inference
• list(): Association list for basic scoping

Example

Env1 = cure_types:new_env(),
Env2 = cure_types:extend_env(Env1, x, {primitive_type, 'Int'}),
Env3 = cure_types:extend_env(Env2, y, {primitive_type, 'String'}).

Extract type parameter names from a list that may contain atoms or records.

Arguments

• TypeParams - List of atoms or #type_param_decl{} records

Returns

List of type parameter name atoms

Find all free type variables in a type.

Arguments

• Type - Type expression to analyze

Returns

Set of type variable names/ids that appear free in the type

Find all free type variables in a type environment.

Arguments

• Env - Type environment

Returns

Set of type variable names/ids that appear free in any type in the environment

Create fresh type variables for a list of type parameters.

Arguments

• TypeParams - List of type parameter atoms or #type_param_decl{} records

Returns

A map from type parameter names to fresh type variables

Example

FreshVars = fresh_type_vars_for_params(['T', 'U']).
% Result: #{'T' => TypeVar1, 'U' => TypeVar2}

Generalize a type by quantifying over free type variables.

Implements Hindley-Milner let-polymorphism by creating a poly_type that quantifies over type variables that are free in the type but not free in the environment.

Arguments

• Type - Type to generalize
• Env - Current type environment

Returns

Either a poly_type (if there are free type variables) or the original type

Example

% Type: T -> T where T is free
% Env: {x: Int}
% Result: forall T. T -> T
Type = {function_type, [TypeVar], TypeVar},
Generalized = generalize_type(Type, Env).

Performs type inference for recursive function calls with dependent type tracking.

This is the main entry point for recursive function call type inference that properly handles dependent types across recursive boundaries.

Arguments

• FunctionName - Name of the recursive function
• Args - Argument expressions
• Env - Type environment
• RecState - Recursive inference state

Returns

• {ok, ResultType, Constraints, UpdatedState} - Successful inference
• {error, Reason} - Type inference failure

Features

• Dependent Type Tracking: Maintains dependent relationships across calls
• Fixed-Point Computation: Iterates until type constraints converge
• Constraint Propagation: Propagates constraints between recursive levels
• Cycle Detection: Prevents infinite recursion in type inference

Instantiate a poly_type record with fresh type variables.

Handles the poly_type AST record which explicitly represents polymorphic types with forall quantification.

Arguments

• PolyType - A #poly_type{} record

Returns

The instantiated body type with fresh type variables

Instantiate a poly_type record with provided type arguments.

Handles explicit type application where concrete types are provided for type parameters (e.g., id<Int> applies Int to identity function).

Arguments

• PolyType - A #poly_type{} record
• TypeArgs - List of concrete types to substitute for type parameters

Returns

The instantiated body type with type arguments substituted

Instantiate a polymorphic type with fresh type variables.

Given a type with type parameters (e.g., forall T. T -> T), creates a new type with fresh type variables replacing all type parameters.

Arguments

• Type - The polymorphic type to instantiate
• TypeParams - List of type parameter names to instantiate (e.g., ['T', 'U'])

Returns

The instantiated type with fresh type variables

Example

PolyType = {function_type, [{primitive_type, 'T'}], {primitive_type, 'T'}},
InstType = instantiate_polymorphic_type(PolyType, ['T']).
% Result: {function_type, [TypeVar1], TypeVar1} where TypeVar1 is fresh

Instantiate a polymorphic type if needed, handling both poly_type and regular types.

This is the main entry point for type instantiation during inference. It handles:

• poly_type records: Instantiates with fresh type variables
• Regular function types: Uses existing instantiate_type_if_function
• Other types: Returns as-is

Arguments

• Type - Any type expression

Returns

Instantiated type with fresh type variables for polymorphic types

Checks if a type expression represents the Nat type.

Recognizes both the algebraic Nat type (union type with Zero/Succ) and the refined Nat type (non-negative integers).

Arguments

• Type - Type expression to check

Returns

• true - If the type is Nat or Nat-related
• false - Otherwise

Example

true = cure_types:is_nat_type({primitive_type, 'Nat'}),
true = cure_types:is_nat_type({union_type, 'Nat', _, _}),
true = cure_types:is_nat_type({refined_type, 'Int', ...}).

Checks if a term is a type variable.

Arguments

• Term - Any term to check

Returns

• true - If the term is a type_var record
• false - Otherwise

Example

TVar = cure_types:new_type_var(),
true = cure_types:is_type_var(TVar),
false = cure_types:is_type_var(my_atom).

Looks up a variable binding in the type environment.

Searches the current environment and parent environments if available.

Arguments

• Env - Type environment (type_env(), map(), or list())
• Var - Variable name to look up (atom())

Returns

• Type - The type bound to the variable if found
• undefined - If the variable is not bound in the environment

Scoping

For type_env() records, searches parent environments if the variable is not found in the current scope.

Example

Env = cure_types:extend_env(cure_types:new_env(), x, IntType),
IntType = cure_types:lookup_env(Env, x),
undefined = cure_types:lookup_env(Env, unbound_var).

Converts an Erlang integer to Peano-encoded Nat.

Creates a chain of Succ constructors wrapping Zero, representing the given non-negative integer.

Arguments

• N - Non-negative integer

Returns

• {ok, NatExpr} - Peano-encoded natural number
• {error, negative_integer} - If N < 0

Example

{ok, Three} = cure_types:nat_from_int(3),
%% Results in Succ(Succ(Succ(Zero)))

Constructs the successor of a natural number.

In Peano encoding, Succ(n) represents n+1, similar to Idris's S constructor.

Arguments

• Nat - A natural number expression

Returns

• An expression representing Succ(Nat) : Nat

Example

One = cure_types:nat_succ(cure_types:nat_zero()),
Two = cure_types:nat_succ(One),
%% Results in Succ(Succ(Zero))

Converts a Peano-encoded Nat to an Erlang integer.

Unwraps the chain of Succ constructors to compute the integer value.

Arguments

• NatExpr - Peano-encoded natural number expression

Returns

• {ok, Integer} - The integer value
• {error, invalid_nat} - If not a valid Nat expression

Example

{ok, Three} = cure_types:nat_from_int(3),
{ok, 3} = cure_types:nat_to_int(Three).

Constructs the Zero value of the Nat type.

In Peano encoding, Zero is the base case for natural numbers, similar to Idris's Z constructor.

Returns

• An expression representing Zero : Nat

Example

Zero = cure_types:nat_zero(),
%% Results in an identifier expression representing Zero

Creates a new empty type environment.

The type environment maintains variable bindings, constraints, and supports hierarchical scoping through parent environments.

Returns

• type_env() - A new empty type environment

Example

Env = cure_types:new_env(),
Env2 = cure_types:extend_env(Env, x, {primitive_type, 'Int'}),
{ok, Type} = cure_types:lookup_env(Env2, x).

Features

• Hierarchical Scoping: Supports nested environments
• Constraint Tracking: Accumulates type constraints
• Efficient Lookup: Fast variable resolution

Creates a new recursive inference state for tracking recursive function calls.

Returns

• recursive_inference_state() - New state with empty call stack

Example

State = cure_types:new_recursive_state(),
UpdatedState = cure_types:push_recursive_call(factorial, ParamTypes, RetType, State).

Creates a new unique type variable without a specific name.

This is a convenience function that calls new_type_var/1 with undefined name.

Returns

• type_var() - A new unique type variable

Example

TVar = cure_types:new_type_var(),
true = cure_types:is_type_var(TVar).

Note

Uses a process dictionary counter to ensure uniqueness within a process. For concurrent use, external synchronization may be required.

Creates a new unique type variable with an optional name.

Arguments

• Name - Optional name for the type variable (atom() | undefined)

Returns

• type_var() - A new unique type variable with the given name

Example

TVar1 = cure_types:new_type_var(my_var),
TVar2 = cure_types:new_type_var(undefined),
true = TVar1#type_var.name =:= my_var.

Note

The name is primarily for debugging and error reporting. The unique ID ensures type variable identity regardless of name.

Performs an occurs check to prevent infinite types during unification.

The occurs check ensures that a type variable does not occur within the type it would be unified with, preventing infinite type structures.

Arguments

• TypeVar - Type variable to check for
• Type - Type expression to check within

Returns

• true - If the type variable occurs in the type (would create infinite type)
• false - If the unification would be safe

Example

TVar = cure_types:new_type_var(),
ListType = {list_type, TVar},
true = cure_types:occurs_check(TVar, ListType),  % Would create infinite list
false = cure_types:occurs_check(TVar, {primitive_type, 'Int'}).

Note

This is essential for preventing infinite types like T = List(T) during unification.

Pops a recursive function call context from the call stack.

Arguments

• State - Current recursive inference state

Returns

• {ok, Context, NewState} - Popped context and updated state
• {error, empty_stack} - If the call stack is empty

Pushes a recursive function call context onto the call stack.

This tracks recursive calls to enable proper dependent type handling across recursive boundaries.

Arguments

• FunctionName - Name of the function being called recursively
• ParameterTypes - Types of the parameters in this call
• ReturnType - Expected return type of the function
• State - Current recursive inference state

Returns

• {ok, NewState} - Updated state with the call pushed
• {error, Reason} - If maximum recursion depth exceeded

Example

{ok, NewState} = cure_types:push_recursive_call(
    factorial, [NType], FactorialRetType, State
).

Solves recursive type constraints using fixed-point computation.

This function iteratively refines type constraints until they converge, handling dependent types that may change across recursive calls.

Arguments

• Constraints - List of type constraints to solve
• RecState - Recursive inference state

Returns

• {ok, Substitution, Iterations} - Converged solution
• {error, Reason} - If convergence fails or max iterations exceeded

Algorithm

1. Apply current substitution to constraints
2. Solve constraints to get new substitution
3. Check for convergence by comparing substitutions
4. Repeat until convergence or max iterations reached

Tracks dependent constraints within recursive function calls.

This function maintains the relationships between dependent types across recursive call boundaries, ensuring type safety.

Arguments

• Constraints - Type constraints from the current call
• Context - Recursive call context
• RecState - Current recursive inference state

Returns

• {ok, TrackedConstraints, UpdatedState} - Success with tracked constraints
• {error, Reason} - If constraint tracking fails

Unifies two types using the Robinson unification algorithm.

This is a convenience function that calls unify/3 with an empty substitution.

Arguments

• Type1 - First type expression to unify
• Type2 - Second type expression to unify

Returns

• {ok, Substitution} - Successful unification with substitution map
• {error, Reason} - Unification failure with detailed error

Example

{ok, Subst} = cure_types:unify(IntType, IntType),
{ok, Subst2} = cure_types:unify(TVar, IntType),
{error, _} = cure_types:unify(IntType, StringType).

Error Cases

• Type mismatch (e.g., Int vs String)
• Occurs check failure (infinite types)
• Constraint violations

Unifies two types with an existing substitution.

Applies the existing substitution to both types before unification and composes the results.

Arguments

• Type1 - First type expression to unify
• Type2 - Second type expression to unify
• Subst - Existing substitution map to compose with

Returns

• {ok, NewSubstitution} - Combined substitution after unification
• {error, Reason} - Unification failure with detailed error

Example

{ok, Subst1} = cure_types:unify(TVar1, IntType),
{ok, Subst2} = cure_types:unify(TVar2, StringType, Subst1),
%% Subst2 now contains bindings for both TVar1 and TVar2

Substitution Composition

The function applies the input substitution to both types before unification and composes the result with the input substitution.

Performs unification with recursive context tracking.

This extends the standard unification algorithm to properly handle type variables and dependent types across recursive call boundaries.

Arguments

• Types1 - First set of types to unify
• Types2 - Second set of types to unify
• Context - Recursive call context
• RecState - Recursive inference state

Returns

• {ok, Constraints, UpdatedState} - Successful unification with constraints
• {error, Reason} - Unification failure