From 2d31adff524070bbebc79d3e0e45e327f77dfbe3 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 1 Nov 2023 15:22:03 -0500 Subject: [PATCH] update --- .gitignore | 6 +++- bsconfig.json | 17 ++++++++++ bun.lockb | Bin 0 -> 1383 bytes package.json | 9 ++++++ src/bidir.res | 85 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/data.res | 49 +++++++++++++++++++++++++++++ src/index.res | 3 ++ 7 files changed, 168 insertions(+), 1 deletion(-) create mode 100644 bsconfig.json create mode 100755 bun.lockb create mode 100644 package.json create mode 100644 src/bidir.res create mode 100644 src/data.res create mode 100644 src/index.res diff --git a/.gitignore b/.gitignore index 3618313..6c57e11 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,8 @@ .DS_Store *.pdf -_build \ No newline at end of file +_build +*.bs.js + +node_modules +lib/bs \ No newline at end of file diff --git a/bsconfig.json b/bsconfig.json new file mode 100644 index 0000000..928db21 --- /dev/null +++ b/bsconfig.json @@ -0,0 +1,17 @@ +{ + "name": "your-project-name", + "sources": [ + { + "dir": "src", + "subdirs": true + } + ], + "package-specs": [ + { + "module": "es6", + "in-source": true + } + ], + "suffix": ".bs.js", + "bs-dependencies": [] +} diff --git a/bun.lockb b/bun.lockb new file mode 100755 index 0000000000000000000000000000000000000000..338c8ef5041b56121d67a9b596bea1959778e32a GIT binary patch literal 1383 zcmY#Z)GsYA(of3F(@)JSQ%EY!;{sycoc!eMw9K4T-L(9o+{6;yG6OCq1_lPVZ@iD@ zq;Kp$u=4tnQ)_2ldMtJI;8mSMP2FGqXOy@1CtPO%DgpwKS`grXP;j~d%CCYcfbtm_ zic*V{i!uvJU;?K@o_Z%u+U&px6CjnoHJ=Hj7iN(dkZsAp(7*+xLE=z{0$GFsNIkMU zQ2GD({~=2fHjXG2j0_NSk&R{%30mrXf$eYA>8hz~PV*i7!SB44!9T+Ju#M4z)_C)) zypx8q78x9Rvgpu8e zMH-9H0cg}*fzn(y#YM?_nR&$}i8(oXumq?VQk0r%r(k5DP@GwnnxCelV4{$ilbN2E zp9YFbF!=W$0ze$FJD4HjEKr)urqtNT4yX}_5e86oCPb(QnV$hw*92D|ZDbZ(Y5{bn z8Qcy-RA<7{H!NLqz!E0I1*jZ zC>A9ZCxboD5_rM2uw=_YOny;nT5btLUcH}bu3UFiQZXtYq?r?#PqO3x`5SoMxdLP} z@B;a-y4K`Gyk&id?hkZ+1JoDi;l2Tdiy^LHVMr=2DN0NR`Y9(fNgvM1C@Co@w$j%x tN=?rMDyY=UE6B|%*2^zS2MR$73VmHTQ`gWy&rr`quOz(+?Ds)P001$Q`T_s| literal 0 HcmV?d00001 diff --git a/package.json b/package.json new file mode 100644 index 0000000..f033ba3 --- /dev/null +++ b/package.json @@ -0,0 +1,9 @@ +{ + "scripts": { + "res:build": "rescript", + "res:dev": "rescript build -w" + }, + "devDependencies": { + "rescript": "^10.1.4" + } +} diff --git a/src/bidir.res b/src/bidir.res new file mode 100644 index 0000000..1eeb97e --- /dev/null +++ b/src/bidir.res @@ -0,0 +1,85 @@ +open Belt +open Data + +let _genSymCtr = ref(0) +let genSym = (~prefix="var", ()): string => { + let num = _genSymCtr.contents + _genSymCtr := num + 1 + `${prefix}${Int.toString(num)}` +} + +let rec isSubtype = (ctx: context, tyA: typ, tyB: typ): result => { + switch (tyA, tyB) { + | (_, _) => failwith("TODO") + } +} + +and typecheck = (ctx: context, term: term, typ: typ): result => { + switch (term, typ) { + // 1I rule + | (Unit, Unit) => Ok(ctx) + + // ∀I rule + | (e, Polytype(x, tyA)) => failwith("TODO") + + // →I rule + | (Lam(x, e), Arrow(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") + } +} + +and synthesize = (ctx: context, term: term): result<(typ, context), string> => { + switch term { + // Var rule + | Var(name) => Ok(lookupTypeVariable(ctx, name), ctx) + + // 1I⇒ rule + | Unit => Ok(Unit, ctx) + + // Anno rule + | Annot(e, tyA) => typecheck(ctx, e, tyA)->Result.map(ctx => (tyA, ctx)) + + // →I⇒ rule + | Lam(x, e) => + // TODO: Check x and e + let exA = genSym(~prefix="ex", ()) + let exB = genSym(~prefix="ex", ()) + Ok(Arrow(Existential(exA), Existential(exB)), ctx) + + // →E rule + | App(e1, e2) => failwith("TODO") + } +} + +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)) + + // ∀App rule + | (Polytype(a, tyA), e) => failwith("TODO") + + // âApp rule + | (Existential(_), _) => failwith("TODO") + + | (Unit | Var(_), _) => 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 => { + switch typ { + | Unit => Unit + | Var(x) => Var(x) + | Existential(_) => failwith("TODO") + | Polytype(_) => failwith("TODO") + | Arrow(a, b) => Arrow(applyContext(ctx, a), applyContext(ctx, b)) + } +} diff --git a/src/data.res b/src/data.res new file mode 100644 index 0000000..d47b15c --- /dev/null +++ b/src/data.res @@ -0,0 +1,49 @@ +// Disable warning about the same constructor for different types +@@warning("-30") + +type rec term = + | Unit // () + | Var(string) // x + | Lam(string, term) // λx.e + | App(term, term) // e e + | Annot(term, typ) // (e : A) + +and typ = + | Unit // 1 + | Var(string) // α + | Existential(string) // â + | Polytype(string, typ) // ∀α.A + | Arrow(typ, typ) // A -> B + +and monotyp = + // Unit monotype + | Unit // 1 + | Var(string) // α + | Existential(string) // â + | Arrow(monotyp, monotyp) // τ -> σ + +type rec contextEntry = + | TypeVar(string) // Γ,α + | TermAnnot(string, typ) // Γ,x:A + | ExistentialVar(string) // Γ,â + | ExistentialSolved(string, monotyp) // Γ,â=τ + | Marker(string) // Γ,🢒â + +type rec completeContextEntry = + | TypeVar(string) // Ω,α + | TermAnnot(string, typ) // Ω,x:A + | ExistentialSolved(string, monotyp) // Ω,â=τ + | Marker(string) // Ω,🢒â + +type context = list + +@@warning("+30") + +/** Context lookup */ +let rec lookupTypeVariable = (ctx: list, name: string): typ => { + switch ctx { + | list{} => failwith("L") + | list{TermAnnot(n, t), ..._} if n == name => t + | list{_, ...rest} => lookupTypeVariable(rest, name) + } +} diff --git a/src/index.res b/src/index.res new file mode 100644 index 0000000..f0554e0 --- /dev/null +++ b/src/index.res @@ -0,0 +1,3 @@ +open Js + +Console.log("hellosu")