Dependent Type Implementer

Implements dependent type theory (Type Theory, Π Types, Σ Types).

When to Use

• Building proof assistants (Coq, Agda, Idris)
• Formalizing mathematics
• Verified programming
• Type-level computation

What This Skill Does

1. Implements Π types - Dependent functions τ → σ(x)
2. Implements Σ types - Dependent pairs (x:τ) × σ(x)
3. Type checking - With conversion and unification
4. Proof elaboration - From surface to core syntax

How to Use

1. Start from a minimal core (Var, Pi, Lam, App, universes)
2. Implement normalization and definitional equality
3. Type-check by synthesis/checking with conversion
4. Add Sigma, naturals, and eliminators incrementally

Core Theory

Dependent Function (Π):
  Π(x:A). B  or  (x:A) → B
  
  When x not in B: A → B (non-dependent)

Dependent Pair (Σ):
  Σ(x:A). B  or  (x:A) × B
  
  When x not in B: A × B (product)

Type formation rules:
  Γ ⊢ A : s    Γ, x:A ⊢ B : s
  ------------------------------
  Γ ⊢ Π(x:A).B : s
  
  Γ ⊢ A : s    Γ, x:A ⊢ B : s
  ------------------------------
  Γ ⊢ Σ(x:A).B : s

Implementation

(* Core Syntax (conceptual) *)

Term types:
  - Type (universe)
  - Var (de Bruijn index)
  - Lam (abstraction with optional type annotation)
  - App (application)
  - Pi (dependent function type)
  - Sigma (dependent pair type)
  - Pair, Proj1, Proj2 (pair intro/elim)
  - Unit, Nat, Zero, Succ, NatElim (basic types)

Type formation rules:
  Γ ⊢ A : s    Γ, x:A ⊢ B : s
  ------------------------------
  Γ ⊢ Π(x:A).B : s

  Γ ⊢ A : s    Γ, x:A ⊢ B : s
  ------------------------------
  Γ ⊢ Σ(x:A).B : s

Typing rules (key cases):
  T_Abs:  Γ ⊢ A : s
          Γ, x:A ⊢ N : B
          ----------------
          Γ ⊢ λx:A. N : Π(x:A).B

  T_App:  Γ ⊢ M : Π(x:A).B
          Γ ⊢ N : A
          -----------------
          Γ ⊢ M N : B[x := N]

  T_Pair: Γ ⊢ M : A
          Γ ⊢ N : B[x := M]
          ------------------
          Γ ⊢ (M, N) : Σ(x:A).B

Elaboration

From surface syntax to core:

Surface: λ(x : A) => e
Core:    Lam A e

Elaboration algorithm:
1. Infer type of binding: A : s
2. Extend context with x : A
3. Elaborate body: e : B
4. Compute result type:
   - Non-dependent: Pi A (λx. B)
   - Dependent: Pi A (λx. B)

Pattern matching elaboration:
  match e return P with
  | c1 => e1
  | c2 => e2
  end

  becomes:
  NatElim P e (λ_. e1) (λn. λIH. e2)

Universe Polymorphism

(* Cumulative universes *)
Inductive universe : Type :=
  | Set0 : universe
  | Set1 : universe
  | Set2 : universe
  | ... (* Prop, SProp, etc. *)

(* Universe constraints *)
Check (Type@{i} -> Type@{j}).
(* i ≤ j required *)

(* Cumulative: Set@{i} ≤ Set@{i+1} *)

Implementation in OCaml

(* Core dependent type checker *)

type term =
  | Var of int
  | Lambda of term * term
  | App of term * term
  | Pi of term * term        (* Π x : A. B *)
  | Sigma of term * term     (* Σ x : A. B *)
  | Pair of term * term
  | Proj1 of term
  | Proj2 of term
  | Star                       (* unit *)
  | Nat | Zero | Succ of term
  | NatElim of term * term * term * term

type value =
  | VLambda of (value -> value)
  | VPi of value * (value -> value)
  | VSigma of value * value
  | VPair of value * value
  | VStar
  | VNat
  | VZero
  | VSucc of value

let rec eval (t : term) (ρ : value list) : value =
  match t with
  | Var i -> List.nth ρ i
  | Lambda (a, b) -> VLambda (fun v -> eval b (v :: ρ))
  | App (m, n) ->
      let vm = eval m ρ in
      let vn = eval n ρ in
      (match vm with
       | VLambda f -> f vn
       | _ -> failwith "apply non-function")
  | Pi (a, b) -> VPi (eval a ρ) (fun v -> eval b (v :: ρ))
  (* ... more cases *)

Key Concepts

Advanced Features

Tips

• Start with simple dependent types
• Implement conversion checking carefully
• Use de Bruijn for binding
• Consider universe constraints
• Handle definitional equality

Related Skills

• system-f - Polymorphic lambda calculus
• type-inference-engine - HM inference
• coq-proof-assistant - Coq proofs

Canonical References

Tradeoffs and Limitations

Implementation Approach Tradeoffs

When NOT to Implement Dependent Types

• For simple verification: Use refinement types instead (Liquid Haskell, F*)
• For performance: Consider Haskell/OCaml with GADTs
• For teaching: Start with System F or STLC

Complexity Considerations

• Undecidability: Full type checking is undecidable for dependent types
• Universe constraints: Solving universe constraints is complex
• Normalization: Required for conversion; expensive without NbE
• Type inference: Principally undecidable; use bidirectional checking

Limitations

• Performance: 10-100x slower than simple types
• Error messages: Hard to make comprehensible
• Termination checking: Required for soundness (or positivity)
• Universe levels: Must handle Level → Level max → etc.
• Normalization: Full β-reduction needed for conversion
• Learning curve: Users need to understand type theory

Research Tools & Artifacts

Dependent type systems:

Key Papers

• Martin-Löf - Original type theory
• Coquand - Calculus of Constructions
• Harper et al. - Syntactic theory

Research Frontiers

1. Homotopy Type Theory

• Goal: Univalence, higher inductive types
• Approach: Path types, identity types
• Books: HoTT Book

2. Cubical Type Theory

• Goal: Computational univalence
• Approach: Kan operations, faces

Implementation Pitfalls