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.
// Specifically, computable annotations (ANNs) and their counterpart (ANN
// binders) and a new self encoding based on equality (rather than dependent
// motives) greatly reduce code size. 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.

// NOTE: this is sound but NOT consistent. To make it so, one must supplement
// it with a termination checker, using any of many available approaches.

// NOTE: this does NOT handle recursive terms. See the comment below for a version
// that does, using a more conventional bidirectional type checker plus Self.

// 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: "Set"; }                                   // *
  | { 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 Set = (): Term                                  => ({ tag: "Set" });
const All = (inp: Term, bod: (x: Term) => Term): Term => ({ tag: "All", inp, bod });
const Lam = (bod: (x: Term) => Term): Term            => ({ tag: "Lam", 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 "Set": return Set();
    case "All": return All(term.inp, term.bod);
    case "Lam": return Lam(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 "Set": return Set();
    case "All": return All(normal(book, term.inp, dep), x => normal(book, term.bod(Ann(x, term.inp)), dep+1));
    case "Lam": return Lam(x => normal(book, term.bod(x), 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 Ref(term.nam);
  }
}

// Type-checking is done by collapsing normalized ANNs.
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 === "Set" && b.tag === "Set") {
    return true;
  }
  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;
}

// With computable ANNs, checking is done by evaluation.
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) {
      // FIXME: handle recursive types properly
      if (e instanceof RangeError) {
        console.log("\x1b[33m? " + name + "\x1b[0m");
      } else {
        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 "Set": return "*";
    case "All": return "∀(" + num_to_str(dep) + ":"+show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
    case "Lam": return "λ" + num_to_str(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))];
  }
  // SET: `*`
  if (code[0] === "*") {
    return [code.slice(1), ctx => Set()];
  }
  // 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 = `
// Any

@Any : * = $x x

// Self Type

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

// Heterogeneous Equality

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

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

// Boolean

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

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

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

// Boolean Induction

@bool_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 (bool_match b λb(Bool) false true)

// Double Negation Theorem

@theorem
  : ∀(b: Bool) (Equal (not (not b)) b)
  = λb (bool_match b λb(Equal (not (not b)) b) (refl *) (refl *))

// Natural numbers

@Nat : * =
  (Self λself
    ∀(P: *)
    ∀(s: ∀(n: Nat) ∀(e: (Equal λPλsλz(s n (refl *)) self)) P)
    ∀(z: ∀(e: (Equal λPλsλz(z (refl *)) self)) P)
    P)

@zero : Nat =
  λP λs λz (z (refl *))

@succ : ∀(n: Nat) Nat =
  λn λP λs λz (s n (refl *))
