wip

.gitignore

@@ -0,0 +1,175 @@
+# Based on https://raw.githubusercontent.com/github/gitignore/main/Node.gitignore
+
+# Logs
+
+logs
+_.log
+npm-debug.log_
+yarn-debug.log*
+yarn-error.log*
+lerna-debug.log*
+.pnpm-debug.log*
+
+# Caches
+
+.cache
+
+# Diagnostic reports (https://nodejs.org/api/report.html)
+
+report.[0-9]_.[0-9]_.[0-9]_.[0-9]_.json
+
+# Runtime data
+
+pids
+_.pid
+_.seed
+*.pid.lock
+
+# Directory for instrumented libs generated by jscoverage/JSCover
+
+lib-cov
+
+# Coverage directory used by tools like istanbul
+
+coverage
+*.lcov
+
+# nyc test coverage
+
+.nyc_output
+
+# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files)
+
+.grunt
+
+# Bower dependency directory (https://bower.io/)
+
+bower_components
+
+# node-waf configuration
+
+.lock-wscript
+
+# Compiled binary addons (https://nodejs.org/api/addons.html)
+
+build/Release
+
+# Dependency directories
+
+node_modules/
+jspm_packages/
+
+# Snowpack dependency directory (https://snowpack.dev/)
+
+web_modules/
+
+# TypeScript cache
+
+*.tsbuildinfo
+
+# Optional npm cache directory
+
+.npm
+
+# Optional eslint cache
+
+.eslintcache
+
+# Optional stylelint cache
+
+.stylelintcache
+
+# Microbundle cache
+
+.rpt2_cache/
+.rts2_cache_cjs/
+.rts2_cache_es/
+.rts2_cache_umd/
+
+# Optional REPL history
+
+.node_repl_history
+
+# Output of 'npm pack'
+
+*.tgz
+
+# Yarn Integrity file
+
+.yarn-integrity
+
+# dotenv environment variable files
+
+.env
+.env.development.local
+.env.test.local
+.env.production.local
+.env.local
+
+# parcel-bundler cache (https://parceljs.org/)
+
+.parcel-cache
+
+# Next.js build output
+
+.next
+out
+
+# Nuxt.js build / generate output
+
+.nuxt
+dist
+
+# Gatsby files
+
+# Comment in the public line in if your project uses Gatsby and not Next.js
+
+# https://nextjs.org/blog/next-9-1#public-directory-support
+
+# public
+
+# vuepress build output
+
+.vuepress/dist
+
+# vuepress v2.x temp and cache directory
+
+.temp
+
+# Docusaurus cache and generated files
+
+.docusaurus
+
+# Serverless directories
+
+.serverless/
+
+# FuseBox cache
+
+.fusebox/
+
+# DynamoDB Local files
+
+.dynamodb/
+
+# TernJS port file
+
+.tern-port
+
+# Stores VSCode versions used for testing VSCode extensions
+
+.vscode-test
+
+# yarn v2
+
+.yarn/cache
+.yarn/unplugged
+.yarn/build-state.yml
+.yarn/install-state.gz
+.pnp.*
+
+# IntelliJ based IDEs
+.idea
+
+# Finder (MacOS) folder config
+.DS_Store

README.md

