Type Checker Skill
/plugin marketplace add plurigrid/asi/plugin install asi-skills@asi-skillsThis skill inherits all available tools. When active, it can use any tool Claude has access to.
README.md"Catch errors before they run. Types are theorems, programs are proofs."
Type Checker implements bidirectional type checking for dependent types. Validates that programs are well-typed before execution, catching errors at compile time.
| Aspect | Value |
|---|---|
| Trit | -1 (MINUS) |
| Role | VALIDATOR |
| Function | Validates type correctness of programs |
┌─────────────────────────────────────────────────────────────────┐
│ 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 │
│ │
└─────────────────────────────────────────────────────────────────┘
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}")
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
-- 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)))
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}
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)}
"""
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)
)
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 ✓
# 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
This skill connects to the K-Dense-AI/claude-scientific-skills ecosystem:
general: 734 citations in bib.duckdbThis 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)
The skill participates in triads where:
(-1) + (0) + (+1) ≡ 0 (mod 3)
This ensures compositional coherence in the Cat# equipment structure.