wip

main.ts

@@ -5,7 +5,11 @@ export type expr =
   | { kind: "universe"; level: number }
   | { kind: "pi"; abs: abstraction }
   | { kind: "lambda"; abs: abstraction }
-  | { kind: "app"; left: expr; right: expr };
+  | { kind: "app"; left: expr; right: expr }
+
+  // Types
+  | { kind: "cons"; name: variable; type: expr }
+  | { kind: "elim"; name: variable; eval: (_: expr) => expr };
 
 export interface abstraction {
   x: variable;
@@ -20,6 +24,7 @@ export type variable =
   | { kind: "string"; name: string }
   | { kind: "gensym"; name: string; n: number }
   | { kind: "dummy" };
+const dummy: variable = { kind: "dummy" };
 
 export interface Substitution {
   x: variable;
@@ -52,6 +57,9 @@ export function subst(s: Substitution[], e: expr): expr {
       return { kind: "lambda", abs: substAbstraction(s, e.abs) };
     case "app":
       return { kind: "app", left: subst(s, e.left), right: subst(s, e.right) };
+    case "cons":
+    case "elim":
+      return e;
   }
 }
 
@@ -279,7 +287,7 @@ export function ppExpr(e: expr): string {
     case "pi":
       if (occursIn(e.abs.x, e.abs.body)) {
         return `(∏ (${ppVariable(e.abs.x)} : ${ppExpr(e.abs.type)}), ${ppExpr(
-          e.abs.type,
+          e.abs.body,
         )})`;
       }
       return `(${ppExpr(e.abs.type)} → ${ppExpr(e.abs.body)})`;
@@ -301,13 +309,126 @@ export function ppContext(ctx: context): string {
   return `[${ss.join(", ")}]`;
 }
 
+// =============================================================================
+// Types
+
+// =============================================================================
+// W-types
+
+interface InductiveTypeDefinition {
+  name: string;
+  labels: InductiveTypeLabel[];
+}
+
+interface InductiveTypeLabel {
+  name: string;
+  type: expr;
+}
+
+interface InductiveType {
+  // The new context
+  ctx: context;
+
+  // Name of the type
+  T: variable;
+
+  // Recursor
+  rec: variable;
+}
+
+export function defineInductiveType(
+  ctx: context,
+  def: InductiveTypeDefinition,
+): InductiveType {
+  const ctx2 = [...ctx];
+  const Tvar: variable = { kind: "string", name: def.name };
+  ctx2.push({
+    x: Tvar,
+    type: { kind: "universe", level: 0 },
+  });
+  const T: expr = { kind: "var", x: Tvar };
+
+  // First, we need A, which represents the labels of this W-type
+  // The size of A is equal to the number of constructors we have
+  const Aname = refresh({ kind: "string", name: `A` });
+  const A: expr = { kind: "var", x: Aname };
+  ctx2.push({ x: Aname, type: { kind: "universe", level: 0 } });
+  const labels: variable[] = def.labels.map((label, idx) => {
+    const newName = refresh({
+      kind: "string",
+      name: `cons${idx}`,
+    });
+    ctx2.push({ x: newName, type: A });
+    return newName;
+  });
+
+  // Now we need B : A -> U, which is the arity of labels
+  const Bname = refresh({ kind: "string", name: `B` });
+  const B: expr = { kind: "var", x: Bname };
+
+  function inferArity(ctx: context, e: expr): number {
+    switch (e.kind) {
+      case "var": {
+        const value = lookupValue(e.x, ctx);
+        if (!value) return 0;
+        return inferArity(ctx, value);
+      }
+      case "pi":
+        return 1 + inferArity(ctx, e.abs.body);
+      case "app":
+      case "lambda":
+      case "universe":
+        return 0;
+    }
+  }
+  // biome-ignore lint/complexity/noForEach: <explanation>
+  const labelArities: number[] = def.labels.forEach((label, idx) => {
+    const arity = inferArity(ctx2, label.type);
+    console.log(`arity(${ppExpr(label.type)}) = ${arity}`);
+  });
+
+  // Create the supremum function
+  const supName: variable = refresh({ kind: "string", name: `sup` });
+  const sup_a_name: variable = refresh({ kind: "string", name: "a" });
+  const sup_a: expr = { kind: "var", x: sup_a_name };
+  const supType: expr = {
+    kind: "pi",
+    abs: {
+      x: dummy,
+      type: {
+        kind: "pi",
+        abs: {
+          x: sup_a_name,
+          type: A,
+          body: {
+            kind: "pi",
+            abs: {
+              x: dummy,
+              type: { kind: "app", left: B, right: sup_a },
+              body: T,
+            },
+          },
+        },
+      },
+      body: T,
+    },
+  };
+  ctx2.push({
+    x: supName,
+    type: supType,
+  });
+
+  // Now we have the W-type representing this
+
+  return ctx2;
+}
+
 // =============================================================================
 // Testing
 
 function test() {
   const ctx: context = [];
 
-  const dummy: variable = { kind: "dummy" };
   const varify = (name: string): expr => ({
     kind: "var",
     x: { kind: "string", name },
@@ -383,9 +504,19 @@ function test() {
   };
   define("result", normalize(ctx, evaled));
 
+  const N2 = varify("N2");
+  const N2toN2: expr = { kind: "pi", abs: { x: dummy, type: N2, body: N2 } };
+  const ctx2 = defineInductiveType(ctx, {
+    name: "N2",
+    labels: [
+      { name: "zero", type: N2 },
+      { name: "suc", type: N2toN2 },
+    ],
+  });
+
   console.log("ctx =");
   // biome-ignore lint/complexity/noForEach: <explanation>
-  ctx.forEach(({ x, type, value }, idx) => {
+  ctx2.forEach(({ x, type, value }, idx) => {
     console.log(
       `  ${idx === 0 ? "[" : ","} ${ppVariable(x)} : ${ppExpr(type)}${
         value ? ` = ${ppExpr(value)}` : ""