System F polymorphism

lib/common/interface.ml

@@ -1,7 +1,11 @@
 open Common_types
 open Util.Utility
 
-type t = { name: string; env: (string * (Type.t[@name "ty"]) list) list }
+type t = {
+  name: string;
+  typarams: (Type.t[@name "ty"]) list;
+  env: (string * (Type.t[@name "ty"]) list) list
+}
 [@@name "interface"]
 [@@deriving visitors {
     variety = "map";
@@ -19,11 +23,13 @@ let lookup ?(pos_list=[]) (x: tag) (iface: t) =
             in
             raise (Errors.Type_error (msg, pos_list))
 
-let make name env =
-    { name; env }
+let make name typarams env =
+    { name; typarams; env }
 
 let name x = x.name
 
+let typarams x = x.typarams
+
 let bindings x = x.env
 
 let pp ppf x =
@@ -33,7 +39,8 @@ let pp ppf x =
             pp_print_string name
             (pp_print_comma_list Type.pp) tys
     in
-    fprintf ppf "interface %a { %a }"
+    fprintf ppf "interface %a <%a> { %a }"
         pp_print_string x.name
+        (pp_print_list Type.pp) x.typarams
         (pp_print_comma_list pp_message)
         x.env

lib/common/ir.ml

@@ -66,6 +66,7 @@ type program = {
 }
 and decl = {
     decl_name: (Binder.t[@name "binder"]);
+    typarams : (Type.t[@name "ty"]) list;
     decl_parameters: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) list;
     decl_return_type: (Type.t[@name "ty"]);
     decl_body: comp
@@ -82,6 +83,7 @@ and comp_node =
     | Return of value
     | App of {
         func: value;
+        tyargs: (Type.t[@name "ty"]) list;
         args: value list
       }
     | If of { test: value; then_expr: comp; else_expr: comp }
@@ -97,19 +99,19 @@ and comp_node =
         branch1: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp;
         branch2: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp
     }
-    | New of string
+    | New of (string * (Type.t[@name "ty"]) list)
     | Spawn of comp
     | Send of {
         target: value;
         message: (message[@name "msg"]);
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
       }
-    | Free of (value * string option)
+    | Free of (value * (string * (Type.t[@name "ty"]) list) option)
     | Guard of {
         target: value;
         pattern: (Type.Pattern.t[@name "pattern"]);
         guards: guard list;
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
       }
 and value = (value_node WithPos.t [@name "withP"])
 and value_node =
@@ -170,9 +172,10 @@ and pp_interface ppf iface =
         (pp_print_comma_list pp_msg_ty) xs
 (* Declarations *)
 and pp_decl ppf decl_with_pos =
-    let { WithPos.node = { decl_name; decl_parameters; decl_return_type; decl_body }; _ } = decl_with_pos in
-    fprintf ppf "def %a(%a): %a {@,@[<v 2>  %a@]@,}"
+  let { WithPos.node = { decl_name; typarams; decl_parameters; decl_return_type; decl_body }; _ } = decl_with_pos in
+    fprintf ppf "def %a<%a>(%a): %a {@,@[<v 2>  %a@]@,}"
         Binder.pp decl_name
+        (pp_print_list Type.pp) typarams
         (pp_print_comma_list pp_param) decl_parameters
         Type.pp decl_return_type
         pp_comp decl_body
@@ -210,11 +213,12 @@ and pp_comp ppf comp_with_pos =
             pp_value test
             pp_comp then_expr
             pp_comp else_expr
-    | App { func; args } ->
-        fprintf ppf "%a(%a)"
+    | App { func; tyargs; args } ->
+        fprintf ppf "%a<%a>(%a)"
             pp_value func
+            (pp_print_list Type.pp) tyargs
             (pp_print_comma_list pp_value) args
-    | New iname -> fprintf ppf "new[%s]" iname
+    | New (iname, _) -> fprintf ppf "new[%s]" iname
     | Spawn e -> fprintf ppf "spawn {@[<v>@,%a@]@,}" pp_comp e
     | Send { target; message; _ (* iname *) } ->
         (* Special-case the common case of sending to a variable.

lib/common/lib_types.ml

@@ -6,9 +6,9 @@ open Common_types
 let signatures =
     let open Type in
     let open Base in
-    let int_op_type = function_type false [Base Int; Base Int] (Base Int) in
-    let int_rel_op_type = function_type false [Base Int; Base Int] (Base Bool) in
-    let bool_rel_op_type = function_type false [Base Bool; Base Bool] (Base Bool) in
+    let int_op_type = function_type false [] [Base Int; Base Int] (Base Int) in
+    let int_rel_op_type = function_type false [] [Base Int; Base Int] (Base Bool) in
+    let bool_rel_op_type = function_type false [] [Base Bool; Base Bool] (Base Bool) in
     let int_ops =
         List.map (fun x -> (x, int_op_type)) ["+"; "-"; "/"; "*"]
     in
@@ -20,9 +20,9 @@ let signatures =
     in
     int_ops @ int_rel_ops @ bool_rel_ops @
     [
-        ("print", function_type false [Base Base.String] Type.unit_type);
-        ("concat", function_type false [Base Base.String; Base Base.String] Type.string_type);
-        ("rand", function_type false [Base Base.Int] (Base Base.Int));
-        ("sleep", function_type false [Base Base.Int] Type.unit_type);
-        ("intToString", function_type false [Base Base.Int] (Base Base.String))
+      ("print", function_type false [] [Base Base.String] Type.unit_type);
+      ("concat", function_type false [] [Base Base.String; Base Base.String] Type.string_type);
+      ("rand", function_type false [] [Base Base.Int] (Base Base.Int));
+      ("sleep", function_type false [] [Base Base.Int] Type.unit_type);
+      ("intToString", function_type false [][Base Base.Int] (Base Base.String))
     ]

lib/common/pretype.ml

@@ -9,8 +9,9 @@ open Util.Utility
 
 type t =
     | PBase of base
-    | PFun of { linear: bool; args: (Type.t[@name "ty"]) list; result: (Type.t[@name "ty"]) }
-    | PInterface of string
+    | PVar of string
+    | PFun of { linear: bool; typarams: (Type.t[@name "ty"]) list; args: (Type.t[@name "ty"]) list; result: (Type.t[@name "ty"]) }
+    | PInterface of (string * (Type.t[@name "ty"]) list)
     | PSum of (t * t)
     | PTuple of t list
     [@@name "pretype"]
@@ -21,12 +22,13 @@ let unit = PTuple []
 
 let rec pp ppf =
   let open Format in
-  let ps = pp_print_string ppf in
   function
     | PBase b -> Common_types.Base.pp ppf b
-    | PFun { linear; args; result } ->
+    | PVar s -> fprintf ppf "%s" s
+    | PFun { linear; typarams; args; result } ->
         let arrow = if linear then "-o" else "->" in
-        fprintf ppf "(%a) %s %a"
+        fprintf ppf "<%a> (%a) %s %a"
+            (pp_print_list Type.pp) typarams
             (pp_print_comma_list Type.pp) args
             arrow
             Type.pp result
@@ -38,7 +40,10 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
-    | PInterface name -> ps name
+    | PInterface (iname, tyargs) ->
+        fprintf ppf "%s<%a>"
+            iname
+            (pp_print_list Type.pp) tyargs
 
 let show t =
   let open Format in
@@ -47,8 +52,9 @@ let show t =
 
 let rec of_type = function
     | Type.Base b -> PBase b
-    | Type.Fun { linear; args; result } ->
-        PFun { linear; args; result = result }
+    | Type.TVar s -> PVar s
+    | Type.Fun { linear; typarams; args; result } ->
+        PFun { linear; typarams; args; result = result }
     | Type.Tuple ts -> PTuple (List.map of_type ts)
     | Type.Sum (t1, t2) -> PSum (of_type t1, of_type t2)
     | Type.Mailbox { interface; _ } -> PInterface interface
@@ -59,8 +65,9 @@ let rec of_type = function
     when trying to type an application in synthesis mode). *)
 let rec to_type = function
     | PBase b -> Some (Type.Base b)