@@ -0,0 +1,15 @@
+# inference
+
+To install dependencies:
+
+```bash
+bun install
+```
+
+To run:
+
+```bash
+bun run src/index.ts
+```
+
+This project was created using `bun init` in bun v1.1.29. [Bun](https://bun.sh) is a fast all-in-one JavaScript runtime.

biome.json

@@ -0,0 +1,31 @@
+{
+	"$schema": "https://biomejs.dev/schemas/1.9.4/schema.json",
+	"vcs": {
+		"enabled": false,
+		"clientKind": "git",
+		"useIgnoreFile": false
+	},
+	"files": {
+		"ignoreUnknown": false,
+		"ignore": []
+	},
+	"formatter": {
+		"enabled": true,
+		"indentStyle": "space",
+		"indentWidth": 2
+	},
+	"organizeImports": {
+		"enabled": true
+	},
+	"linter": {
+		"enabled": true,
+		"rules": {
+			"recommended": true
+		}
+	},
+	"javascript": {
+		"formatter": {
+			"quoteStyle": "double"
+		}
+	}
+}

index.html

@@ -0,0 +1,3 @@
+<div id="root"></div>
+
+<script type="module" src="src/index.tsx"></script>

package.json

@@ -0,0 +1,26 @@
+{
+  "name": "inference",
+  "module": "src/index.ts",
+  "type": "module",
+  "devDependencies": {
+    "@biomejs/biome": "^1.9.4",
+    "@types/bun": "latest",
+    "@types/lodash.isequal": "^4.5.8",
+    "@types/react": "^18.3.11",
+    "@types/react-dom": "^18.3.1",
+    "@vitejs/plugin-react": "^4.3.3",
+    "sass": "^1.80.3",
+    "vite": "^5.4.9"
+  },
+  "peerDependencies": {
+    "typescript": "^5.0.0"
+  },
+  "dependencies": {
+    "lodash.isequal": "^4.5.0",
+    "react": "^18.3.1",
+    "react-dom": "^18.3.1"
+  },
+  "trustedDependencies": [
+    "@biomejs/biome"
+  ]
+}

src/App.tsx

@@ -0,0 +1,47 @@
+import { ppJudgement, type rule } from "./lib";
+import {
+  contextVar,
+  ppAnyExpr,
+  type AnyContextEntry,
+  type anyExpr,
+} from "./lib/core";
+import defaultRules from "./lib/defaultRules";
+import type { ContextEntry } from "./lib/pi";
+
+import "./global.scss";
+
+const globalContext: ContextEntry[] = [
+  {
+    x: { kind: "string", name: "Type₀" },
+    type: { kind: "var", x: { kind: "string", name: "Type₁" } },
+  },
+];
+const database: rule[] = [...defaultRules];
+
+interface InferenceRuleProps {
+  rule: rule;
+}
+
+export function InferenceRule({ rule }: InferenceRuleProps) {
+  return (
+    <>
+      <div className="inferenceRule">
+        {rule.premises.map((premise) => (
+          <>{ppJudgement(premise)}</>
+        ))}
+        <hr />
+        <>{ppJudgement(rule.conclusion)}</>
+      </div>
+    </>
+  );
+}
+
+export default function App() {
+  return (
+    <div className="container">
+      {database.map((rule) => (
+        <InferenceRule key={JSON.stringify(rule)} rule={rule} />
+      ))}
+    </div>
+  );
+}

src/global.scss

@@ -0,0 +1,20 @@
+.container {
+    display: flex;
+    flex-direction: row;
+    align-items: center;
+    gap: 8px;
+}
+
+.inferenceRule {
+    border: 1px solid gray; 
+    border-radius: 8px;
+    padding: 8px;
+    box-sizing: border-box;
+    text-align: center;
+    box-shadow: 0px 1px 8px lightgray;
+
+    hr {
+        border: none;
+        border-top: 1px solid gray;
+    }
+}

src/index.tsx

@@ -0,0 +1,5 @@
+import {createRoot} from "react-dom/client"
+import App from "./App";
+
+const root = createRoot(document.getElementById("root")!);
+root.render(<App />)

src/lib/core.ts

@@ -0,0 +1,30 @@
+import {
+  ppContext,
+  ppContextEntry,
+  ppExpr,
+  type context,
+  type ContextEntry,
+  type expr,
+} from "./pi";
+
+const _contextVar = Symbol("contextvar");
+type ContextVar = { [_contextVar]: true; name: string };
+export function contextVar(name: string): AnyContextEntry {
+  return { kind: "contextvar", name };
+}
+
+export type AnyContextEntry =
+  | { kind: "contextentry"; entry: ContextEntry }
+  | { kind: "contextvar"; name: string };
+
+export type anyExpr = expr | { kind: "context"; context: AnyContextEntry[] };
+
+export function ppAnyExpr(e: anyExpr): string {
+  if (e.kind === "context") {
+    return e.context
+      .map((ce) =>
+        ce.kind === "contextvar" ? ce.name : ppContextEntry(ce.entry)
+      )
+      .join(",");
+  } else return ppExpr(e);
+}

src/lib/defaultJudgements.ts

@@ -0,0 +1,15 @@
+import { ppAnyExpr } from "./core";
+import type { judgementKind } from "./judgements";
+
+const defaultJudgements: [string, judgementKind][] = [
+  [
+    "contextHas",
+    {
+      arity: 3,
+      pp: ([ctx, term, type]) =>
+        `${ppAnyExpr(ctx)} ⊢ ${ppAnyExpr(term)} : ${ppAnyExpr(type)}`,
+    },
+  ],
+];
+
+export default defaultJudgements;

src/lib/defaultRules.ts

@@ -0,0 +1,58 @@
+import type { rule } from ".";
+import { contextVar, ppAnyExpr } from "./core";
+
+const defaultRules: rule[] = [
+  {
+    premises: [],
+    conclusion: {
+      kind: "contextHas",
+      args: [
+        { kind: "context", context: [contextVar("Γ")] },
+        { kind: "var", x: { kind: "string", name: "ℕ" } },
+        { kind: "var", x: { kind: "string", name: "Type₀" } },
+      ],
+    },
+    vars: ["Γ"],
+  },
+
+  {
+    premises: [],
+    conclusion: {
+      kind: "contextHas",
+      args: [
+        { kind: "context", context: [contextVar("Γ")] },
+        { kind: "var", x: { kind: "string", name: "zero" } },
+        { kind: "var", x: { kind: "string", name: "ℕ" } },
+      ],
+    },
+    vars: ["Γ"],
+  },
+
+  {
+    premises: [
+      {
+        kind: "contextHas",
+        args: [
+          { kind: "context", context: [contextVar("Γ")] },
+          { kind: "var", x: { kind: "string", name: "n" } },
+          { kind: "var", x: { kind: "string", name: "ℕ" } },
+        ],
+      },
+    ],
+    conclusion: {
+      kind: "contextHas",
+      args: [
+        { kind: "context", context: [contextVar("Γ")] },
+        {
+          kind: "app",
+          left: { kind: "var", x: { kind: "string", name: "suc" } },
+          right: { kind: "var", x: { kind: "string", name: "n" } },
+        },
+        { kind: "var", x: { kind: "string", name: "ℕ" } },
+      ],
+    },
+    vars: ["Γ", "n"],
+  },
+];
+
+export default defaultRules;

src/lib/index.ts

@@ -0,0 +1,20 @@
+import { ppAnyExpr, type anyExpr } from "./core";
+import defaultJudgements from "./defaultJudgements";
+import type { judgement, judgementKind } from "./judgements";
+
+export const judgementKinds = new Map<string, judgementKind>();
+for (const [name, kind] of defaultJudgements) {
+  judgementKinds.set(name, kind);
+}
+
+export function ppJudgement(j: judgement): string {
+  const kind = judgementKinds.get(j.kind);
+  if (!kind) throw new Error(`could not find judgement kind ${j.kind}`);
+  return kind.pp(j.args);
+}
+
+export type rule = {
+  premises: judgement[];
+  conclusion: judgement;
+  vars: string[];
+};

src/lib/judgements.ts

@@ -0,0 +1,8 @@
+import type { anyExpr } from "./core";
+
+export type judgementKind = { arity: number; pp: (args: anyExpr[]) => string };
+
+export type judgement = {
+  kind: string;
+  args: anyExpr[];
+};

src/lib/pi.ts

@@ -0,0 +1,400 @@
+import isEqual from "lodash.isequal";
+
+export type expr =
+  | { kind: "var"; x: variable }
+  | { kind: "universe"; level: number }
+  | { kind: "pi"; abs: abstraction }
+  | { kind: "lambda"; abs: abstraction }
+  | { kind: "app"; left: expr; right: expr };
+
+export interface abstraction {
+  x: variable;
+  type: expr;
+  body: expr;
+}
+
+// =============================================================================
+// Substitution
+
+export type variable =
+  | { kind: "string"; name: string }
+  | { kind: "gensym"; name: string; n: number }
+  | { kind: "dummy" };
+
+export interface Substitution {
+  x: variable;
+  repl: expr;
+}
+
+let ctr = 0;
+export function refresh(v: variable): variable {
+  const n = ctr + 1;
+  ctr += 1;
+  switch (v.kind) {
+    case "gensym":
+    case "string": {
+      return { kind: "gensym", name: v.name, n };
+    }
+    case "dummy":
+      return { kind: "gensym", name: "_", n };
+  }
+}
+
+export function subst(s: Substitution[], e: expr): expr {
+  switch (e.kind) {
+    case "var":
+      return s.find((sub) => isEqual(sub.x, e.x))?.repl ?? e;
+    case "universe":
+      return e;
+    case "pi":
+      return { kind: "pi", abs: substAbstraction(s, e.abs) };
+    case "lambda":
+      return { kind: "lambda", abs: substAbstraction(s, e.abs) };
+    case "app":
+      return { kind: "app", left: subst(s, e.left), right: subst(s, e.right) };
+  }
+}
+
+export function substAbstraction(
+  s: Substitution[],
+  { x, type, body }: abstraction
+): abstraction {
+  const x2 = refresh(x);
+  return {
+    x: x2,
+    type: subst(s, type),
+    body: subst([{ x, repl: { kind: "var", x: x2 } }, ...s], body),
+  };
+}
+
+// =============================================================================
+// Type inference
+
+export type context = ContextEntry[];
+
+export interface ContextEntry {
+  x: variable;
+  type: expr;
+  value?: expr | undefined;
+}
+
+/** Returns the type of the definition associated with `x` inside the context `ctx` */
+export function lookupTy(x: variable, ctx: context): expr {
+  const res = ctx.find((entry) => isEqual(entry.x, x));
+  if (res === undefined)
+    throw new Error(
+      `unknown identifier ${ppVariable(x)} (ctx: ${ppContext(ctx)})`
+    );
+  return res.type;
+}
+
+/** Returns the value of the definition associated with `x` inside the context `ctx` */
+export function lookupValue(x: variable, ctx: context): expr | null {
+  const res = ctx.find((entry) => isEqual(entry.x, x));
+  if (res === undefined)
+    throw new Error(
+      `unknown identifier ${ppVariable(x)} (ctx: ${ppContext(ctx)})`
+    );
+  return res.value ?? null;
+}
+
+export function extend(
+  x: variable,
+  t: expr,
+  value: expr | undefined,
+  ctx: context
+): context {
+  return [...ctx, { x: x, type: t, value }];
+}
+
+/** Infer the type of the expression `e` in context `ctx` */
+export function inferType(ctx: context, e: expr): expr {
+  function inferType(ctx: context, e: expr): expr {
+    switch (e.kind) {
+      case "var": {
+        const ty = lookupTy(e.x, ctx);
+        return ty;
+      }
+      case "universe":
+        return { kind: "universe", level: e.level + 1 };
+      case "pi": {
+        const { x, type, body } = e.abs;
+        const k1 = inferUniverse(ctx, type);
+        const k2 = inferUniverse(extend(x, type, undefined, ctx), body);
+        return { kind: "universe", level: Math.max(k1, k2) };
+      }
+      case "lambda": {
+        const { x, type, body } = e.abs;
+        inferUniverse(ctx, type);
+        const te = inferType(extend(x, type, undefined, ctx), body);
+        return { kind: "pi", abs: { x, type, body: te } };
+      }
+      case "app": {
+        const { x, type, body } = inferPi(ctx, e.left);
+        const te = inferType(ctx, e.right);
+        checkEqual(ctx, type, te);
+        return subst([{ x, repl: e.right }], body);
+      }
+    }
+  }
+
+  const result = inferType(ctx, e);
+  return result;
+}
+
+export function inferUniverse(ctx: context, t: expr): number {
+  const u = inferType(ctx, t);
+  const n = normalize(ctx, u);
+  switch (n.kind) {
+    case "universe":
+      return n.level;
+    default:
+      throw new Error("type expected.");
+  }
+}
+
+export function inferPi(ctx: context, e: expr): abstraction {
+  const t = inferType(ctx, e);
+  const n = normalize(ctx, t);
+  switch (n.kind) {
+    case "pi":
+      return n.abs;
+    default:
+      throw new Error("function expected");
+  }
+}
+
+export function checkEqual(ctx: context, e1: expr, e2: expr) {
+  if (!equal(ctx, e1, e2))
+    throw new Error(`expressions ${e1} and ${e2} not equal`);
+}
+
+// =============================================================================
+// Normalization and equality
+
+export function normalize(ctx: context, e: expr): expr {
+  function normalize(ctx: context, e: expr): expr {
+    switch (e.kind) {
+      case "var": {
+        const n = lookupValue(e.x, ctx);
+        return n ? normalize(ctx, n) : e;
+      }
+      case "app": {
+        const e1 = normalize(ctx, e.left);
+        const e2 = normalize(ctx, e.right);
+        switch (e1.kind) {
+          case "lambda": {
+            const { x, body } = e1.abs;
+            return normalize(ctx, subst([{ x, repl: e2 }], body));
+          }
+          default:
+            return { kind: "app", left: e1, right: e2 };
+        }
+      }
+      case "universe":
+        return { kind: "universe", level: e.level };
+      case "pi":
+        return { kind: "pi", abs: normalizeAbstraction(ctx, e.abs) };
+      case "lambda":
+        return { kind: "lambda", abs: normalizeAbstraction(ctx, e.abs) };
+    }
+  }
+
+  const result = normalize(ctx, e);
+  return result;
+}
+
+export function normalizeAbstraction(
+  ctx: context,
+  { x, type, body }: abstraction
+): abstraction {
+  const t = normalize(ctx, type);
+  return { x, type: t, body: normalize(extend(x, t, undefined, ctx), body) };
+}
+
+export function equal(ctx: context, e1: expr, e2: expr): boolean {
+  function equalHelper(e1: expr, e2: expr): boolean {
+    if (e1.kind === "var" && e2.kind === "var") return isEqual(e1.x, e2.x);
+    if (e1.kind === "app" && e2.kind === "app")
+      return equalHelper(e1.left, e2.left) && equalHelper(e1.right, e2.right);
+    if (e1.kind === "universe" && e2.kind === "universe")
+      return e1.level === e2.level;
+    if (e1.kind === "pi" && e2.kind === "pi")
+      return equalAbstraction(e1.abs, e2.abs);
+    if (e1.kind === "lambda" && e2.kind === "lambda")
+      return equalAbstraction(e1.abs, e2.abs);
+    return false;
+  }
+
+  function equalAbstraction(
+    { x, type: type1, body: body1 }: abstraction,
+    { x: y, type: type2, body: body2 }: abstraction
+  ): boolean {
+    return (
+      equalHelper(type1, type2) &&
+      equalHelper(body1, subst([{ x: y, repl: { kind: "var", x } }], body2))
+    );
+  }
+
+  return equalHelper(normalize(ctx, e1), normalize(ctx, e2));
+}
+
+// =============================================================================
+// Pretty printing
+
+export function ppVariable(v: variable): string {
+  switch (v.kind) {
+    case "string":
+      return `${v.name}`;
+    case "gensym":
+      return `?${v.name}$${v.n}`;
+    case "dummy":
+      return "_";
+  }
+}
+
+function occursIn(x: variable, e: expr): boolean {
+  switch (e.kind) {
+    case "var":
+      return isEqual(e.x, x);
+    case "universe":
+      return false;
+    case "pi":
+    case "lambda":
+      if (occursIn(x, e.abs.type)) return true;
+      if (!isEqual(e.abs.x, x)) return occursIn(x, e.abs.body);
+      return false;
+    case "app":
+      return occursIn(x, e.left) || occursIn(x, e.right);
+  }
+}
+
+export function ppExpr(e: expr): string {
+  switch (e.kind) {
+    case "var":
+      return ppVariable(e.x);
+    case "universe":
+      if (e.level === 0) return "U";
+      return `U(${e.level})`;
+    case "pi":
+      if (occursIn(e.abs.x, e.abs.body)) {
+        return `(∏ (${ppVariable(e.abs.x)} : ${ppExpr(e.abs.type)}), ${ppExpr(
+          e.abs.type
+        )})`;
+      }
+      return `(${ppExpr(e.abs.type)} → ${ppExpr(e.abs.body)})`;
+    case "lambda":
+      return `(λ (${ppVariable(e.abs.x)} : ${ppExpr(e.abs.type)}), ${ppExpr(
+        e.abs.body
+      )})`;
+    case "app":
+      return `(${ppExpr(e.left)} ${ppExpr(e.right)})`;
+  }
+}
+
+export function ppContextEntry({ x, type, value }: ContextEntry): string {
+  return `${ppVariable(x)} : ${ppExpr(type)}${
+    value ? ` = ${ppExpr(value)}` : ""
+  }`;
+}
+export function ppContext(ctx: context): string {
+  const ss = ctx.map(ppContextEntry);
+
+  return `[${ss.join(", ")}]`;
+}
+
+// =============================================================================
+// Testing
+
+function test() {
+  const ctx: context = [];
+
+  const dummy: variable = { kind: "dummy" };
+  const varify = (name: string): expr => ({
+    kind: "var",
+    x: { kind: "string", name },
+  });
+  const define = (name: string, e: expr) => {
+    const type = inferType(ctx, e);
+    ctx.push({ x: { kind: "string", name }, type, value: e });
+  };
+
+  // N : Set lzero
+  ctx.push({
+    x: { kind: "string", name: "N" },
+    type: { kind: "universe", level: 0 },
+  });
+  const N = varify("N");
+
+  // z : N
+  ctx.push({ x: { kind: "string", name: "z" }, type: N });
+  const z = varify("z");
+
+  // s : N -> N
+  const NtoN: expr = { kind: "pi", abs: { x: dummy, type: N, body: N } };
+  ctx.push({
+    x: { kind: "string", name: "s" },
+    type: NtoN,
+  });
+  const s = varify("s");
+
+  const f = varify("f");
+  const x = varify("x");
+  const threeExpr: expr = {
+    kind: "lambda",
+    abs: {
+      x: { kind: "string", name: "f" },
+      type: NtoN,
+      body: {
+        kind: "lambda",
+        abs: {
+          x: { kind: "string", name: "x" },
+          type: N,
+          body: {
+            kind: "app",
+            left: f,
+            right: {
+              kind: "app",
+              left: f,
+              right: { kind: "app", left: f, right: x },
+            },
+          },
+        },
+      },
+    },
+  };
+  const three = varify("three");
+  define("three", threeExpr);
+
+  const nineExpr: expr = {
+    kind: "app",
+    left: three,
+    right: {
+      kind: "app",
+      left: three,
+      right: s,
+    },
+  };
+  const nine = varify("nine");
+  define("nine", nineExpr);
+
+  const evaled: expr = {
+    kind: "app",
+    left: nine,
+    right: z,
+  };
+  define("result", normalize(ctx, evaled));
+
+  console.log("ctx =");
+  // biome-ignore lint/complexity/noForEach: <explanation>
+  ctx.forEach(({ x, type, value }, idx) => {
+    console.log(
+      `  ${idx === 0 ? "[" : ","} ${ppVariable(x)} : ${ppExpr(type)}${
+        value ? ` = ${ppExpr(value)}` : ""
+      }`
+    );
+  });
+  console.log("  ]");
+}
+
+// test();

tsconfig.json

@@ -0,0 +1,27 @@
+{
+  "compilerOptions": {
+    // Enable latest features
+    "lib": ["ESNext", "DOM"],
+    "target": "ESNext",
+    "module": "ESNext",
+    "moduleDetection": "force",
+    "jsx": "react-jsx",
+    "allowJs": true,
+
+    // Bundler mode
+    "moduleResolution": "bundler",
+    "allowImportingTsExtensions": true,
+    "verbatimModuleSyntax": true,
+    "noEmit": true,
+
+    // Best practices
+    "strict": true,
+    "skipLibCheck": true,
+    "noFallthroughCasesInSwitch": true,
+
+    // Some stricter flags (disabled by default)
+    "noUnusedLocals": false,
+    "noUnusedParameters": false,
+    "noPropertyAccessFromIndexSignature": false
+  }
+}

vite.config.ts

@@ -0,0 +1,6 @@
+import { defineConfig } from "vite";
+import react from "@vitejs/plugin-react";
+
+export default defineConfig({
+  plugins: [react()],
+});