From fc24057dadbe9b0dcec237bd0dafc2ed4da64158 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 11 Feb 2021 03:41:12 -0600
Subject: [PATCH] asdf

---
 bidi.ml | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 bidi.ml

diff --git a/bidi.ml b/bidi.ml
new file mode 100644
index 0000000..e306230
--- /dev/null
+++ b/bidi.ml
@@ -0,0 +1,40 @@
+type expr =
+  | EUnit (* () *)
+  | EVar of string (* x *)
+  | EAbs of string * expr (* λx.e *)
+  | EApp of expr * expr (* e.e *)
+  | EAnnot of expr * ty (* e:A *)
+
+and ty =
+  | TUnit (* () *)
+  | TFun of ty * ty (* A->A *)
+
+type err =
+  | UnboundName of string
+  | CantApplyNonFunc
+  | NeedsAnnotation of string
+
+type ctx = (string * ty) list
+
+let rec infer (ctx: ctx) (expr: expr): (ty, err) result =
+  match expr with
+  | EUnit -> Ok TUnit
+  | EVar name ->
+      List.find_opt (fun (n, _) -> n = name) ctx
+      |> Option.to_result ~none:(UnboundName name)
+      |> Result.map snd
+  | EAnnot (_, ty) -> Ok ty
+  | EApp (func, arg) ->
+      begin match infer ctx func with
+      | Ok (TFun (a, b)) -> check ctx arg a |> Result.map (Fun.const b)
+      | Ok _ -> Error CantApplyNonFunc
+      | Error e -> Error e
+      end
+  | EAbs (name, _) -> Error (NeedsAnnotation name)
+
+and check (ctx: ctx) (expr: expr) (ty: ty): (unit, err) result =
+  match (expr, ty) with
+  | (EAbs (name, body), TFun (argt, bodyt)) -> check ((name, argt) :: ctx) body bodyt
+  | _ -> infer ctx expr |> Result.map (Fun.const ())
+
+(* vim: set sw=2 : *)