ok fuck rescript

.gitignore

@@ -2,7 +2,11 @@
 *.pdf
 
 _build
+*.bs.mjs
 *.bs.js
 
 node_modules
-lib/bs
+lib/bs
+
+__tests__/**/*.mjs
+src/**/*.mjs

__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"))))
+})

babel.config.js

@@ -0,0 +1,9 @@
+module.exports = {
+  presets: [
+    [
+      "@babel/preset-env",
+      { targets: { node: "current", esmodules: false }, modules: "cjs" },
+    ],
+  ],
+  plugins: [],
+};

bidir-writeup.typ

@@ -0,0 +1,3 @@
+= Expressions
+
+- $ id : forall a. a arrow.r a $

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"]
 }

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)/)"]
+}

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"
   }
 }

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<context, string> => {
@@ -17,31 +17,30 @@ let rec isSubtype = (ctx: context, tyA: typ, tyB: typ): result<context, string>
 and typecheck = (ctx: context, term: term, typ: typ): result<context, string> => {
   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))
   }
 }

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<contextEntry>
 
-@@warning("+30")
-
 /** Context lookup */
-let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): typ => {
+let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): result<typ, string> => {
   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)
   }
 }