From a8876a4cdaaf0a1f051fefad436e08d983b402e2 Mon Sep 17 00:00:00 2001
From: William Carroll <wpcarro@gmail.com>
Date: Wed, 12 Oct 2022 10:22:58 -0700
Subject: feat(wpcarro/scratch): Implement "Algorithm W"

I've been wanting to grok Haskell-style type inference for awhile, so instead of
just watching conference talks and reading papers about it, I've decided to
attempt to implement it to more readily test my understanding of it.

Change-Id: I69261202a3d74d55c6e38763d7ddfec73c392465
Reviewed-on: https://cl.tvl.fyi/c/depot/+/6988
Tested-by: BuildkiteCI
Reviewed-by: wpcarro <wpcarro@gmail.com>
Autosubmit: wpcarro <wpcarro@gmail.com>
---
 users/wpcarro/scratch/compiler/type_parser.ml | 115 ++++++++++++++++++++++++++
 1 file changed, 115 insertions(+)
 create mode 100644 users/wpcarro/scratch/compiler/type_parser.ml

(limited to 'users/wpcarro/scratch/compiler/type_parser.ml')

diff --git a/users/wpcarro/scratch/compiler/type_parser.ml b/users/wpcarro/scratch/compiler/type_parser.ml
new file mode 100644
index 000000000000..9b6c0a309309
--- /dev/null
+++ b/users/wpcarro/scratch/compiler/type_parser.ml
@@ -0,0 +1,115 @@
+(******************************************************************************
+ * Type Expression Language:
+ *
+ * Helpers:
+ *   symbol   -> [a-z]
+ *
+ * Core:
+ *   type     -> function
+ *   function -> ( variable | literal ) '->' type
+ *   literal  -> 'Integer' | 'Boolean'
+ *   variable -> symbol
+ ******************************************************************************)
+
+open Types
+open Parser
+open Inference
+
+type side = LHS | RHS
+
+let ( let* ) = Option.bind
+
+let printsub (s : substitution) =
+  FromString.fold (fun k v acc -> Printf.sprintf "%s\"%s\" |-> %s;" acc k (pretty v)) s ""
+  |> Printf.sprintf "Sub { %s }"
+  |> print_string
+  |> print_newline
+
+let to_array (q : 'a Queue.t) : 'a array =
+  let result = Array.make (Queue.length q) "" in
+  let i = ref 0 in
+  Queue.iter
+    (fun x ->
+      result.(!i) <- x;
+      i := !i + 1)
+    q;
+  result
+
+let tokenize (x : string) : token array =
+  let q = Queue.create () in
+  let i = ref 0 in
+  while !i < String.length x do
+    match x.[!i] with
+    | ' ' -> i := !i + 1
+    | _ ->
+       let beg = !i in
+       while (!i < String.length x) && (x.[!i] != ' ') do
+         i := !i + 1
+       done;
+       Queue.push (String.sub x beg (!i - beg)) q
+  done;
+  to_array q
+
+let rec parse_type (p : parser) : _type option =
+  parse_function p
+and parse_function (p : parser) : _type option =
+  match p#next with
+  | Some "->" ->
+     let* a = parse_literal p in
+     p#advance;
+     let* b = parse_type p in
+     Some (TypeArrow (a, b))
+  | _ -> parse_literal p
+and parse_literal (p : parser) : _type option =
+  match p#curr with
+  | Some "Integer" | Some "Int" -> p#advance; Some TypeInt
+  | Some "Boolean" | Some "Bool" -> p#advance; Some TypeBool
+  | Some _ -> parse_variable p
+  | None -> None
+and parse_variable (p : parser) : _type option =
+  match p#curr with
+  | Some x when String.length x = 1 -> p#advance; Some (TypeVariable x)
+  | _ -> None
+
+let print_tokens (xs : string array) =
+  xs
+  |> Array.to_list
+  |> List.map (Printf.sprintf "\"%s\"")
+  |> String.concat ", "
+  |> Printf.sprintf "tokens: [ %s ]"
+  |> print_string |> print_newline
+
+let print_type (t : _type) =
+  t |> pretty |> Printf.sprintf "type: %s" |> print_string |> print_newline
+
+let parse_input (x : string) : _type option =
+  let tokens = tokenize x in
+  print_tokens tokens;
+  parse_type (new parser tokens)
+
+(* Continually prompt until user provides a parseable type expression *)
+let rec read_type (arg : side) : _type =
+  let prompt = match arg with
+    | LHS -> "lhs> "
+    | RHS -> "rhs> " in
+  print_string prompt;
+  let x = read_line () in
+  match parse_input x with
+  | None ->
+     print_string "Failed to parse input.\n";
+     read_type arg
+  | Some ast ->
+     print_type ast;
+     ast
+
+let main =
+  while true do
+    begin
+      let lhs = read_type LHS in
+      let rhs = read_type RHS in
+      match unify lhs rhs with
+      | None ->
+         Printf.printf "Cannot unify \"%s\" with \"%s\"\n" (pretty lhs) (pretty rhs)
+      | Some x -> printsub x
+    end
+  done
-- 
cgit 1.4.1