From dbad9eb094ebc36b3d6301677a4a11544d01ddee Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 25 Nov 2024 19:49:47 -0600 Subject: [PATCH] stlc --- README.md | 15 ++++ biome.json | 13 --- bun.lockb | Bin 0 -> 3504 bytes package.json | 23 +++--- pnpm-lock.yaml | 146 --------------------------------- stlc-bidir/index.ts | 118 +++++++++++++++++++++++++++ stlc-bidir/simple.test.ts | 65 +++++++++++++++ stlc/index.test.ts | 19 ----- stlc/index.ts | 164 -------------------------------------- tsconfig.json | 27 +++++++ 10 files changed, 235 insertions(+), 355 deletions(-) create mode 100644 README.md delete mode 100644 biome.json create mode 100755 bun.lockb delete mode 100644 pnpm-lock.yaml create mode 100644 stlc-bidir/index.ts create mode 100644 stlc-bidir/simple.test.ts delete mode 100644 stlc/index.test.ts delete mode 100644 stlc/index.ts create mode 100644 tsconfig.json diff --git a/README.md b/README.md new file mode 100644 index 0000000..eab03b7 --- /dev/null +++ b/README.md @@ -0,0 +1,15 @@ +# plsandbox + +To install dependencies: + +```bash +bun install +``` + +To run: + +```bash +bun run index.ts +``` + +This project was created using `bun init` in bun v1.1.26. [Bun](https://bun.sh) is a fast all-in-one JavaScript runtime. diff --git a/biome.json b/biome.json deleted file mode 100644 index 22c6209..0000000 --- a/biome.json +++ /dev/null @@ -1,13 +0,0 @@ -{ - "$schema": "https://biomejs.dev/schemas/1.7.3/schema.json", - "organizeImports": { - "enabled": true - }, - "formatter": { "enabled": true, "indentStyle": "space", "indentWidth": 2 }, - "linter": { - "enabled": true, - "rules": { - "recommended": true - } - } -} diff --git a/bun.lockb b/bun.lockb new file mode 100755 index 0000000000000000000000000000000000000000..d56199f6be4fabb28f2b4d8f9dbc0232d7ac7b22 GIT binary patch literal 3504 zcmd5;drVVT7{9G$XhlTDg=rW?wnnMFeezIhs|+&}6cimg6-R+fd$F{o_m)TJ1A-b5 z7K(Ffbkj{i5i=78z`;7bnQJ?DJC z-#zF1zFvM|p$aGCP^8gT1!c{Zq&cl(7;=j(eQhRfq2!r1N4Alb=PJcQf*|%8l7+h0 zVq@z!YrFkcj7>XOT713m{m^aiJt+R;p|mqWG7f^kMtj{qd?B}P#sQxB7=kDah9`gU zlfa9?SA$3E_rQ+@A0;3NKk!}LI_!DkI@^m6f3N9jG#3aBpPuhXIsM#>hInOB&zrxR z&X!EPF|AUu@-6A{IkU#tbgkV>cAq+MW>>+!tPAwMmkVdgHdARp`%H$if=mV@4$db6 z?}HYGX&7&V_(;H`^Ps^ca!3}8KMIjCJp8mFk=_7|?}h1Xzz2edJfm6+%P{^GIP^Tg zqq|RmG29$r{3gI_0goC3VgKv>n*p!m-tP-|%nOf0+9-%X0~zu_MW8w&j_0^J;zWi# z+UGa$v*G*3_aVan(|}JvczOBMqN>?ZJ8qBJ{HS}!H(T6a&B&VS^I-0=wbN5iFSs|e zY5v0MBh}02#(t;vEj>!K)U*ZUZykT-c&fCnEk2+^dCE|1}Q&uVnZbMYA;!mLmvCr_I|t};ngfZ@tTTu zcSu=j$;6FO_2R2ll`T_}ZF|DQuHRmr*vR8W^~5Hs|GKI3BAse*w&u&`30vKXCzI+g z8ltvRW@CBa?#pb|myzd~jrt?3IdqA#MNrwq=qq;7+EMx)K6yDSWxIL2{5}^+7njF$ ze!#|xYnSA_y+0(mFfiGyx!DraX6U$|%N~iUsSo{m@jD4;Us5z|+Vy&Y&uT@*kcg~*c;q#9xv`=#4Re@u@wI4Qp6j^$cK67YQ82dxroZfp=C(x^dcS;r>?2X-0wgGrY zlHnR-|1@VCVOM&ZD~w1?9rwX(=Db+PIMPYl%CJU@g~W1$T;`xCy+o~)Ftm%ZWzLjn zB}NNvvf4616kzLn>@_q;{d|Yx^h2TmOssQi)Ovva3kj+*`hKBr4eAy28%DpkXb!(( z7(D2`hy!sU9)!nS$d_O)?%ZPCDs^OvGa4=z*?%t8z~xXl(mhz01PIndkV;ZX5Lgjm zWiwi6F|riH5(L&vSo;Y3Kg!j>28@MR1qlTzQblUuA8Z%5gLRNlupyd^AXQ2ND=n;; zU`MSaRcbOCYcH&!U?+l9N0QnnV8VePSq*pZU;6LQuQx+w=TZ)Gem+Y%tVYXH)H*!Y;GB~z!%z<3O!-z)l$06&=o2Um z(u0z1W|J7_yQ*Yl_Vd2F#| z7#TB3GgOY#Xfd;_otdprI4Bd%u#N)KYR}GMNSni?_-mj-{=14.21.3'} - hasBin: true - requiresBuild: true - optionalDependencies: - '@biomejs/cli-darwin-arm64': 1.7.3 - '@biomejs/cli-darwin-x64': 1.7.3 - '@biomejs/cli-linux-arm64': 1.7.3 - '@biomejs/cli-linux-arm64-musl': 1.7.3 - '@biomejs/cli-linux-x64': 1.7.3 - '@biomejs/cli-linux-x64-musl': 1.7.3 - '@biomejs/cli-win32-arm64': 1.7.3 - '@biomejs/cli-win32-x64': 1.7.3 - dev: true - - /@biomejs/cli-darwin-arm64@1.7.3: - resolution: {integrity: sha512-eDvLQWmGRqrPIRY7AIrkPHkQ3visEItJKkPYSHCscSDdGvKzYjmBJwG1Gu8+QC5ed6R7eiU63LEC0APFBobmfQ==} - engines: {node: '>=14.21.3'} - cpu: [arm64] - os: [darwin] - requiresBuild: true - dev: true - optional: true - - /@biomejs/cli-darwin-x64@1.7.3: - resolution: {integrity: sha512-JXCaIseKRER7dIURsVlAJacnm8SG5I0RpxZ4ya3dudASYUc68WGl4+FEN03ABY3KMIq7hcK1tzsJiWlmXyosZg==} - engines: {node: '>=14.21.3'} - cpu: [x64] - os: [darwin] - requiresBuild: true - dev: true - optional: true - - /@biomejs/cli-linux-arm64-musl@1.7.3: - resolution: {integrity: sha512-c8AlO45PNFZ1BYcwaKzdt46kYbuP6xPGuGQ6h4j3XiEDpyseRRUy/h+6gxj07XovmyxKnSX9GSZ6nVbZvcVUAw==} - engines: {node: '>=14.21.3'} - cpu: [arm64] - os: [linux] - requiresBuild: true - dev: true - optional: true - - /@biomejs/cli-linux-arm64@1.7.3: - resolution: {integrity: sha512-phNTBpo7joDFastnmZsFjYcDYobLTx4qR4oPvc9tJ486Bd1SfEVPHEvJdNJrMwUQK56T+TRClOQd/8X1nnjA9w==} - engines: {node: '>=14.21.3'} - cpu: [arm64] - os: [linux] - requiresBuild: true - dev: true - optional: true - - /@biomejs/cli-linux-x64-musl@1.7.3: - resolution: {integrity: sha512-UdEHKtYGWEX3eDmVWvQeT+z05T9/Sdt2+F/7zmMOFQ7boANeX8pcO6EkJPK3wxMudrApsNEKT26rzqK6sZRTRA==} - engines: {node: '>=14.21.3'} - cpu: [x64] - os: [linux] - requiresBuild: true - dev: true - optional: true - - /@biomejs/cli-linux-x64@1.7.3: - resolution: {integrity: sha512-vnedYcd5p4keT3iD48oSKjOIRPYcjSNNbd8MO1bKo9ajg3GwQXZLAH+0Cvlr+eMsO67/HddWmscSQwTFrC/uPA==} - engines: {node: '>=14.21.3'} - cpu: [x64] - os: [linux] - requiresBuild: true - dev: true - optional: true - - /@biomejs/cli-win32-arm64@1.7.3: - resolution: {integrity: sha512-unNCDqUKjujYkkSxs7gFIfdasttbDC4+z0kYmcqzRk6yWVoQBL4dNLcCbdnJS+qvVDNdI9rHp2NwpQ0WAdla4Q==} - engines: {node: '>=14.21.3'} - cpu: [arm64] - os: [win32] - requiresBuild: true - dev: true - optional: true - - /@biomejs/cli-win32-x64@1.7.3: - resolution: {integrity: sha512-ZmByhbrnmz/UUFYB622CECwhKIPjJLLPr5zr3edhu04LzbfcOrz16VYeNq5dpO1ADG70FORhAJkaIGdaVBG00w==} - engines: {node: '>=14.21.3'} - cpu: [x64] - os: [win32] - requiresBuild: true - dev: true - optional: true - - /@types/bun@1.1.1: - resolution: {integrity: sha512-lUe9rLMhgDCViciZtgDj5CMl2u7uTq/IP149kSZH/Si6FWkCioximABFf+baRQgbm8QlH4bzT0qJRteQFNqeGA==} - dependencies: - bun-types: 1.1.6 - dev: true - - /@types/node@20.11.30: - resolution: {integrity: sha512-dHM6ZxwlmuZaRmUPfv1p+KrdD1Dci04FbdEm/9wEMouFqxYoFl5aMkt0VMAUtYRQDyYvD41WJLukhq/ha3YuTw==} - dependencies: - undici-types: 5.26.5 - dev: true - - /@types/ws@8.5.10: - resolution: {integrity: sha512-vmQSUcfalpIq0R9q7uTo2lXs6eGIpt9wtnLdMv9LVpIjCA/+ufZRozlVoVelIYixx1ugCBKDhn89vnsEGOCx9A==} - dependencies: - '@types/node': 20.11.30 - dev: true - - /bun-types@1.1.6: - resolution: {integrity: sha512-LK2aaJdBBTUkDyN+kRiJHLF3VGrAcdkEHrbBvbmTkccShPw6ZalxxKjWSBJwn4UkikhZdrdA87bZWmfUgkRUYg==} - dependencies: - '@types/node': 20.11.30 - '@types/ws': 8.5.10 - dev: true - - /fast-check@3.18.0: - resolution: {integrity: sha512-/951xaT0kA40w0GXRsZXEwSTE7LugjZtSA/8vPgFkiPQ8wNp8tRvqWuNDHBgLxJYXtsK11e/7Q4ObkKW5BdTFQ==} - engines: {node: '>=8.0.0'} - dependencies: - pure-rand: 6.1.0 - dev: true - - /pure-rand@6.1.0: - resolution: {integrity: sha512-bVWawvoZoBYpp6yIoQtQXHZjmz35RSVHnUOTefl8Vcjr8snTPY1wnpSPMWekcFwbxI6gtmT7rSYPFvz71ldiOA==} - dev: true - - /undici-types@5.26.5: - resolution: {integrity: sha512-JlCMO+ehdEIKqlFxk6IfVoAUVmgz7cU7zD/h9XZ0qzeosSHmUJVOzSQvvYSYWXkFXC+IfLKSIffhv0sVZup6pA==} - dev: true diff --git a/stlc-bidir/index.ts b/stlc-bidir/index.ts new file mode 100644 index 0000000..868ef8b --- /dev/null +++ b/stlc-bidir/index.ts @@ -0,0 +1,118 @@ +import { isEqual } from "lodash"; + +export type ty = { kind: "arr"; left: ty; right: ty } | { kind: "unit" }; + +export const unitTy = (): ty => ({ kind: "unit" }); + +export const arr = (left: ty, right: ty): ty => ({ + kind: "arr", + left, + right, +}); + +export type term = + | { kind: "unit" } + | { kind: "var"; name: string } + | { kind: "app"; left: term; right: term } + | { kind: "abs"; arg: string; ty: ty; body: term }; + +export const unit1 = (): term => ({ kind: "unit" }); +export const var1 = (name: string): term => ({ kind: "var", name }); +export const app1 = (left: term, right: term): term => ({ + kind: "app", + left, + right, +}); +export const abs1 = (arg: string, ty: ty, body: term): term => ({ + kind: "abs", + arg, + ty, + body, +}); + +export type term2 = + | { kind: "unit" } + | { kind: "var"; idx: number } + | { kind: "app"; left: term2; right: term2 } + | { kind: "abs"; ty: ty; body: term2 }; + +export const unit2 = (): term2 => ({ kind: "unit" }); +export const var2 = (idx: number): term2 => ({ kind: "var", idx }); +export const app2 = (left: term2, right: term2): term2 => ({ + kind: "app", + left, + right, +}); +export const abs2 = (ty: ty, body: term2): term2 => ({ kind: "abs", ty, body }); + +export function convertToDebruijn(t: term): term2 { + function helper(t: term, ctx: string[]): term2 { + switch (t.kind) { + case "unit": + return { kind: "unit" }; + case "abs": + return { kind: "abs", ty: t.ty, body: helper(t.body, [t.arg, ...ctx]) }; + case "app": + return { + kind: "app", + left: helper(t.left, ctx), + right: helper(t.right, ctx), + }; + case "var": + return { kind: "var", idx: ctx.indexOf(t.name) }; + } + } + + return helper(t, []); +} + +export function infer(t: term2): ty { + function check(t: term2, ty: ty, ctx: ty[]): boolean { + switch (t.kind) { + case "unit": + return ty.kind === "unit"; + case "var": + return isEqual(ctx[t.idx], ty); + case "app": { + const fTy = infer(t.left, ctx); + if (fTy.kind !== "arr") return false; + const fArgTy = fTy.left; + const fBodyTy = fTy.right; + if (!check(t.right, fBodyTy, ctx)) return false; + return true; + } + case "abs": + // ty MUST be a function + if (ty.kind !== "arr") return false; + const { left: tyLeft, right: tyRight } = ty; + // the types must match + if (!isEqual(tyLeft, t.ty)) return false; + return true; + } + } + + function infer(t: term2, ctx: ty[]): ty { + switch (t.kind) { + case "unit": + return { kind: "unit" }; + case "abs": + return { + kind: "arr", + left: t.ty, + right: infer(t.body, [...ctx, t.ty]), + }; + case "var": + return ctx[t.idx]; + case "app": { + const leftTy = infer(t.left, ctx); + if (leftTy.kind !== "arr") throw new Error("not a function"); + if (!check(t.right, leftTy.right, ctx)) + throw new Error("types don't match"); + // TODO: Ensure that the types match + return leftTy.right; + } + } + } + + return infer(t, []); +} diff --git a/stlc-bidir/simple.test.ts b/stlc-bidir/simple.test.ts new file mode 100644 index 0000000..b36ad3c --- /dev/null +++ b/stlc-bidir/simple.test.ts @@ -0,0 +1,65 @@ +import { test, expect, describe } from "bun:test"; +import { + abs1, + abs2, + app1, + app2, + arr, + convertToDebruijn, + infer, + unitTy, + var1, + var2, +} from "."; + +describe("convertToDeBruijn", () => { + test("K combinator", () => { + const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x"))); + const expr2 = abs2(unitTy(), abs2(unitTy(), var2(1))); + + expect(convertToDebruijn(expr)).toEqual(expr2); + }); + + test("S combinator", () => { + const expr = abs1( + "x", + arr(unitTy(), arr(unitTy(), unitTy())), + abs1( + "y", + arr(unitTy(), unitTy()), + abs1( + "z", + unitTy(), + app1(app1(var1("x"), var1("z")), app1(var1("y"), var1("z"))), + ), + ), + ); + const expr2 = abs2( + arr(unitTy(), arr(unitTy(), unitTy())), + abs2( + arr(unitTy(), unitTy()), + abs2(unitTy(), app2(app2(var2(2), var2(0)), app2(var2(1), var2(0)))), + ), + ); + + expect(convertToDebruijn(expr)).toEqual(expr2); + }); +}); + +describe("infer", () => { + test("K combinator", () => { + const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x"))); + const expr2 = convertToDebruijn(expr); + const ty = arr(unitTy(), arr(unitTy(), unitTy())); + + expect(infer(expr2)).toEqual(ty); + }); + + test("K combinator", () => { + const expr = abs1("x", unitTy(), abs1("y", unitTy(), var1("x"))); + const expr2 = convertToDebruijn(expr); + const ty = arr(unitTy(), arr(unitTy(), arr(unitTy(), unitTy()))); + + expect(infer(expr2)).not.toEqual(ty); + }); +}); diff --git a/stlc/index.test.ts b/stlc/index.test.ts deleted file mode 100644 index 5da20a3..0000000 --- a/stlc/index.test.ts +++ /dev/null @@ -1,19 +0,0 @@ -import fc from "fast-check"; -import { describe, expect, test } from "bun:test"; -import { churchEncode, inferType, prettyTerm, prettyType } from "."; - -// Code under test -const contains = (text, pattern) => text.indexOf(pattern) >= 0; - -// Properties -describe("church encoding", () => { - test("well typed", () => { - fc.assert( - fc.property(fc.integer(), (num) => { - const churchNum = churchEncode(num); - console.log(prettyTerm(churchNum)); - console.log(prettyType(inferType(churchNum))); - }), - ); - }); -}); diff --git a/stlc/index.ts b/stlc/index.ts deleted file mode 100644 index 1ccc4bb..0000000 --- a/stlc/index.ts +++ /dev/null @@ -1,164 +0,0 @@ -type Type = - | { kind: "var"; name: string } - | { kind: "arrow"; left: Type; right: Type }; - -type Term = - | { kind: "var"; name: string } - | { kind: "abs"; name: string; ty: Type; body: Term } - | { kind: "app"; func: Term; arg: Term }; - -type TypeEnv = Map; -type TermEnv = Map; - -function substitute(term: Term, name: string, repl: Term): Term { - switch (term.kind) { - case "var": { - if (term.name === name) return repl; - return term; - } - - case "app": { - return { - kind: "app", - func: substitute(term.func, name, repl), - arg: substitute(term.arg, name, repl), - }; - } - - case "abs": { - // The lambda body will shadow this substitution, so throw it away - if (term.name === name) return term; - return { - kind: "abs", - ty: term.ty, - name: term.name, - body: substitute(term.body, name, repl), - }; - } - } -} - -export function tyEqual(t1: Type, t2: Type): boolean { - if (t1.kind === "arrow" && t2.kind === "arrow") { - return tyEqual(t1.left, t2.left) && tyEqual(t1.right, t2.right); - } - if (t1.kind === "var" && t2.kind === "var") { - return t1.name === t2.name; - } - return false; -} - -export function inferType(term: Term): Type { - function inferTypeRec(env: TypeEnv, term: Term): Type { - switch (term.kind) { - case "var": { - const entry = env.get(term.name); - if (!entry) throw new Error("unknown name"); - return entry; - } - - case "abs": { - const newEnv = new Map([...env.entries()]); - newEnv.set(term.name, term.ty); - return tyarr(term.ty, inferTypeRec(newEnv, term.body)); - } - - case "app": { - const funcTy = inferTypeRec(env, term.func); - const argTy = inferTypeRec(env, term.arg); - if (funcTy.kind !== "arrow") throw new Error("not a function"); - if (!tyEqual(funcTy.left, argTy)) throw new Error("arg type mismatch"); - return funcTy.right; - } - } - } - - return inferTypeRec(new Map(), term); -} - -function evalTerm(term: Term): Term { - function evalTermRec(env: TermEnv, term: Term): Term { - switch (term.kind) { - case "app": { - const func = evalTermRec(env, term.func); - - // Require func is a function - if (func.kind !== "abs") throw new Error("applying a non-function"); - - const arg = evalTermRec(env, term.arg); - - return substitute(func.body, func.name, arg); - } - - case "var": { - const entry = env.get(term.name); - if (entry === undefined) throw new Error("unknown name"); - return entry; - } - - case "abs": - return term; - } - } - - return evalTermRec(new Map(), term); -} - -// Printing - -export function prettyTerm(term: Term): string { - switch (term.kind) { - case "abs": - return `(λ ${term.name} : ${prettyType(term.ty)} -> ${prettyTerm( - term.body, - )})`; - case "app": - return `(${prettyTerm(term.func)} ${prettyTerm(term.arg)})`; - case "var": - return term.name; - } -} -export function prettyType(ty: Type): string { - switch (ty.kind) { - case "arrow": - return `(${prettyType(ty.left)} -> ${prettyType(ty.right)})`; - case "var": - return ty.name; - } -} - -// Convenience - -function tyvar(name: string): Type { - return { kind: "var", name }; -} -function tyarr(left: Type, right: Type): Type { - return { kind: "arrow", left, right }; -} -function tvar(name: string): Term { - return { kind: "var", name }; -} -function tabs(name: string, ty: Type, body: Term): Term { - return { kind: "abs", name, ty, body }; -} -function tapp(func: Term, arg: Term): Term { - return { kind: "app", func, arg }; -} - -// Examples - -const Nat: Type = tyvar("Nat"); - -export function churchNumeralTy(): Type { - return tyarr(tyarr(Nat, Nat), tyarr(Nat, Nat)); -} - -export function churchEncode(num: number): Term { - if (!Number.isInteger(num)) throw new Error("not an integer"); - let body = tvar("z"); - let n = num; - while (--n) { - body = tapp(tvar("s"), body); - } - return tabs("s", tyarr(Nat, Nat), tabs("z", Nat, body)); -} diff --git a/tsconfig.json b/tsconfig.json new file mode 100644 index 0000000..238655f --- /dev/null +++ b/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 + } +}