From c3c801896f8440345653e5b1a3ab016cf5f5bee4 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 11 May 2024 02:49:40 -0500 Subject: [PATCH] initial --- .gitignore | 1 + biome.json | 13 ++++ package.json | 17 +++++ pnpm-lock.yaml | 146 ++++++++++++++++++++++++++++++++++++++++ stlc/index.test.ts | 19 ++++++ stlc/index.ts | 164 +++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 360 insertions(+) create mode 100644 .gitignore create mode 100644 biome.json create mode 100644 package.json create mode 100644 pnpm-lock.yaml create mode 100644 stlc/index.test.ts create mode 100644 stlc/index.ts diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..b512c09 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +node_modules \ No newline at end of file diff --git a/biome.json b/biome.json new file mode 100644 index 0000000..22c6209 --- /dev/null +++ b/biome.json @@ -0,0 +1,13 @@ +{ + "$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/package.json b/package.json new file mode 100644 index 0000000..df5ccf7 --- /dev/null +++ b/package.json @@ -0,0 +1,17 @@ +{ + "name": "plsandbox", + "version": "1.0.0", + "description": "", + "main": "index.js", + "scripts": { + "test": "echo \"Error: no test specified\" && exit 1" + }, + "keywords": [], + "author": "", + "license": "ISC", + "devDependencies": { + "@biomejs/biome": "^1.7.3", + "@types/bun": "^1.1.1", + "fast-check": "^3.18.0" + } +} diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml new file mode 100644 index 0000000..ce1f09c --- /dev/null +++ b/pnpm-lock.yaml @@ -0,0 +1,146 @@ +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/index.test.ts b/stlc/index.test.ts new file mode 100644 index 0000000..5da20a3 --- /dev/null +++ b/stlc/index.test.ts @@ -0,0 +1,19 @@ +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 new file mode 100644 index 0000000..1ccc4bb --- /dev/null +++ b/stlc/index.ts @@ -0,0 +1,164 @@ +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)); +}