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>
This commit is contained in:
William Carroll 2022-10-12 10:22:58 -07:00 committed by wpcarro
parent 5bd0e723c1
commit a8876a4cda
7 changed files with 658 additions and 1 deletions

View file

@ -0,0 +1,43 @@
open Expr_parser
open Type_parser
open Inference
type test = { input : string; expect : string; }
(* type sub_test = { s1 : string; s2 : string; s3 : string } *)
let ( let* ) = Option.bind
let tests = [
{ input = "((fn x x) 10)"; expect = "Integer"; };
{ input = "(let f (fn x x) f)"; expect = "a -> a"; };
]
(* let sub_tests = [ *)
(* { *)
(* s1 = "{b |-> b -> Int}"; *)
(* s2 = "{a: Bool, b: Int, c: Bool}"; *)
(* s3 = "{a: Bool, b: Int -> Int, c: Bool}"; *)
(* } *)
(* ] *)
exception FailedAssertion
exception TestError
let main =
tests
|> List.iter (fun { input; expect } ->
Printf.sprintf ":t %s == %s\n" input expect |> print_string;
match (parse_language input, parse_input expect) with
| Some ast, Some expected ->
(match do_infer ast with
| Some actual ->
if actual != expected then
begin
print_type actual;
raise FailedAssertion
end
else
print_string "Test passed.\n"
| _ -> raise TestError)
| _ -> raise TestError);
print_string "All tests pass!"