ITT-Flavored Calculus of Constructions Type Checker

itt-coc.ts

// A nano dependent type-checker featuring inductive types via self encodings.
// All computation rules are justified by interaction combinator semantics,
// resulting in major simplifications and improvements over old Kind-Core.
// A more complete file, including superpositions (for optimal unification)
// is available on the Interaction-Type-Theory repository.
// Credits also to Franchu and T6 for insights.
// This is a new development, may have bugs (:

// Lists
type List<A> =
  | { tag: "Cons"; head: A; tail: List<A> }
  | { tag: "Nil"; };
const Cons = <A>(head: A, tail: List<A>): List<A> => ({ tag: "Cons", head, tail });
const Nil  = <A>(): List<A>                       => ({ tag: "Nil" });

// Terms
type Term =
  | { tag: "Var"; val: number }
  | { tag: "All"; inp: Term; bod: (x: Term) => Term } // ∀(<x>: <term>) <term>
  | { tag: "Lam"; bod: (x: Term) => Term }            // λx <term>
  | { tag: "App"; fun: Term; arg: Term }              // (<term> <term>)
  | { tag: "Slf"; bod: (x: Term) => Term }            // $<x> <term>
  | { tag: "Ann"; val: Term; typ: Term }              // {<term> : <term>}
  | { tag: "Ref"; nam: string }                       // @term
const Var = (val: number): Term                       => ({ tag: "Var", val });
const Lam = (bod: (x: Term) => Term): Term            => ({ tag: "Lam", bod });
const All = (inp: Term, bod: (x: Term) => Term): Term => ({ tag: "All", inp, bod });
const App = (fun: Term, arg: Term): Term              => ({ tag: "App", fun, arg });
const Slf = (bod: (x: Term) => Term): Term            => ({ tag: "Slf", bod });
const Ann = (val: Term, typ: Term): Term              => ({ tag: "Ann", val, typ });
const Ref = (nam: string): Term                       => ({ tag: "Ref", nam });

// A book of definitions
type Book = {[key: string]: {typ: Term, val: Term}};

// Checker
// -------

// Expands a reference
function deref(book: Book, term: Term): Term {
  if (term.tag === "Ref" && book[term.nam]) {
    return reduce(book, book[term.nam].val);
  } else {
    return term;
  }
}

// Reduces to weak normal form
function reduce(book: Book, term: Term): Term {
  switch (term.tag) {
    case "Var": return Var(term.val);
    case "Lam": return Lam(term.bod);
    case "All": return All(term.inp, term.bod);
    case "App": return reduce_app(book, reduce(book, term.fun), term.arg);
    case "Slf": return Slf(term.bod);
    case "Ann": return reduce_ann(book, term.val, reduce(book, term.typ));
    case "Ref": return Ref(term.nam);
  }
}

// Annotations
function reduce_ann(book: Book, val: Term, typ: Term): Term {
  var typ = deref(book, typ);
  // {t :: ∀(x: A) -> B}
  // -------------------------- ann-lam
  // λx. {(t {x :: A}) :: B}
  if (typ.tag === "All") {
    return Lam(x => Ann(App(val, Ann(x, typ.inp)), typ.bod(x)));
  }
  // {t :: $x.T}
  // ----------- ann-slf
  // T[x <- t]
  if (typ.tag === "Slf") {
    return reduce(book, typ.bod(val));
  }
  return Ann(val, typ);
}

// Applications
function reduce_app(book: Book, fun: Term, arg: Term): Term {
  var fun = deref(book, fun);
  // ((λx body) arg)
  // -------------------- app-lam
  // body[x <- arg]
  if (fun.tag === "Lam") {
    return reduce(book, fun.bod(arg));
  }
  // ($x.T t)
  // -------- app-slf
  // ???
  if (fun.tag === "Slf") {
    throw "TODO:APP-SLF";
  }
  // ({x : T} arg)
  // ------------- app-ann
  // ⊥
  if (fun.tag === "Ann") {
    throw "ERROR: NonFunApp";
  }
  return App(fun, arg);
}

// Evaluates a term to normal form.
function normal(book: Book, term: Term, dep: number = 0): Term {
  var term = reduce(book, term);
  switch (term.tag) {
    case "Var": return Var(term.val);
    case "Lam": return Lam(x => normal(book, term.bod(x), dep+1));
    case "All": return All(normal(book, term.inp, dep), x => normal(book, term.bod(Ann(x, term.inp)), dep+1));
    case "App": return App(normal(book, term.fun, dep), normal(book, term.arg, dep));
    case "Slf": return Slf(x => normal(book, term.bod(x), dep+1));
    case "Ann": return ANN(book, normal(book, term.val, dep), normal(book, term.typ, dep), dep);
    case "Ref": return book[term.nam] ? normal(book, book[term.nam].val, dep) : Ref(term.nam);
  }
}