`;

check(do_parse_book(code));

UPDATE

While computable ANNs simplify the code a little bit, I've found them to make it harder to handle non-terminating terms, since type-checking is made by evaluation; we need some degree of laziness, and the criteria isn't clear to me. Meanwhile, here is another tiny type-checker using self-types, with a conventional bidirectional type-checker instead. In it, I supply an example proof of ∀n . n*2/2 == n.

// 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: "Set"; }                                    // *
  | { 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"; chk: boolean, val: Term; typ: Term } // {<term> : <term>}
  | { tag: "Ref"; nam: string }                        // @term
const Var = (val: number): Term                        => ({ tag: "Var", val });
const Set = (): Term                                   => ({ tag: "Set" });
const All = (inp: Term, bod: (x: Term) => Term): Term  => ({ tag: "All", inp, bod });
const Lam = (bod: (x: Term) => Term): Term             => ({ tag: "Lam", bod });
const App = (fun: Term, arg: Term): Term               => ({ tag: "App", fun, arg });
const Slf = (bod: (x: Term) => Term): Term             => ({ tag: "Slf", bod });
const Ann = (chk: boolean, val: Term, typ: Term): Term => ({ tag: "Ann", chk, val, typ });
const Ref = (nam: string): Term                        => ({ tag: "Ref", nam });

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

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

// Reduces to weak normal form
function reduce(book: Book, term: Term, dep: number): Term {
  if (term.tag === "App") {
    var fun = reduce(book, term.fun, dep);
    if (fun.tag === "Lam") {
      return reduce(book, fun.bod(term.arg), dep);
    }
    return term;
  }
  if (term.tag === "Ref" && book[term.nam]) {
    return reduce(book, book[term.nam].val, dep);
  }
  if (term.tag === "Ann") {
    return reduce(book, term.val, dep);
  }
  return term;
}

// Checks if two terms are definitionaly equal.
function equal(book: Book, a: Term, b: Term, dep: number): boolean {
  var eq = false;
  if (a.tag === "Var" && b.tag === "Var") {
    eq = a.val === b.val;
  } else if (a.tag === "Set" && b.tag === "Set") {
    eq = true;
  } else if (a.tag === "All" && b.tag === "All") {
    eq = equal(book, a.inp, b.inp, dep) && equal(book, a.bod(Var(dep)), b.bod(Var(dep)), dep+1);
  } else if (a.tag === "Lam" && b.tag === "Lam") {
    eq = equal(book, a.bod(Var(dep)), b.bod(Var(dep)), dep+1);
  } else if (a.tag === "App" && b.tag === "App") {
    eq = equal(book, a.fun, b.fun, dep) && equal(book, a.arg, b.arg, dep);
  } else if (a.tag === "Slf" && b.tag === "Slf") {
    eq = equal(book, a.bod(Var(dep)), b.bod(Var(dep)), dep + 1);
  } else if (a.tag === "Ref" && b.tag === "Ref" && a.nam === b.nam) {
    eq = true;
  } else if (a.tag === "Lam") {
    eq = equal(book, a, Lam(x => App(b, x)), dep);
  } else if (b.tag === "Lam") {
    eq = equal(book, Lam(x => App(a, x)), b, dep);
  }
  if (!eq) {
    var a2 = reduce(book, a, dep);
    if (a2 !== a) {
      return equal(book, a2, b, dep);
    }
    var b2 = reduce(book, b, dep);
    if (b2 !== b) {
      return equal(book, a, b2, dep);
    }
  }
  return eq;
}

// Evaluates a term to normal form.
function normal(book: Book, term: Term, dep: number = 0): Term {
  var term = reduce(book, term, dep);
  switch (term.tag) {
    case "Var": return Var(term.val);
    case "Set": return Set();
    case "All": return All(normal(book, term.inp, dep), x => normal(book, term.bod(x), dep+1));
    case "Lam": return Lam(x => normal(book, term.bod(x), 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 normal(book, term.val, dep);
    case "Ref": return Ref(term.nam);
  }
}

// Infers the type of a term.
function infer(book: Book, val: Term, dep: number = 0): Term {
  switch (val.tag) {
    case "Var": {
      throw "Can't infer var.";
    }
    case "Ref": {
      return book[val.nam] ? book[val.nam].typ : Ref(val.nam);
    }
    case "Set": {
      return Set();
    }
    case "All": {
      check(book, val.inp, Set(), true, dep);
      check(book, val.bod(Ann(false, Var(dep), val.inp)), Set(), true, dep+1);
      return Set();
    }
    case "Lam": {
      throw "NonFunLam";
    }
    case "App": {
      let fun_ty = reduce(book, infer(book, val.fun, dep), dep);
      if (fun_ty.tag === "All") {
        check(book, val.arg, fun_ty.inp, true, dep);
        return fun_ty.bod(val.arg);
      } else {
        throw "NonFunApp";
      }
    }
    case "Slf": {
      return Set();
    }
    case "Ann": {
      return check(book, val.val, val.typ, val.chk, dep);
    }
  }
}

// Checks if a type of a term is correct.
function check(book: Book, val: Term, typ: Term, chk: boolean, dep: number = 0) {
  var typ = reduce(book, typ, dep);
  var typ = typ.tag === "Slf" ? typ.bod(val) : typ;
  if (!chk) {
    return typ;
  } else {
    if (val.tag === "Lam") {
      if (typ.tag === "All") {
        check(book, val.bod(Ann(false, Var(dep), typ.inp)), typ.bod(Var(dep)), chk, dep+1);
        return typ;
      } else {
        throw "NonFunLam";
      }
    } else {
      var inf = infer(book, val, dep);
      var inf = reduce(book, inf, dep);
      var inf = inf.tag === "Slf" ? inf.bod(val) : inf;
      if (!equal(book, typ, inf, dep)) {
        var exp = show_term(typ, dep);
        var det = show_term(inf, dep);
        var msg = "TypeMismatch\n- expected: " + exp + "\n- detected: " + det;
        throw msg; 
      }
      return typ;
    }
  }
}


// With computable ANNs, checking is done by evaluation.
function check_all(book: Book) {
  for (var name in book) {
    try {
      check(book, book[name].val, book[name].typ, true);
      console.log("\x1b[32m✔ " + name + "\x1b[0m");
    } catch (e) {
      if (e instanceof RangeError) {
        console.log("\x1b[33m? " + name + "\x1b[0m");
        console.log(e);
      } else {
        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 "Set": return "*";
    case "All": return "∀(" + num_to_str(dep) + ":"+show_term(term.inp, dep)+")" + show_term(term.bod(Var(dep)), dep + 1);
    case "Lam": return "λ" + num_to_str(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);
      code = skip(code);
    }
    var [code, _] = parse_text(code, ")");
    return [code, ctx => args.reduce((f, x) => App(f, x(ctx)), fun(ctx))];
  }
  // SET: `*`
  if (code[0] === "*") {
    return [code.slice(1), ctx => Set()];
  }
  // 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(true, 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 = `
