diff --git a/.gitignore b/.gitignore index 6c57e11..1454376 100644 --- a/.gitignore +++ b/.gitignore @@ -2,7 +2,11 @@ *.pdf _build +*.bs.mjs *.bs.js node_modules -lib/bs \ No newline at end of file +lib/bs + +__tests__/**/*.mjs +src/**/*.mjs \ No newline at end of file diff --git a/__tests__/terms_test.res b/__tests__/terms_test.res new file mode 100644 index 0000000..099b1fc --- /dev/null +++ b/__tests__/terms_test.res @@ -0,0 +1,17 @@ +open Jest +open Belt +open Data +open Bidir + +open Expect +open! Expect.Operators + +let mapFirst = a => a->Result.map(((x, _)) => x) + +test("id", () => { + let id: term = Lam("x", Var("x")) + let ctx = list{} + let typ = synthesize(ctx, id)->mapFirst + Js.Console.error2("output: ", typ) + expect(typ) === Ok(TPolytype("ex0", TArrow(TVar("ex0"), TVar("ex0")))) +}) diff --git a/babel.config.js b/babel.config.js new file mode 100644 index 0000000..805b799 --- /dev/null +++ b/babel.config.js @@ -0,0 +1,9 @@ +module.exports = { + presets: [ + [ + "@babel/preset-env", + { targets: { node: "current", esmodules: false }, modules: "cjs" }, + ], + ], + plugins: [], +}; diff --git a/bidir-writeup.typ b/bidir-writeup.typ new file mode 100644 index 0000000..dfb1923 --- /dev/null +++ b/bidir-writeup.typ @@ -0,0 +1,3 @@ += Expressions + +- $ id : forall a. a arrow.r a $ diff --git a/bsconfig.json b/bsconfig.json index 928db21..2bac544 100644 --- a/bsconfig.json +++ b/bsconfig.json @@ -1,17 +1,17 @@ { "name": "your-project-name", + "bsc-flags": [], "sources": [ - { - "dir": "src", - "subdirs": true - } + { "dir": "src", "subdirs": true }, + { "dir": "__tests__", "subdirs": true, "type": "dev" } ], "package-specs": [ { - "module": "es6", + "module": "commonjs", "in-source": true } ], "suffix": ".bs.js", - "bs-dependencies": [] + "bs-dependencies": [], + "bs-dev-dependencies": ["@glennsl/bs-jest"] } diff --git a/bun.lockb b/bun.lockb index 338c8ef..3f57b2a 100755 Binary files a/bun.lockb and b/bun.lockb differ diff --git a/jest.config.json b/jest.config.json new file mode 100644 index 0000000..2428146 --- /dev/null +++ b/jest.config.json @@ -0,0 +1,10 @@ +{ + "verbose": true, + "moduleFileExtensions": ["js", "mjs"], + "extensionsToTreatAsEsm": [".bs.mjs"], + "testMatch": ["**/__tests__/**/*_test.mjs", "**/__tests__/**/*_test.bs.js"], + "transform": { + "^.+.m?js$": "babel-jest" + }, + "transformIgnorePatterns": ["node_modules/(?!(rescript)/)"] +} diff --git a/package.json b/package.json index f033ba3..ee023c3 100644 --- a/package.json +++ b/package.json @@ -1,9 +1,14 @@ { "scripts": { "res:build": "rescript", - "res:dev": "rescript build -w" + "res:dev": "rescript build -w", + "test": "retest lib/**/*.mjs" }, "devDependencies": { - "rescript": "^10.1.4" + "@glennsl/bs-jest": "^0.7.0", + "jest": "^29.7.0", + "rescript": "^10.1.4", + "rescript-js": "^1.0.0-beta.2", + "rescript-test": "^5.0.0" } } diff --git a/src/bidir.res b/src/bidir.res index 1eeb97e..51bef48 100644 --- a/src/bidir.res +++ b/src/bidir.res @@ -5,7 +5,7 @@ let _genSymCtr = ref(0) let genSym = (~prefix="var", ()): string => { let num = _genSymCtr.contents _genSymCtr := num + 1 - `${prefix}${Int.toString(num)}` + `${prefix}${num->Int.toString}` } let rec isSubtype = (ctx: context, tyA: typ, tyB: typ): result => { @@ -17,31 +17,30 @@ let rec isSubtype = (ctx: context, tyA: typ, tyB: typ): result and typecheck = (ctx: context, term: term, typ: typ): result => { switch (term, typ) { // 1I rule - | (Unit, Unit) => Ok(ctx) + | (Unit, TUnit) => Ok(ctx) // ∀I rule - | (e, Polytype(x, tyA)) => failwith("TODO") + | (e, TPolytype(x, tyA)) => failwith("TODO ∀I-rule") // →I rule - | (Lam(x, e), Arrow(tyA, tyB)) => + | (Lam(x, e), TArrow(tyA, tyB)) => let augmentedCtx = ctx->List.add(TermAnnot(x, tyA)) typecheck(augmentedCtx, e, tyB)->Result.map(_ => ctx) // Sub rule - // TODO: Subtyping rule??? - - | (Var(_) | Lam(_, _) | App(_, _) | Annot(_, _), _) => failwith("TODO") - | _ => Error("could not resolve") + | (_, _) => + let tyA = synthesize(ctx, term) + let tyA' = applyContext(ctx, tyA) } } and synthesize = (ctx: context, term: term): result<(typ, context), string> => { switch term { // Var rule - | Var(name) => Ok(lookupTypeVariable(ctx, name), ctx) + | Var(name) => lookupTypeVariable(ctx, name)->Result.map(ty => (ty, ctx)) // 1I⇒ rule - | Unit => Ok(Unit, ctx) + | Unit => Ok(TUnit, ctx) // Anno rule | Annot(e, tyA) => typecheck(ctx, e, tyA)->Result.map(ctx => (tyA, ctx)) @@ -51,35 +50,39 @@ and synthesize = (ctx: context, term: term): result<(typ, context), string> => { // TODO: Check x and e let exA = genSym(~prefix="ex", ()) let exB = genSym(~prefix="ex", ()) - Ok(Arrow(Existential(exA), Existential(exB)), ctx) + let augmentedCtx = list{TermAnnot(x, TVar(exA)), TypeVar(exB), TypeVar(exA), ...ctx} + typecheck(augmentedCtx, e, TVar(exB))->Result.map(_ => ( + TArrow(TExistential(exA), TExistential(exB)), + ctx, + )) // →E rule - | App(e1, e2) => failwith("TODO") + | App(e1, e2) => synthesize(ctx, e1)->Result.flatMap(((tyA, ctx)) => appSynthesize(ctx, tyA, e2)) } } and appSynthesize = (ctx: context, funTy: typ, term: term): result<(typ, context), string> => { switch (funTy, term) { // →App rule - | (Arrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx)) + | (TArrow(tyA, tyC), e) => typecheck(ctx, e, tyA)->Result.map(_ => (tyC, ctx)) // ∀App rule - | (Polytype(a, tyA), e) => failwith("TODO") + | (TPolytype(a, tyA), e) => failwith("TODO") // âApp rule - | (Existential(_), _) => failwith("TODO") + | (TExistential(_), _) => failwith("TODO") - | (Unit | Var(_), _) => Error("trying to appSynthesize with a non-function type") + | (TUnit | TVar(_), _) => Error("trying to appSynthesize with a non-function type") } } // Figure 8. Applying a context, as a substitution, to a type -let rec applyContext = (ctx: context, typ: typ): typ => { +and applyContext = (ctx: context, typ: typ): typ => { switch typ { - | Unit => Unit - | Var(x) => Var(x) - | Existential(_) => failwith("TODO") - | Polytype(_) => failwith("TODO") - | Arrow(a, b) => Arrow(applyContext(ctx, a), applyContext(ctx, b)) + | TUnit => TUnit + | TVar(x) => TVar(x) + | TExistential(_) => failwith("TODO") + | TPolytype(_) => failwith("TODO") + | TArrow(a, b) => TArrow(applyContext(ctx, a), applyContext(ctx, b)) } } diff --git a/src/data.res b/src/data.res index d47b15c..d64a93a 100644 --- a/src/data.res +++ b/src/data.res @@ -1,6 +1,3 @@ -// Disable warning about the same constructor for different types -@@warning("-30") - type rec term = | Unit // () | Var(string) // x @@ -9,18 +6,18 @@ type rec term = | Annot(term, typ) // (e : A) and typ = - | Unit // 1 - | Var(string) // α - | Existential(string) // â - | Polytype(string, typ) // ∀α.A - | Arrow(typ, typ) // A -> B + | TUnit // 1 + | TVar(string) // α + | TExistential(string) // â + | TPolytype(string, typ) // ∀α.A + | TArrow(typ, typ) // A -> B and monotyp = // Unit monotype - | Unit // 1 - | Var(string) // α - | Existential(string) // â - | Arrow(monotyp, monotyp) // τ -> σ + | MUnit // 1 + | MVar(string) // α + | MExistential(string) // â + | MArrow(monotyp, monotyp) // τ -> σ type rec contextEntry = | TypeVar(string) // Γ,α @@ -30,20 +27,18 @@ type rec contextEntry = | Marker(string) // Γ,🢒â type rec completeContextEntry = - | TypeVar(string) // Ω,α - | TermAnnot(string, typ) // Ω,x:A - | ExistentialSolved(string, monotyp) // Ω,â=τ - | Marker(string) // Ω,🢒â + | CCTypeVar(string) // Ω,α + | CCTermAnnot(string, typ) // Ω,x:A + | CCExistentialSolved(string, monotyp) // Ω,â=τ + | CCMarker(string) // Ω,🢒â type context = list -@@warning("+30") - /** Context lookup */ -let rec lookupTypeVariable = (ctx: list, name: string): typ => { +let rec lookupTypeVariable = (ctx: list, name: string): result => { switch ctx { - | list{} => failwith("L") - | list{TermAnnot(n, t), ..._} if n == name => t + | list{} => Error(`could not find name ${name}`) + | list{TermAnnot(n, t), ..._} if n == name => Ok(t) | list{_, ...rest} => lookupTypeVariable(rest, name) } }