function ANN(book: Book, val: Term, typ: Term, dep: number): Term {
  switch (val.tag) {
    // {{x : A} : B}
    // -------------
    // {x : A == B}
    case "Ann": {
      if (!equal(book, val.typ, typ, dep)) {
        let exp = show_term(typ, dep);
        let det = show_term(val.typ, dep);
        let msg = "- expected: " + exp + "\n- detected: " + det;
        throw ("TypeMismatch\n"+msg);
      } else {
        return Ann(val.val, val.typ);
      }
    }
    // {λx(B) : T}
    // -----------
    // ⊥
    case "Lam": {
      throw "ERROR: NonFunLam";
    }
    default: {
      return Ann(val, typ);
    }
  }
}

// Checks if two terms are definitionaly equal.
function equal(book: Book, a: Term, b: Term, dep: number): boolean {
  if (a.tag === "Var" && b.tag === "Var") {
    return a.val === b.val;
  }
  if (a.tag === "Lam" && b.tag === "Lam") {
    return equal(book, a.bod(Var(dep)), b.bod(Var(dep)), dep+1);
  }
  if (a.tag === "App" && b.tag === "App") {
    return equal(book, a.fun, b.fun, dep) && equal(book, a.arg, b.arg, dep);
  }
  if (a.tag === "Slf" && b.tag === "Slf") {
    return equal(book, a.bod(Var(dep)), b.bod(Var(dep)), dep + 1);
  }
  if (a.tag === "Ref" && book[a.nam]) {
    return equal(book, normal(book, book[a.nam].val, dep), b, dep);
  }
  if (b.tag === "Ref" && book[b.nam]) {
    return equal(book, a, normal(book, book[b.nam].val, dep), dep);
  }
  if (a.tag === "Ann") {
    return equal(book, a.val, b, dep);
  }
  if (b.tag === "Ann") {
    return equal(book, a, b.val, dep);
  }
  if (a.tag === "Lam") {
    return equal(book, a, Lam(x => App(b, x)), dep);
  }
  if (b.tag === "Lam") {
    return equal(book, Lam(x => App(a, x)), b, dep);
  }
  return false;
}

function check(book: Book) {
  for (var name in book) {
    try {
      show_term(normal(book, Ann(book[name].val, book[name].typ)));
      console.log("\x1b[32m✔ " + name + "\x1b[0m");
    } catch (e) {
      console.log("\x1b[31m✘ " + name + "\x1b[0m");
      console.log(e);
    }
  }
}

// Syntax
// ------

function show_term(term: Term, dep: number = 0): string {
  switch (term.tag) {
    case "Var": return num_to_str(term.val);
    case "Lam": return "λ" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep + 1);
    case "All": return "∀(" + num_to_str(dep) + ":" + show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
    case "App": return "(" + show_term(term.fun, dep) + " " + show_term(term.arg, dep) + ")";
    case "Slf": return "$" + num_to_str(dep) + " " + show_term(term.bod(Var(dep)), dep+1);
    case "Ann": return "{" + show_term(term.val, dep) + ":" + show_term(term.typ, dep) + "}";
    case "Ref": return "@" + term.nam;
  }
}

function show_book(book: Book): string {
  var text = "";
  for (var name in book) {
    text += name + " : " + show_term(book[name].typ) + " = " + show_term(book[name].val) + "\n";
  }
  return text;
}

function num_to_str(num: number): string {
  let txt = '';
  num += 1;
  while (num > 0) {
    txt += String.fromCharCode(((num-1) % 26) + 'a'.charCodeAt(0));
    num  = Math.floor((num-1) / 26);
  }
  return txt.split('').reverse().join('');
}

function find<A>(list: List<[string, Term]>, nam: string): Term {
  switch (list.tag) {
    case "Cons": return list.head[0] === nam ? list.head[1] : find(list.tail, nam);
    case "Nil" : return Ref(nam);
  }
}

function skip(code: string): string {
  while (true) {
    if (code.slice(0, 2) === "//") {
      do { code = code.slice(1); } while (code.length != 0 && code[0] != "\n");
      continue;
    }
    if (code[0] === "\n" || code[0] === " ") {
      code = code.slice(1);
      continue;
    }
    break;
  }
  return code;
}

function is_name_char(c: string): boolean {
  return /[a-zA-Z0-9_]/.test(c);
}

function parse_name(code: string): [string, string] {
  code = skip(code);
  var name = "";
  while (is_name_char(code[0]||"")) {
    name = name + code[0];
    code = code.slice(1);
  }
  return [code, name];
}