-    | PFun { linear; args; result } ->
-        Some (Type.Fun { linear; args; result })
+    | PVar s -> Some (Type.TVar s)
+    | PFun { linear; typarams; args; result } ->
+        Some (Type.Fun { linear; typarams; args; result })
     | PTuple ts ->
         let rec go acc =
             function

lib/common/sugar_ast.ml

@@ -28,6 +28,7 @@ and expr_node =
     | Seq of expr * expr
     | App of {
         func: expr;
+        tyargs: (Type.t[@name "ty"]) list;
         args: expr list
     }
     | If of { test: expr; then_expr: expr; else_expr: expr }
@@ -51,20 +52,20 @@ and expr_node =
        not wired to their continuations. I've experimented with the
        bidirectional rules and it seems that this does not pose any problems. *)
     (* That said, we may revisit this later when we look at deadlock detection. *)
-    | New of string (* interface name *)
+    | New of (string * (Type.t[@name "ty"]) list) (* interface name *)
     | Spawn of expr
     (* interface names for Send and Guard will be added after pre-type checking *)
     | Send of {
         target: expr;
         message: (string * (expr list));
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
     }
     | Guard of {
         target: expr;
         (* At least at the moment, each guard must be annotated with a pattern *)
         pattern: (Type.Pattern.t [@name "pattern"]);
         guards: guard list;
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
     }
     | Free of expr
     (* fail(e)[A], desugars to (guard e : 0 { fail } : A) *)
