Infer scalar types with let generalization

test/test_harness.ml

@@ -63,3 +63,32 @@ let run_suite suite cases =
 let failure_count () = !failures
 
 let case_count () = !cases
+
+let root () = try Sys.getenv "DELTA_ROOT" with Not_found -> "."
+
+let fixture name = Filename.concat (root ()) (Filename.concat "test/fixture" name)
+
+let read_fixture name = Native.read_file (fixture name)
+
+let error_of thunk =
+  try
+    ignore (thunk ());
+    None
+  with Diagnostic.Error diagnostic -> Some diagnostic
+
+let parse text = Parse.program text
+
+let resolve text = Resolve.program (parse text)
+
+let infer text = Infer.program (resolve text)
+
+let parse_error text = error_of (fun () -> parse text)
+
+let resolve_error text = error_of (fun () -> resolve text)
+
+let infer_error text = error_of (fun () -> infer text)
+
+let check_message name expected thunk =
+  match error_of thunk with
+  | None -> fail name "expected a diagnostic"
+  | Some diagnostic -> check_equal_string name expected diagnostic.Diagnostic.message

test/test_harness.mli

@@ -9,3 +9,15 @@ val expect_diagnostic : string -> (unit -> unit) -> unit
 val run_suite : string -> case list -> unit
 val failure_count : unit -> int
 val case_count : unit -> int
+
+val root : unit -> string
+val fixture : string -> string
+val read_fixture : string -> string
+val error_of : (unit -> 'a) -> Diagnostic.t option
+val parse : string -> Syntax.program
+val resolve : string -> Resolve.program
+val infer : string -> Typed.program
+val parse_error : string -> Diagnostic.t option
+val resolve_error : string -> Diagnostic.t option
+val infer_error : string -> Diagnostic.t option
+val check_message : string -> string -> (unit -> 'a) -> unit

test/test_main.ml

@@ -180,12 +180,6 @@ let parse_cases =
           (match parsed.Syntax.e with Syntax.EInt 7 -> true | _ -> false) );
   ]
 
-let root () = try Sys.getenv "DELTA_ROOT" with Not_found -> "."
-
-let fixture name = Filename.concat (root ()) (Filename.concat "test/fixtures" name)
-
-let read_fixture name = Native.read_file (fixture name)
-
 let program_error text =
   try
     ignore (Parse.program text);
@@ -379,5 +373,6 @@ let () =
   Test_harness.run_suite "parse" parse_cases;
   Test_harness.run_suite "program" program_cases;
   Test_harness.run_suite "resolve" resolve_cases;
+  Test_harness.run_suite "types" Test_type.cases;
   Printf.printf "%d cases, %d failures\n" (Test_harness.case_count ()) (Test_harness.failure_count ());
   exit (if Test_harness.failure_count () = 0 then 0 else 1)

test/test_type.ml