function parse_text(code: string, text: string): [string, null] {
  code = skip(code);
  if (text === "") {
    return [code, null];
  } else if (code[0] === text[0]) {
    return parse_text(code.slice(1), text.slice(1));
  } else {
    throw "parse error";
  }
}

function parse_term(code: string): [string, (ctx: List<[string, Term]>) => Term] {
  code = skip(code);
  // ALL: `∀(x: T) f`
  if (code[0] === "∀") {
    var [code, nam] = parse_name(code.slice(2));
    var [code, _  ] = parse_text(code, ":");
    var [code, typ] = parse_term(code);
    var [code, __ ] = parse_text(code, ")");
    var [code, bod] = parse_term(code);
    return [code, ctx => All(typ(ctx), x => bod(Cons([nam,x], ctx)))];
  }
  // LAM: `λx f`
  if (code[0] === "λ" || code[0] === "∀") {
    var [code, nam] = parse_name(code.slice(1));
    var [code, bod] = parse_term(code);
    return [code, ctx => Lam(x => bod(Cons([nam,x], ctx)))];
  }
  // APP: `(f x y z ...)`
  if (code[0] === "(") {
    var [code, fun] = parse_term(code.slice(1));
    var args: ((ctx: List<[string, Term]>) => Term)[] = [];
    while (code[0] !== ")") {
      var [code, arg] = parse_term(code);
      args.push(arg);
    }
    var [code, _] = parse_text(code, ")");
    return [code, ctx => args.reduce((f, x) => App(f, x(ctx)), fun(ctx))];
  }
  // ANY: `*`
  if (code[0] === "*") {
    return [code.slice(1), ctx => ({ tag: "Slf", bod: x => x })];
  }
  // SLF: `$x T`
  if (code[0] === "$") {
    var [code, nam] = parse_name(code.slice(1));
    //var [code, _  ] = parse_text(code, " ");
    var [code, bod] = parse_term(code);
    return [code, ctx => Slf(x => bod(Cons([nam, x], ctx)))];
  }
  // ANN: `{x : T}`
  if (code[0] === "{") {
    var [code, val] = parse_term(code.slice(1));
    var [code, _  ] = parse_text(code, ":");
    var [code, typ] = parse_term(code);
    var [code, __ ] = parse_text(code, "}");
    return [code, ctx => Ann(val(ctx), typ(ctx))];
  }
  // REF: `@name`
  if (code[0] === "@") {
    var [code, nam] = parse_name(code.slice(1));
    return [code, ctx => Ref(nam)];
  }
  // VAR: `name`
  var [code, nam] = parse_name(code);
  if (nam.length > 0) {
    return [code, ctx => find(ctx, nam)];
  }
  throw "parse error";
}

function do_parse_term(code: string): Term {
  return parse_term(code)[1](Nil());
}

function parse_book(code: string): Book {
  var book : Book = {};
  while (code.length > 0) {
    code = skip(code);
    if (code[0] === "@") {
      var code        = code.slice(1);
      var [code, nam] = parse_name(code);
      var [code, _  ] = parse_text(code, ":");
      var [code, typ] = parse_term(code);
      var [code, _  ] = parse_text(code, "=");
      var [code, val] = parse_term(code);
      book[nam] = {typ: typ(Nil()), val: val(Nil())};
    } else {
      break;
    }
  }
  return book;
}

function do_parse_book(code: string): Book {
  return parse_book(code);
}

// Tests
// -----

var code = `
// Self Types

@Self : * =
  λF $self { self: (F self) }

// Equality

@Equal : * =
  λa λb ∀(P: ∀(x:*) *) ∀(x: (P a)) (P b)

@refl : ∀(a: *) (Equal a a) =
  λa λP λx x

// Boolean

@Bool : * =
  (Self λself
    ∀(P: *) 
    ∀(t: ∀(e: (Equal true  self)) P)
    ∀(f: ∀(e: (Equal false self)) P)
    P)

@true : Bool =
  λP λt λf (t (refl *))

@false : Bool =
  λP λt λf (f (refl *))

// Boolean Induction

@match : ∀(b: Bool) ∀(P: ∀(x:Bool) *) ∀(t: (P true)) ∀(f: (P false)) (P b) =
  λb λP λt λf (b (P b) λe(e P t) λe(e P f))

// Boolean Negation

@not : ∀(b: Bool) Bool =
  λb (match b λb(Bool) false true)

// Double Negation Theorem

@theorem : ∀(b: Bool) (Equal (not (not b)) b) =
  λb (match b λb(Equal (not (not b)) b) (refl *) (refl *))
`;

