update

.gitignore

@@ -1,4 +1,8 @@
 .DS_Store
 *.pdf
 
-_build
+_build
+*.bs.js
+
+node_modules
+lib/bs

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": []
+}

package.json

@@ -0,0 +1,9 @@
+{
+  "scripts": {
+    "res:build": "rescript",
+    "res:dev": "rescript build -w"
+  },
+  "devDependencies": {
+    "rescript": "^10.1.4"
+  }
+}

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<context, string> => {
+  switch (tyA, tyB) {
+  | (_, _) => failwith("TODO")
+  }
+}
+
+and typecheck = (ctx: context, term: term, typ: typ): result<context, string> => {
+  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))
+  }
+}

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<contextEntry>
+
+@@warning("+30")
+
+/** Context lookup */
+let rec lookupTypeVariable = (ctx: list<contextEntry>, name: string): typ => {
+  switch ctx {
+  | list{} => failwith("L")
+  | list{TermAnnot(n, t), ..._} if n == name => t
+  | list{_, ...rest} => lookupTypeVariable(rest, name)
+  }
+}

src/index.res

@@ -0,0 +1,3 @@
+open Js
+
+Console.log("hellosu")