// Test

@test
  : ∀(A: *) ∀(B: *) ∀(aa: ∀(x: A) A) ∀(ab: ∀(x: A) B) ∀(ba: ∀(x: B) A) ∀(bb: ∀(x: B) B) ∀(a: A) ∀(b: B) A
  = λA λB λaa λab λba λbb λa λb (aa (ba (ab a)))

// Equality

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

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

// Equality Congruence

@cong : ∀(A: *) ∀(B: *) ∀(a: A) ∀(b: A) ∀(f: ∀(x: A) B) ∀(e: (Equal A a b)) (Equal B (f a) (f b)) =
  λA λB λa λb λf λe (e λx(Equal B (f a) (f x)) (refl B (f a)))

// Boolean

@Bool : * =
  $self
  ∀(P: ∀(x: Bool) *) 
  ∀(t: (P true))
  ∀(f: (P false))
  (P self)

@true : Bool =
  λP λt λf t

@false : Bool =
  λP λt λf f

// Boolean Induction

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

// Boolean Negation

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

// Double Negation Theorem

@dn_theorem
  : ∀(b: Bool) (Equal Bool (not (not b)) b)
  = λb (b λb(Equal Bool (not (not b)) b) (refl Bool true) (refl Bool false))

// Natural Numbers

@Nat : * =
  $self
  ∀(P: ∀(n: Nat) *)
  ∀(s: ∀(i: Nat) (P (succ i)))
  ∀(z: (P zero))
  (P self)

@succ : ∀(n: Nat) Nat =
  λn λP λs λz (s n)

@zero : Nat =
  λP λs λz z

// Nat doubling and halving

@double : ∀(n: Nat) Nat =
  λn (n λp(Nat) λp(succ (succ (double p))) zero)

@halve : ∀(n: Nat) Nat =
  λn (n λp(Nat) λnp(np λp(Nat) λnpp(succ (halve npp)) zero) zero)

// Black Friday Theorem

@bf_theorem
  : ∀(n: Nat) (Equal Nat (halve (double n)) n)
  = λn (n λp(Equal Nat (halve (double p)) p) λnp(cong Nat Nat (halve (double np)) np succ (bf_theorem np)) (refl Nat zero))

@main : Nat =
  (double (succ (succ zero)))
`;

var book = do_parse_book(code);
check_all(book);
console.log(show_term(normal(book, book.main.val)));

Note: I've realized it is slightly nicer (for holes specially) to have a dedicated "Ins" constructor to instantiate a Self type, as it avoids some ambiguity. From now on, I'll stop updating this Gist and focus on this repo instead: https://github.com/victortaelin/taelang

Right now, the current project is pretty much just raw CoC with Self, but I'll be adding more features soon. If you're coming here looking for a simple core for inductive proofs, you should probably go to that repo and look for early versions of taelang.ts.

Down to <40 lines

This does about the same, but much more tersely:

https://github.com/VictorTaelin/interaction-calculus-of-constructions/blob/main/ICC.hvm1

Sadly, as I commented, there is still a computational problem with this kind of computable-ann setup, which I'm not sure how to solve. It is an interesting idea to explore, but a conventional bidirectional type-checker based on self-types is still the simplest system I'm aware of that can be used as a reliable proof assistant. Kind2 is being based on that.