type-checker Skill

"Catch errors before they run. Types are theorems, programs are proofs."

Overview

Type Checker implements bidirectional type checking for dependent types. Validates that programs are well-typed before execution, catching errors at compile time.

GF(3) Role

Bidirectional Type Checking

┌─────────────────────────────────────────────────────────────────┐
│                  BIDIRECTIONAL TYPING                           │
├─────────────────────────────────────────────────────────────────┤
│                                                                 │
│  Check Mode (⇐):             Infer Mode (⇒):                   │
│  "Does term have type?"      "What type does term have?"       │
│                                                                 │
│  Γ ⊢ e ⇐ A                   Γ ⊢ e ⇒ A                        │
│                                                                 │
│  Used for:                   Used for:                         │
│  - Lambda abstractions       - Variables                       │
│  - Match expressions         - Applications                    │
│  - Holes                     - Annotated terms                 │
│                                                                 │
└─────────────────────────────────────────────────────────────────┘

Core Algorithm

class TypeChecker:
    """Bidirectional type checker with dependent types."""

    TRIT = -1  # VALIDATOR role

    def check(self, ctx: Context, term: Term, expected: Type) -> bool:
        """
        Check mode: verify term has expected type.
        """
        match term:
            case Lam(x, body):
                # For λx.body, expected must be Π(x:A).B
                match expected:
                    case Pi(_, a, b):
                        # Check body in extended context
                        return self.check(ctx.extend(x, a), body, b)
                    case _:
                        return False

            case Hole(name):
                # Record constraint for hole
                self.add_constraint(name, expected)
                return True

            case _:
                # Fall back to infer and compare
                inferred = self.infer(ctx, term)
                return self.equal(ctx, inferred, expected)

    def infer(self, ctx: Context, term: Term) -> Type:
        """
        Infer mode: synthesize type from term.
        """
        match term:
            case Var(x):
                return ctx.lookup(x)

            case App(func, arg):
                func_type = self.infer(ctx, func)
                match func_type:
                    case Pi(x, a, b):
                        self.check(ctx, arg, a)
                        return self.subst(b, x, arg)
                    case _:
                        raise TypeError(f"Expected function, got {func_type}")

            case Ann(term, typ):
                # Annotation: (term : type)
                self.check(ctx, typ, Type())
                self.check(ctx, term, typ)
                return typ

            case _:
                raise TypeError(f"Cannot infer type of {term}")

Type Equality

def equal(self, ctx: Context, a: Type, b: Type) -> bool:
    """
    Check type equality up to β-reduction.
    """
    # Normalize both types
    a_nf = self.normalize(ctx, a)
    b_nf = self.normalize(ctx, b)

    # Compare normal forms
    return self.alpha_equal(a_nf, b_nf)

def normalize(self, ctx: Context, term: Term) -> Term:
    """
    Reduce term to normal form.
    """
    match term:
        case App(Lam(x, body), arg):
            # β-reduction
            return self.normalize(ctx, self.subst(body, x, arg))

        case App(func, arg):
            func_nf = self.normalize(ctx, func)
            if func_nf != func:
                return self.normalize(ctx, App(func_nf, arg))
            return App(func_nf, self.normalize(ctx, arg))

        case _:
            return term

Dependent Types

-- Pi types: Π(x : A). B(x)
-- The type of functions where return type depends on input

-- Vector: type indexed by length
data Vec : Nat -> Type -> Type where
  Nil  : Vec 0 a
  Cons : a -> Vec n a -> Vec (Succ n) a

-- Dependent function: length is part of the type!
head : Π(n : Nat). Π(a : Type). Vec (Succ n) a -> a
head _ _ (Cons x _) = x

-- Sigma types: Σ(x : A). B(x)
-- Dependent pairs where second component type depends on first

-- Exists: there exists an n such that vec has length n
exists_vec : Σ(n : Nat). Vec n Int
exists_vec = (3, Cons 1 (Cons 2 (Cons 3 Nil)))

Universes

Type : Type₁ : Type₂ : Type₃ : ...

Universe levels prevent paradoxes:
- Type₀ (or just Type) is the type of "small" types
- Type₁ is the type of Type₀
- And so on...

Cumulativity: Type_i <: Type_{i+1}

Error Messages

class TypeErrorFormatter:
    """Generate helpful type error messages."""

    def format_mismatch(self, expected: Type, got: Type, term: Term) -> str:
        return f"""
Type mismatch:
  Expected: {self.pretty(expected)}
  Got:      {self.pretty(got)}
  In term:  {self.pretty(term)}

Hint: {self.suggest_fix(expected, got)}
"""

    def format_undefined(self, var: str, ctx: Context) -> str:
        similar = self.find_similar(var, ctx.names())
        return f"""
Undefined variable: {var}

Did you mean: {', '.join(similar)}?

Available in scope:
{self.format_context(ctx)}
"""

GF(3) Type Validation

class GF3TypeChecker(TypeChecker):
    """Type checker with GF(3) conservation verification."""

    def check_program(self, program: Program) -> Result:
        """
        Type check with GF(3) balance verification.
        """
        # Standard type checking
        type_result = super().check_program(program)

        if not type_result.success:
            return type_result

        # GF(3) validation
        gf3_result = self.verify_gf3_balance(program)

        return Result(
            success=type_result.success and gf3_result.balanced,
            types=type_result.types,
            gf3_sum=gf3_result.sum,
            conserved=gf3_result.balanced
        )

    def verify_gf3_balance(self, program: Program) -> GF3Result:
        """
        Verify program maintains GF(3) conservation.

        Terms classified:
        - GENERATOR (+1): Constructors, lambdas
        - COORDINATOR (0): Applications, matches
        - VALIDATOR (-1): Destructors, checks
        """
        trit_sum = 0
        for term in program.terms:
            trit_sum += self.term_trit(term)

        return GF3Result(
            sum=trit_sum,
            balanced=(trit_sum % 3 == 0)
        )

GF(3) Triads

type-checker (-1) ⊗ interaction-nets (0) ⊗ lambda-calculus (+1) = 0 ✓
type-checker (-1) ⊗ datalog-fixpoint (0) ⊗ hvm-runtime (+1) = 0 ✓
type-checker (-1) ⊗ move-narya-bridge (0) ⊗ discopy (+1) = 0 ✓

Commands

# Type check a file
just typecheck program.tt

# Infer types with holes
just typecheck program.tt --infer-holes

# Check with verbose output
just typecheck program.tt --verbose

# Generate type annotations
just typecheck program.tt --annotate

# Check Move contract types
just move-typecheck sources/gf3.move

Skill Name: type-checker Type: Type Theory / Static Analysis Trit: -1 (MINUS - VALIDATOR) GF(3): Validates type correctness before execution

Cat# Integration

This skill maps to Cat# = Comod(P) as a bicomodule in the Prof home:

Trit: 0 (ERGODIC)
Home: Prof (profunctors/bimodules)
Poly Op: ⊗ (parallel composition)
Kan Role: Adj (adjunction bridge)

GF(3) Naturality

The skill participates in triads where:

(-1) + (0) + (+1) ≡ 0 (mod 3)

This ensures compositional coherence in the Cat# equipment structure.