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 0000000..d56199f Binary files /dev/null and b/bun.lockb differ diff --git a/package.json b/package.json index df5ccf7..fc46a80 100644 --- a/package.json +++ b/package.json @@ -1,17 +1,14 @@ { "name": "plsandbox", - "version": "1.0.0", - "description": "", - "main": "index.js", - "scripts": { - "test": "echo \"Error: no test specified\" && exit 1" - }, - "keywords": [], - "author": "", - "license": "ISC", + "module": "index.ts", + "type": "module", "devDependencies": { - "@biomejs/biome": "^1.7.3", - "@types/bun": "^1.1.1", - "fast-check": "^3.18.0" + "@types/bun": "latest" + }, + "peerDependencies": { + "typescript": "^5.0.0" + }, + "dependencies": { + "lodash.isequal": "^4.5.0" } -} +} \ No newline at end of file diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml deleted file mode 100644 index ce1f09c..0000000 --- a/pnpm-lock.yaml +++ /dev/null @@ -1,146 +0,0 @@ -lockfileVersion: '6.0' - -settings: - autoInstallPeers: true - excludeLinksFromLockfile: false - -devDependencies: - '@biomejs/biome': - specifier: ^1.7.3 - version: 1.7.3 - '@types/bun': - specifier: ^1.1.1 - version: 1.1.1 - fast-check: - specifier: ^3.18.0 - version: 3.18.0 - -packages: - - /@biomejs/biome@1.7.3: - resolution: {integrity: sha512-ogFQI+fpXftr+tiahA6bIXwZ7CSikygASdqMtH07J2cUzrpjyTMVc9Y97v23c7/tL1xCZhM+W9k4hYIBm7Q6cQ==} - engines: {node: '>=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 + } +}