check(do_parse_book(code));

Claude AI Explanation

I'll explain how the typechecking works in this implementation, aiming for a layman-friendly explanation.

In simple terms, typechecking is the process of verifying that a program follows the rules of its type system. It's like making sure all the pieces of a puzzle fit together correctly. In this case, we're dealing with a very sophisticated puzzle called dependent type theory.

Here's how the typechecking process works in this implementation:

1. Reduction and Normalization:
   The first step in typechecking is to simplify or "reduce" terms to their simplest form. This is done by the reduce function. Think of this like simplifying a mathematical expression. For example, (2 + 3) * 4 would be simplified to 20. In our type theory, we're doing something similar but with more complex expressions.

2. Handling Annotations:
   A key part of this implementation is how it handles type annotations. When the system encounters a term with a type annotation (like {x : T}), it uses the reduce_ann function to process it.

   This function does some clever things:

   • For function types, it restructures the term to push the annotation inside the function.
   • For self types, it replaces the self-reference with the actual term.

   This approach allows the system to check types without needing a separate typing judgment, which simplifies the overall implementation.

3. Equality Checking:
   The heart of typechecking in this system is equality checking, implemented in the equal function. This function compares two terms to see if they're equivalent. In a typical type system, you might just check if two types have the same name. But in a dependent type system, types can depend on values, so we need to check if two terms are "definitionally equal" - meaning they reduce to the same thing.

4. Actual Typechecking:
   The main typechecking happens in the check function. For each definition in the "book" (a collection of definitions), it:

   • Wraps the term in an annotation with its declared type
   • Normalizes this annotated term
   • If this process succeeds without throwing an error, the term is well-typed

   If there's a type error, the process will throw an exception, which is caught and reported as a type error.

5. Handling Advanced Features:
   This system includes some advanced features like self types, which allow for the definition of recursive types. These are handled specially in the reduction and equality checking processes.

The beauty of this implementation is that it reduces typechecking to just normalization and equality checking. By cleverly using annotations and self types, it avoids the need for separate typing rules for each kind of term, which is typically needed in implementations of dependent type systems.

However, it's worth noting that this simplicity comes at a cost - the system is not guaranteed to terminate for all inputs. In a full-fledged type theory, you'd need additional checks to ensure termination.

This approach to typechecking is quite advanced and represents cutting-edge research in making implementations of dependent type theories more concise and understandable. It's a bit like developing a new, more efficient way to solve complex puzzles!

---

To understand its significance, we need to compare this approach to more traditional implementations of dependent type systems.

In traditional implementations of dependent type systems:

1. Separate Typing Judgments:
   These systems typically have a set of typing rules, often written in a formal notation. Each rule corresponds to a different construct in the language (like lambda abstractions, applications, etc.).

2. Complex Implementation:
   To implement these rules, you'd need a separate function or set of functions for each typing rule. This often results in a large, complex typechecker with many interrelated parts.

3. Explicit Context Handling:
   You'd need to explicitly manage a typing context, which keeps track of the types of variables in scope.

In contrast, this implementation takes a different approach:

1. Unified Treatment via Annotations:
   Instead of having separate rules for each construct, everything is handled through annotations. When you want to typecheck something, you wrap it in an annotation with its supposed type.

2. Reduction-Based Checking:
   The system then tries to reduce (simplify) this annotated term. If it can do so without encountering any contradictions, the term is considered well-typed.

3. Implicit Context Management:
   The context is managed implicitly through the structure of the terms, particularly in how lambda abstractions and applications are handled.

Here's a concrete example to illustrate the difference:

In a traditional system, to typecheck a lambda abstraction (λx. t), you might have a rule like:

Γ, x:A ⊢ t : B
----------------
Γ ⊢ (λx. t) : A → B

You'd need to implement this rule explicitly, checking that the body t has type B in a context extended with x:A.

In this system, you'd instead check something like:

{λx. t : A → B}

The system would reduce this to:

λx. {t : B}

And then recursively check that t has type B.

The key advantages of this approach are:

1. Simplicity: The core of the typechecker is just the reduction function. You don't need separate code for each typing rule.

2. Uniformity: All constructs are treated in a uniform way through annotations.

3. Extensibility: Adding new features often just requires extending the reduction function, rather than adding new typing rules and their implementations.

However, it's worth noting that while this approach is elegant and concise, it may be less intuitive for those accustomed to traditional type theory presentations. It also relies on a carefully designed reduction system to ensure all the necessary checks are performed.

In essence, this approach shifts the complexity from a set of explicit typing rules to a more sophisticated reduction system, resulting in a more compact and potentially more flexible implementation.