@@ -91,6 +92,7 @@ and guard_node =
     | Fail of (Type.t[@name "ty"])
 and decl = {
     decl_name: string;
+    typarams: (Type.t[@name "ty"]) list;
     decl_parameters: (string * (Type.t[@name "ty"])) list;
     decl_return_type: (Type.t[@name "ty"]);
     decl_body: expr
@@ -141,11 +143,12 @@ and pp_interface ppf iface =
         (pp_print_comma_list pp_msg_ty) xs
 (* Declarations *)
 and pp_decl ppf decl =
-    let  { decl_name; decl_parameters; decl_return_type; decl_body } =
+  let  { decl_name; typarams; decl_parameters; decl_return_type; decl_body } =
         WithPos.node decl
     in
-    fprintf ppf "def %s(%a): %a {@,@[<v 2>  %a@]@,}"
+    fprintf ppf "def %s<%a>(%a): %a {@,@[<v 2>  %a@]@,}"
       decl_name
+      (pp_print_list Type.pp) typarams
       (pp_print_comma_list pp_param) decl_parameters
       Type.pp decl_return_type
       pp_expr decl_body
@@ -193,11 +196,12 @@ and pp_expr ppf expr_with_pos =
             pp_expr else_expr
     | Seq (e1, e2) ->
         fprintf ppf "(%a;@,%a)" pp_expr e1 pp_expr e2
-    | App { func; args } ->
-        fprintf ppf "%a(%a)"
+    | App { func; tyargs; args } ->
+        fprintf ppf "%a<%a>(%a)"
             pp_expr func
+            (pp_print_list Type.pp) tyargs
             (pp_print_comma_list pp_expr) args
-    | New iname -> fprintf ppf "new[%s]" iname
+    | New (iname, _) -> fprintf ppf "new[%s]" iname
     | Spawn e -> fprintf ppf "spawn {@[<v>@,%a@]@,}" pp_expr e
     | Send { target; message; _ (* iname *) } ->
         (* Special-case the common case of sending to a variable.

lib/common/type.ml

@@ -249,13 +249,14 @@ module Pattern = struct
 end
 
 type t =
+    | TVar of string
     | Base of base
-    | Fun of { linear: bool; args: t list; result: t }
+    | Fun of { linear: bool; typarams: t list; args: t list; result: t }
     | Tuple of t list
     | Sum of (t * t)
     | Mailbox of {
         capability: (Capability.t [@name "capability"]);
-        interface: string;
+        interface: (string * t list);
         (* A mailbox type can either be returnable or usable.
            A returnable mailbox name can be used for all purposes (can be
            returned from subexpressions, can be sent upon, can be received
@@ -296,8 +297,8 @@ let string_type = Base Base.String
 let bool_type = Base Base.Bool
 let unit_type = Tuple []
 let atom = Base Base.Atom
-let function_type linear args result =
-    Fun { linear; args; result }
+let function_type linear typarams args result =
+    Fun { linear; typarams; args; result }
 
 let mailbox_send_unit interface quasilinearity =
     Mailbox {
@@ -311,9 +312,11 @@ let rec pp ppf =
   let open Format in
   function
     | Base b -> Base.pp ppf b
-    | Fun { linear; args; result } ->
+    | TVar s -> fprintf ppf "%s" s
+    | Fun { linear; typarams; args; result } ->
         let arrow = if linear then "-o" else "->" in
-        fprintf ppf "(%a) %s %a"
+        fprintf ppf "<%a> (%a) %s %a"
+            (pp_print_list pp) typarams
             (pp_print_comma_list pp) args
             arrow
             pp result
@@ -325,7 +328,7 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
-    | Mailbox { capability; interface; pattern; quasilinearity } ->
+    | Mailbox { capability; interface=(iname, tyargs); pattern; quasilinearity } ->
         let ql =
             match quasilinearity with
                 | Quasilinearity.Returnable -> "R"
@@ -336,8 +339,9 @@ let rec pp ppf =
                 | Capability.In -> "?"
                 | Capability.Out -> "!"
         in
-        fprintf ppf "%s%s(%a)[%s]"
-            interface
+        fprintf ppf "%s<%a>%s(%a)[%s]"
+            iname
+            (pp_print_list pp) tyargs
             op
             (pp_print_option pp_pattern) pattern
             ql
@@ -353,6 +357,7 @@ let show t =
 
 let rec is_lin = function
     | Base _ -> false
+    | TVar _ -> false
     | Fun { linear; _ } -> linear
     (* !1 is unrestricted... *)
     | Mailbox { capability = Out; pattern = Some One; _ } -> false
@@ -411,8 +416,8 @@ let rec is_returnable = function
     | Sum  (t1, t2) -> is_returnable t1 && is_returnable t2
     | _ -> true
 
-let make_function_type linear args result =
-    Fun { linear; args; result }
+let make_function_type linear typarams args result =
+    Fun { linear; typarams; args; result }
 
 let make_tuple_type tys =
     Tuple (List.map make_returnable tys)

lib/frontend/desugar_sugared_guards.ml

@@ -30,7 +30,7 @@ let visitor =
                 target = new_target;
                 pattern = Type.Pattern.Zero;
                 guards = [WithPos.make ~pos:(WithPos.pos new_target) (Fail ty)];
-                iname = None
+                iface = None
               } in
               let new_expr_node = Annotate (WithPos.make ~pos:(WithPos.pos new_target) new_guard, ty) in
               { expr_with_pos with node = new_expr_node }

lib/frontend/insert_pattern_variables.ml

@@ -12,9 +12,11 @@ let rec annotate_type =
     let open Type in
     function
         | Base t -> Base t
-        | Fun { linear; args; result } ->
+        | TVar s -> TVar s
+        | Fun { linear; typarams; args; result } ->
             Fun {
                 linear;
+                typarams;
                 args = List.map annotate_type args;
                 result = annotate_type result
             }
@@ -49,7 +51,7 @@ let annotate_interface_type =
 let annotate_interface iface =
     Interface.bindings iface
     |> List.map (fun (tag, tys) -> (tag, List.map annotate_interface_type tys))
-    |> Interface.(make (name iface))
+    |> Interface.(make (name iface) (typarams iface))
 
 (* The visitor traverses the AST to annotate parameters of higher-order
    functions. *)