-
-
Save VictorTaelin/dd291148ee59376873374aab0fd3dd78 to your computer and use it in GitHub Desktop.
// 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.
almost perfect! could make 8 lines shorter...