@@ -0,0 +1,160 @@
+open Test_harness
+
+let infer_program text = infer text
+
+let cases =
+  [
+    ( "the example query infers a collection of tuples of string and int",
+      fun () ->
+        let program = infer_program (read_fixture "expensive_order.delta") in
+        check_equal_string "query type" "collection (string, int)"
+          (Types.pp program.Typed.tp_query_body.Typed.ty);
+        check_equal_string "input element" "order" (Types.pp program.Typed.tp_input_element) );
+    ( "the example helper infers an integer arrow",
+      fun () ->
+        let program = infer_program (read_fixture "expensive_order.delta") in
+        check_equal_string "helper type" "(int -> int)"
+          (Types.pp (List.hd program.Typed.tp_helpers).Typed.th_scheme.Types.body) );
+    ( "revenue infers an integer query",
+      fun () ->
+        let program = infer_program (read_fixture "revenue.delta") in
+        check_equal_string "query type" "int" (Types.pp program.Typed.tp_query_body.Typed.ty) );
+    ( "count_large infers an integer query",
+      fun () ->
+        let program = infer_program (read_fixture "count_large.delta") in
+        check_equal_string "query type" "int" (Types.pp program.Typed.tp_query_body.Typed.ty) );
+    ( "a helper generalizes at its let binding",
+      fun () ->
+        let program =
+          infer_program
+            "type order = { customer : string; total : int }\ninput orders : collection order\nlet pair a b = (a, b)\nquery q = orders |> map (fun o -> pair o.total o.customer)\n"
+        in
+        let scheme = (List.hd program.Typed.tp_helpers).Typed.th_scheme in
+        check_equal_int "two generalized variables" 2 (List.length scheme.Types.vars);
+        check "the helper is a two argument function"
+          (match Types.repr scheme.Types.body with
+          | Types.TArrow (_, Types.TArrow _) -> true
+          | _ -> false);
+        check_equal_string "query type" "collection (int, string)"
+          (Types.pp program.Typed.tp_query_body.Typed.ty) );
+    ( "a polymorphic helper is instantiated independently at each use",
+      fun () ->
+        let program =
+          infer_program
+            "type order = { customer : string; total : int }\ninput orders : collection order\nlet identity x = x\nlet tax n = identity n * 20 / 100\nquery q = orders |> map (fun o -> (identity o.customer, tax o.total))\n"
+        in
+        check_equal_string "query type" "collection (string, int)"
+          (Types.pp program.Typed.tp_query_body.Typed.ty) );
+    ( "the occurs check rejects self application",
+      fun () ->
+        match infer_error "input rows : collection int\nlet f x = x x\nquery q = rows\n" with
+        | None -> fail "occurs" "expected a diagnostic"
+        | Some diagnostic ->
+            check "message mentions an infinite type"
+              (Util.starts_with "cannot construct the infinite type" diagnostic.Diagnostic.message) );
+    ( "an unannotated arithmetic helper that is applied to a string is rejected",
+      fun () ->
+        check_message "arithmetic" "type mismatch: expected int but got string"
+          (fun () ->
+            infer_program "input rows : collection int\nlet f n = n + 1\nquery q = rows |> map (fun r -> f \"a\")\n") );
+    ( "projection on a non record is rejected",
+      fun () ->
+        check_message "projection" "type mismatch: expected order but got int"
+          (fun () ->
+            infer_program
+              "type order = { total : int }\ninput rows : collection int\nquery q = rows |> map (fun r -> r.total)\n") );
+    ( "unknown record fields are rejected",
+      fun () ->
+        check_message "unknown field" "no record type declares a field named `tota`"
+          (fun () ->
+            infer_program
+              "type order = { total : int }\ninput rows : collection order\nquery q = rows |> map (fun r -> r.tota)\n") );
+    ( "record literals must provide every field",
+      fun () ->
+        check_message "missing field" "record literal of type `order` is missing field `customer`"
+          (fun () ->
+            infer_program
+              "type order = { customer : string; total : int }\ninput rows : collection order\nquery q = rows |> map (fun r -> { total = r.total })\n") );
+    ( "record literals reject fields of another record",
+      fun () ->
+        check_message "mixed fields" "record `order` has no field named `other`"
+          (fun () ->
+            infer_program
+              "type order = { total : int }\ninput rows : collection order\nquery q = rows |> map (fun r -> { total = r.total; other = 1 })\n") );
+    ( "a record field with a collection type is rejected",
+      fun () ->
+        check_message "collection field"
+          "record field `items` has a collection type; collections may not be stored in records"
+          (fun () ->
+            infer_program "type box = { items : collection int }\ninput rows : collection box\nquery q = rows\n") );
+    ( "nested collection types are rejected",
+      fun () ->
+        check_message "collection type position"
+          "collection types are only allowed as the input type and as query results"
+          (fun () -> infer_program "input rows : collection (collection int)\nquery q = rows\n") );
+    ( "the input must be declared with a collection type",
+      fun () ->
+        check_message "input type"
+          "the input collection must be declared with a collection type: input NAME : collection T"
+          (fun () -> infer_program "input rows : int\nquery q = 1\n") );
+    ( "sum rejects a non integer collection",
+      fun () ->
+        check_message "sum"
+          "sum expects a collection of integers but got collection string"
+          (fun () ->
+            infer_program
+              "type order = { customer : string }\ninput rows : collection order\nquery q = rows |> map (fun r -> r.customer) |> sum\n") );
+    ( "sum rejects a scalar operand",
+      fun () ->
+        check_message "sum scalar" "sum expects a collection of integers but got int"
+          (fun () -> infer_program "input rows : collection int\nquery q = sum 1\n") );
+    ( "filter must be applied to a collection",
+      fun () ->
+        check_message "filter arity" "`filter` and `map` must be applied to a collection"
+          (fun () -> infer_program "input rows : collection int\nquery q = filter (fun x -> true)\n") );
+    ( "map cannot produce a collection",
+      fun () ->
+        check_message "nested collection" "nested collections are not supported: mapped element"
+          (fun () -> infer_program "input rows : collection int\nquery q = rows |> map (fun r -> rows)\n") );
+    ( "count rejects a scalar operand",
+      fun () ->
+        check_message "count scalar" "count expects a collection but got int"
+          (fun () -> infer_program "input rows : collection int\nquery q = count 1\n") );
+    ( "a query must produce a collection or an integer",
+      fun () ->
+        check_message "query result"
+          "a query must produce a collection or an integer, but this query produces string"
+          (fun () -> infer_program "input rows : collection int\nquery q = \"hello\"\n") );
+    ( "equality is rejected on functions",
+      fun () ->
+        check_message "function equality"
+          "`=` is only supported on integers, booleans, strings, unit, tuples and records of these, but the operands have type (int -> int)"
+          (fun () ->
+            infer_program
+              "input rows : collection int\nlet bad = (fun x -> x + 1) = (fun x -> x + 1)\nquery q = rows\n" ) );
+    ( "conditional branches must have the same type",
+      fun () ->
+        check_message "branch mismatch" "type mismatch: expected int but got string"
+          (fun () -> infer_program "input rows : collection int\nquery q = if true then 1 else \"x\"\n") );
+    ( "unknown type names are rejected",
+      fun () ->
+        check_message "unknown type" "unknown type `order`"
+          (fun () -> infer_program "input rows : collection order\nquery q = rows\n") );
+    ( "negation is integer only",
+      fun () ->
+        check_message "negation" "type mismatch: expected bool but got int"
+          (fun () -> infer_program "input rows : collection int\nquery q = -true\n") );
+    ( "a constant integer query is accepted",
+      fun () ->
+        let program = infer_program "input rows : collection int\nquery q = 40 + 2\n" in
+        check_equal_string "query type" "int" (Types.pp program.Typed.tp_query_body.Typed.ty) );
+    ( "the typed dump is deterministic",
+      fun () ->
+        Types.reset ();
+        Ident.reset ();
+        let first = Typed.program_to_string (infer_program (read_fixture "expensive_order.delta")) in
+        Types.reset ();
+        Ident.reset ();
+        let second = Typed.program_to_string (infer_program (read_fixture "expensive_order.delta")) in
+        check_equal_string "identical dumps" first second );
+  ]