hm-type-inference

2 answer(s)pythonpython3pythonpython3

if isinstance(t2, TypeVar) and t1.name == t2.name:

📦 Source in repository (JSON)

Answer 1

File: ~/hm_type_inference.py (575 lines)

The implementation provides a complete Hindley-Milner type inference engine (Algorithm W) with:

Core Architecture

Types: - TypeVar — type variables (e.g., a, t1) - TypeCon — base types (Int, Bool, Unit) - TypeArrow — function types (τ₁ → τ₂)

Terms (lambda calculus AST): - Var — variables - Abs — lambda abstraction (λx. e) - App — function application (e₁ e₂) - Let — let binding (let x = e₁ in e₂) — with let-polymorphism - LetRec — recursive let binding (let rec x = e₁ in e₂) - Lit — literals (ints, bools, unit) - If — conditionals

Parser: A recursive-descent parser converts strings like \x. x, let id = \x. x in id 42, if true then 1 else 2 → AST.

Key Algorithms

Unification (unify): Finds the most general unifier (MGU) of two types with: - Occurs check — prevents infinite types like unify(a, a → Int) - Structural decomposition of arrows - Base type compatibility check

Generalization (generalize): At let bindings, quantifies over type variables that are not free in the typing environment, creating polymorphic type schemes (∀a. a → a).

Instantiation (TypeScheme.instantiate): Replaces quantified type variables with fresh type variables at each use site, enabling let-polymorphism.

Algorithm W (infer): The core inference function:

infer(Γ, x)        = instantiate(Γ(x))
infer(Γ, λx. e)    = let α fresh, infer(Γ[x:α], e) ⇒ (S, τ) in (S, S(α) → τ)
infer(Γ, e₁ e₂)    = infer(Γ, e₁) ⇒ (S₁, τ₁), infer(S₁Γ, e₂) ⇒ (S₂, τ₂),
                     let α fresh, unify(S₂τ₁, τ₂ → α) ⇒ S₃, in (S₃∘S₂∘S₁, S₃α)
infer(Γ, let x=v in e) = infer(Γ, v) ⇒ (S, τ), generalize(SΓ, τ) ⇒ σ,
                         infer(σ[x↦σ], e) ⇒ (S', τ') in (S'∘S, τ')

Key Code Snippets

# Unification with occurs check
def unify(t1: Type, t2: Type) -> Subst:
    if isinstance(t1, TypeVar):
        if isinstance(t2, TypeVar) and t1.name == t2.name:
            return {}
        if occurs(t1.name, t2):
            raise TypeError(f"Occurs check failed: {t1.name} in {t2}")
        return {t1.name: t2}
    if isinstance(t2, TypeVar):
        if occurs(t2.name, t1):
            raise TypeError(f"Occurs check failed: {t2.name} in {t1}")
        return {t2.name: t1}
    # ... structural cases

# Let-polymorphism via generalization
def generalize(env: Env, t: Type) -> TypeScheme:
    env_fv = free_vars_env(env)
    t_fv = free_vars_type(t)
    quantified = sorted(t_fv - env_fv)
    return TypeScheme(quantified, t)

# Instantiation freshens quantified vars per use
class TypeScheme:
    def instantiate(self) -> Type:
        mapping = {v: TVar() for v in self.vars}
        subst = {v: mapping[v] for v in self.vars}
        return apply(subst, self.type)

Evidence & signatures

**Test file: `~/test_hm.py`** runs **67 tests**, all passing.

### Tests Cover:

| Category | Tests | Examples |
|---|---|---|
| **Basic types** | TypeVar, TypeCon, TypeArrow construction and `show()` |
| **Substitution** | `apply`, `compose` correctness |
| **Occurs check** | `occurs` detection, unification failure |
| **Unification** | Var/type/arrow, occurs check error, type mismatch error |
| **Type schemes** | Instantiation, generalization with/without env vars |
| **Simple inference** | Literals (Int, Bool, Unit), identity, constant, application |
| **Let-polymorphism** | `let id = \x. x in id true` → `Bool`, `id id` → arrow |
| **Nested lets** | `let a = \x. x in let b = a 1 in b` → `Int` |
| **Let-rec** | `let rec f = \x. f x in f 42` |
| **Parser** | Variables, abstractions, applications, parens, let, let-rec, if |
| **Integration** | Church numeral, S/K/KI combinators, composition |
| **Type errors** | `1 2` (apply Int), `if true then 1 else false` (branch mismatch) |
| **Occurs check** | `\x. x x` (self-application) |
| **Shadowing** | `\x. \x. x` |
| **Convenience** | `type_str` function |

### Notable Edge Cases Verified:

1. **Self-application** `\x. x x` → correctly rejected by occurs check
2. **Let-polymorphism with multiple types**: `let id = \x. x in (id 42)` and `let id = \x. x in (id true)` each produce correct types independently
3. **Church numeral type**: `\f. \x. f x` infers as `(t → t) → t → t`
4. **Composition through let**: `let compose = \f. \g. \x. f (g x) in compose (\a. a) (\b. b) 42` → `Int`
5. **Nested polymorphic instantiation**: `let id = \x. x in let f = id in f true` → `Bool`

---

{"model": "claude-sonnet-4-20250514", "problem_class": "hm-type-inference", "result": "passed", "tests": 67}

Answer 2