Tracking control-flow linearity for effect handlers

core/basicsettings.ml

@@ -32,6 +32,17 @@ module Handlers = struct
               |> sync)
 end
 
+(* control-flow linearity *)
+module CTLinearity = struct
+  let enabled =
+    Settings.(flag "track_control_flow_linearity"
+              |> privilege `System
+              |> synopsis "Enables the control-flow linearity extension"
+              |> convert parse_bool
+              |> CLI.(add (long "track-control-flow-linearity"))
+              |> sync)
+end
+
 module Sessions = struct
   let exceptions_enabled =
     Settings.(flag "session_exceptions"

core/commonTypes.ml

@@ -15,9 +15,9 @@ module Linearity = struct
     | Unl -> true
     | _   -> false
 
-  let to_string = function
+  let to_string ?(is_eff=false) = function
     | Any -> "Any"
-    | Unl -> "Unl"
+    | Unl -> if is_eff then "Lin" else "Unl"
 
   let min l r =
     match l, r with

core/compilePatterns.ml

@@ -128,7 +128,7 @@ let rec desugar_pattern : Types.row -> Sugartypes.Pattern.with_pos -> Pattern.t
         | Variant (name, Some p) ->
             let p, env = desugar_pattern p in
             Pattern.Variant (name, p), env
-        | Operation (name, ps, k) ->
+        | Operation (name, ps, k, _) ->
            let ps, env =
              List.fold_right
                (fun p (ps, env) ->
@@ -996,7 +996,7 @@ let compile_handle_cases
               fields
           in
           let rec extract t = match TypeUtils.concrete_type t with
-            | Types.Operation (domain, _) ->
+            | Types.Operation (domain, _, _) ->
               let (fields, _, _) = TypeUtils.extract_row domain |> TypeUtils.extract_row_parts in
               let arity = StringMap.size fields in
               if arity = 1 then

core/desugarDatatypes.ml

@@ -113,8 +113,8 @@ module Desugar = struct
         | Record r -> Types.Record (row alias_env r t')
         | Variant r -> Types.Variant (row alias_env r t')
         | Effect r -> Types.Effect (row alias_env r t')
-        | Operation (f, t) -> Types.Operation ( Types.make_tuple_type (List.map datatype f)
-                           , datatype t )
+        | Operation (f, t, b) -> Types.Operation ( Types.make_tuple_type (List.map datatype f)
+                           , datatype t, b)
         | Table (tmp, r, w, n) -> Types.Table (tmp, datatype r, datatype w, datatype n)
         | List k -> Types.Application (Types.list, [(PrimaryKind.Type, datatype k)])
         | TypeApplication (tycon, ts) ->

core/desugarEffects.ml

@@ -128,10 +128,10 @@ let simplify_tycon_env (tycon_env : Types.tycon_environment) : simple_tycon_env
   in
   SEnv.fold simplify_tycon tycon_env SEnv.empty
 
-let make_anon_point k sk freedom =
+let make_anon_point ?(is_eff=true) k sk freedom =
   let var = Types.fresh_raw_variable () in
   Unionfind.fresh
-    (Types.Var (var, (k, DesugarTypeVariables.concrete_subkind sk), freedom))
+    (Types.Var (var, (k, DesugarTypeVariables.concrete_subkind ~is_effect:is_eff sk), freedom))
 
 (** A map with SugarTypeVar as keys, use for associating the former
    with information about what
@@ -364,7 +364,8 @@ let cleanup_effects tycon_env =
          WithPos.make ~pos (match node with
              | Datatype.Operation _     -> node
              | Datatype.Forall (qs, dt) -> Datatype.Forall (qs, elaborate_op dt)
-             | _                        -> Datatype.Operation ([], dt))
+             | _                        -> Datatype.Operation ([], dt, DeclaredLinearity.Unl))
+             (* nullary operations without =@ are unlimited *)
        in
        let fields = List.map (function
            | name, Present dt when not (TypeUtils.is_builtin_effect name) ->
@@ -379,18 +380,18 @@ let cleanup_effects tycon_env =
             if not (SugarTypeVar.is_resolved stv)
             then begin
                 let gen_unresolved_eff () =
-                  SugarTypeVar.mk_unresolved shared_effect_var_name None `Rigid
+                  SugarTypeVar.mk_unresolved shared_effect_var_name ~is_eff:true None `Rigid
                 in
                 let to_unresolved_general sk fr =
-                  SugarTypeVar.mk_unresolved "$" sk fr
+                  SugarTypeVar.mk_unresolved "$" ~is_eff:true sk fr
                 in
                 let gen_resolved_flex () =
                   SugarTypeVar.mk_resolved_row
                     (let var = Types.fresh_raw_variable () in
                      Unionfind.fresh
-                       (Types.Var (var, (PrimaryKind.Row, (lin_unl, res_effect)), `Flexible)))
+                       (Types.Var (var, (PrimaryKind.Row, (default_effect_lin, res_effect)), `Flexible)))
                 in
-                let name, sk, fr = gue stv in
+                let name, (_, sk), fr = gue stv in
                 if has_effect_sugar
                 then
                   begin
@@ -453,7 +454,7 @@ let gather_mutual_info (tycon_env : simple_tycon_env) =
            match eff_var with
            | Datatype.Open stv
              when (not (SugarTypeVar.is_resolved stv))
-                  && SugarTypeVar.get_unresolved_exn stv = ("$eff", None, `Rigid)
+                  && SugarTypeVar.get_unresolved_exn stv = ("$eff", (true, None), `Rigid)
              ->
                self#with_implicit
            | _ -> self )
@@ -768,7 +769,7 @@ let gather_operations (tycon_env : simple_tycon_env) allow_fresh dt =
                 let point =
                   lazy
                     (let var = Types.fresh_raw_variable () in
-                     Unionfind.fresh (Types.Var (var, (PrimaryKind.Presence, default_subkind), `Rigid)))
+                     Unionfind.fresh (Types.Var (var, (PrimaryKind.Presence, default_effect_subkind), `Rigid)))
                 in
                 StringMap.add op point m)
               v StringMap.empty),
@@ -786,7 +787,7 @@ let preprocess_type (dt : Datatype.with_pos) tycon_env allow_fresh shared_effect
           lazy
             (let var = Types.fresh_raw_variable () in
              Unionfind.fresh
-               (Types.Var (var, (PrimaryKind.Row, (lin_unl, res_any)), `Rigid)))
+               (Types.Var (var, (PrimaryKind.Row, default_effect_subkind), `Rigid)))
         in
         Some point
     | _ ->
@@ -948,7 +949,7 @@ class main_traversal simple_tycon_env =
                     (* Looking for this gives us the operations associcated with
                        the $eff var. The kind and freedom info are ignored for the lookup *)
                     let eff_sugar_var =
-                      SugarTypeVar.mk_unresolved shared_effect_var_name None
+                      SugarTypeVar.mk_unresolved shared_effect_var_name ~is_eff:true None
                         `Rigid
                     in
 
@@ -1018,8 +1019,8 @@ class main_traversal simple_tycon_env =
             if not allow_implictly_bound_vars then
               raise (DesugarTypeVariables.free_type_variable dpos);
 
-            let _name, sk, freedom = SugarTypeVar.get_unresolved_exn stv in
-            let mtv = make_anon_point (PrimaryKind.Row) sk freedom in
+            let _name, (is_eff, sk), freedom = SugarTypeVar.get_unresolved_exn stv in
+            let mtv = make_anon_point ~is_eff:is_eff (PrimaryKind.Row) sk freedom in
             let rtv = SugarTypeVar.mk_resolved_row mtv in
             (o, D.Open rtv)
         | D.Open srv when not (SugarTypeVar.is_resolved srv) ->
@@ -1177,7 +1178,7 @@ class main_traversal simple_tycon_env =
               ({ node = t, args, b; pos } as tn) =
             if StringMap.find t implicits then
               let var = Types.fresh_raw_variable () in
-              let q = (var, (PrimaryKind.Row, (lin_unl, res_effect))) in
+              let q = (var, (PrimaryKind.Row, (default_effect_lin, res_effect))) in
               (* Add the new quantifier to the argument list and rebind. *)
               (* let qs = List.map (snd ->- OptionUtils.val_of) args @ [q] in *)
               let args = args @ [ SugarQuantifier.mk_resolved q ] in
@@ -1191,7 +1192,7 @@ class main_traversal simple_tycon_env =
               let tycon_env = SEnv.bind t (env_args, true, None) tycon_env in
               let shared_effect_var : Types.meta_row_var Lazy.t =
                 lazy
-                  (Unionfind.fresh (Types.Var (var, (PrimaryKind.Row, (lin_unl, res_effect)), `Rigid)))
+                  (Unionfind.fresh (Types.Var (var, (PrimaryKind.Row, (default_effect_lin, res_effect)), `Rigid)))
               in
               let shared_var_env =
                 StringMap.add t (Some shared_effect_var) shared_var_env

core/desugarSessionExceptions.ml

@@ -87,7 +87,8 @@ object (o : 'self_type)
         let ty =
           Types.fresh_type_variable (CommonTypes.lin_any, CommonTypes.res_any) in
         let with_pos x = SourceCode.WithPos.make ~pos x in
-        let doOp = DoOperation (with_pos (Operation failure_op_name), [], Some (Types.empty_type)) in
+        (* FIXME: WT: I don't know whether should it be lindo or not *)
+        let doOp = DoOperation (with_pos (Operation failure_op_name), [], Some (Types.empty_type), DeclaredLinearity.Lin) in
         (o, with_pos (Switch (with_pos doOp, [], Some ty)), ty)
     | { node = TryInOtherwise (_, _, _, _, None); _} -> assert false
     | { node = TryInOtherwise (try_phr, pat, as_phr, otherwise_phr, (Some dt)); pos }
@@ -122,7 +123,8 @@ object (o : 'self_type)
           (Utility.gensym ~prefix:"dsh" ()) in
 
         let otherwise_pat : Sugartypes.Pattern.with_pos =
-          with_dummy_pos (Pattern.Operation (failure_op_name, [], cont_pat)) in
+          (* FIXME: WT: I don't know whether should it be lincase or not *)
+          with_dummy_pos (Pattern.Operation (failure_op_name, [], cont_pat, DeclaredLinearity.Lin)) in
 
         let otherwise_clause = (otherwise_pat, otherwise_phr) in
 

core/desugarTypeVariables.ml

@@ -84,10 +84,10 @@ let free_type_variable ?var pos =
         "Unbound " ^ desc ^ " in position where
         no free type variables are allowed")
 
-let concrete_subkind =
+let concrete_subkind ?(is_effect=false) =
   function
   | Some subkind -> subkind
-  | None         -> default_subkind
+  | None         -> if is_effect then default_effect_subkind else default_subkind
 
 
 let default_kind : PrimaryKind.t = PrimaryKind.Type
@@ -169,36 +169,36 @@ However, this is not the same as setting defaults. Instead,
 the info in the map takes precedence.
 
 *)
-let make_opt_kinded_var k sk_opt freedom : Types.t =
+let make_opt_kinded_var k ?(is_eff=false) sk_opt freedom : Types.t =
   let var = Types.fresh_raw_variable () in
-  let sk = concrete_subkind sk_opt in
+  let sk = concrete_subkind ~is_effect:is_eff sk_opt in
   Types.Var (var, (k, sk), freedom)
 
 let get_var_info (info : Types.t) =
   match info with
   | Types.Var (var, k, fd) -> (var, k, fd)
   | _ -> raise found_non_var_meta_var
 
-let make_fresh_entry pk_opt sk_opt freedom : tyvar_map_entry =
+let make_fresh_entry pk_opt ?(is_eff=false) sk_opt freedom : tyvar_map_entry =
   let open PrimaryKind in
   match pk_opt with
     | None -> TVUnkinded (sk_opt, freedom)
     | Some Type ->
-       let point = Unionfind.fresh (make_opt_kinded_var Type sk_opt freedom) in
+       let point = Unionfind.fresh (make_opt_kinded_var ~is_eff:is_eff Type sk_opt freedom) in
        TVType (sk_opt, point)
     | Some Row ->
-       let point = Unionfind.fresh (make_opt_kinded_var Row sk_opt freedom) in
+       let point = Unionfind.fresh (make_opt_kinded_var ~is_eff:is_eff Row sk_opt freedom) in
        TVRow (sk_opt, point)
     | Some Presence ->
-       let point = Unionfind.fresh (make_opt_kinded_var Presence sk_opt freedom) in
+       let point = Unionfind.fresh (make_opt_kinded_var ~is_eff:is_eff Presence sk_opt freedom) in
        TVPresence (sk_opt, point)
 
 
 
 (* does not do all sanity checks *)
 (* Note that this always reuses existing points! *)
-let update_entry pk sk_opt freedom existing_entry : tyvar_map_entry =
-  let con_sk = concrete_subkind sk_opt in
+let update_entry pk ?(is_eff=false) sk_opt freedom existing_entry : tyvar_map_entry =
+  let con_sk = concrete_subkind ~is_effect:is_eff sk_opt in
   let open PrimaryKind in
   match pk, existing_entry with
     | _, TVUnkinded _ ->
@@ -290,7 +290,7 @@ object (o : 'self)
 
 
   (** Used for type/row/presence variables found along the way, including anonymous ones *)
-  method add ?pos name (pk : PrimaryKind.t) (sk : Subkind.t option) freedom : 'self * SugarTypeVar.t =
+  method add ?pos name (pk : PrimaryKind.t) ?(is_eff=false) (sk : Subkind.t option) freedom : 'self * SugarTypeVar.t =
     let anon = is_anonymous_name name in
     let pos = OptionUtils.from_option SourceCode.Position.dummy pos in
     if not anon && StringMap.mem name tyvar_map then
@@ -314,7 +314,7 @@ object (o : 'self)
            the *existing* unionfind point carried inside the entry *)
         let entry =
           if pk' <> pk_union' || sk' <> sk_union' then
-            update_entry pk sk freedom existing_entry
+            update_entry pk ~is_eff:is_eff sk freedom existing_entry
           else
             existing_entry
         in
@@ -332,7 +332,7 @@ object (o : 'self)
            Since at this point we know the primary kind,
            this will always result in the creation of a unionfind point.
          *)
-        let entry = make_fresh_entry (Some pk) sk freedom in
+        let entry = make_fresh_entry (Some pk) ~is_eff:is_eff sk freedom in
         let o =
           if anon then o else o#bind name entry in
         let resolved_var = resolved_var_of_entry entry in
@@ -390,8 +390,8 @@ object (o : 'self)
     let open Datatype in
     function
     | TypeVar stv ->
-       let (name, sk, freedom) = SugarTypeVar.get_unresolved_exn stv in
-       let o, resolved_tv = o#add name pk_type sk freedom in
+       let (name, (is_eff, sk), freedom) = SugarTypeVar.get_unresolved_exn stv in
+       let o, resolved_tv = o#add name pk_type ~is_eff:is_eff sk freedom in
        (* let resolved_tv = resolved_var_of_entry entry in *)
        o, TypeVar resolved_tv
     | Forall (unresolved_qs, body) ->
@@ -423,8 +423,8 @@ object (o : 'self)
           appear in contexts where implictly scoped variables are allowed.  *)
        o, orig
     | Open srv ->
-       let (name, sk, freedom) = SugarTypeVar.get_unresolved_exn srv in
-       let o, resolved_rv = o#add name pk_row sk freedom in
+       let (name, (is_eff, sk), freedom) = SugarTypeVar.get_unresolved_exn srv in
+       let o, resolved_rv = o#add name pk_row ~is_eff:is_eff sk freedom in
        o, Datatype.Open resolved_rv
     | Recursive (stv, r) ->
        let original_o = o in
@@ -446,8 +446,8 @@ object (o : 'self)
        let o, t = o#datatype t in
        o, Present t
     | Var utv ->
-       let (name, sk, freedom) = SugarTypeVar.get_unresolved_exn utv in
-       let o, resolved_pv = o#add name pk_presence sk freedom in
+       let (name, (is_eff, sk), freedom) = SugarTypeVar.get_unresolved_exn utv in
+       let o, resolved_pv = o#add name pk_presence ~is_eff:is_eff sk freedom in
        o, Var resolved_pv
 
   method! phrase p =

core/desugarTypeVariables.mli

@@ -1,6 +1,6 @@
 val infer_kinds : bool Settings.setting
 
-val concrete_subkind : CommonTypes.Subkind.t option -> CommonTypes.Subkind.t
+val concrete_subkind : ?is_effect:bool -> CommonTypes.Subkind.t option -> CommonTypes.Subkind.t
 
 val free_type_variable : ?var:string -> SourceCode.Position.t -> exn
 

core/generalise.ml

@@ -71,7 +71,7 @@ let rec get_type_args : gen_kind -> TypeVarSet.t -> datatype -> type_arg list =
            get_type_args kind (TypeVarSet.add_quantifiers qs bound_vars) t
         (* Effect *)
         | Effect row -> get_row_type_args kind bound_vars row
-        | Operation (f, t) ->
+        | Operation (f, t, _) ->
             let from_gens = gt f
             and to_gens = gt t in
               from_gens @ to_gens

core/instantiate.ml

@@ -76,7 +76,7 @@ let instantiates : instantiation_maps -> (datatype -> datatype) * (row -> row) *
         | Record row -> Record (instr row)
         | Variant row -> Variant (instr row)
         | Effect row -> Effect (instr row)
-        | Operation (f, t) -> Operation (inst f, inst t)
+        | Operation (f, t, b) -> Operation (inst f, inst t, b)
         | Table (tmp, f, d, r) -> Table (tmp, inst f, inst d, inst r)
         | ForAll (qs, t) ->
            let remove_shadowed_quantifier tmap q =

core/irCheck.ml

@@ -350,11 +350,12 @@ let eq_types occurrence : type_eq_context -> (Types.datatype * Types.datatype) -
          | Effect r -> eq_rows (context, l, r)
          | _         -> false
          end
-      | Operation (lfrom, lto) ->
+      | Operation (lfrom, lto, llin) ->
           begin match t2 with
-            | Operation (rfrom, rto) ->
+            | Operation (rfrom, rto, rlin) ->
               eqt     (context, lfrom, rfrom) &&
-              eqt     (context, lto  , rto  )
+              eqt     (context, lto  , rto  ) &&
+              llin = rlin
             | _ -> false
           end
       (* Row *)

core/lexer.mll

@@ -92,6 +92,7 @@ let keywords = [
  "delete_left", DELETE_LEFT;
  "determined", DETERMINED;
  "do"       , DOOP;
+ "lindo"      , LINDOOP;
  "effectname", EFFECTNAME;
  "else"     , ELSE;
  "escape"   , ESCAPE;
@@ -163,6 +164,8 @@ let keywords = [
  "with"     , WITH;
 (* SAND *)
  "tablekeys"     , TABLEKEYS;
+ (* Control-flow linearity *)
+ "xlin"     , LINFLAG
 ]
 
 exception LexicalError of (string * Lexing.position)
@@ -212,6 +215,7 @@ rule lex ctxt nl = parse
   | "-@"                                { LOLLI }
   | "~@"                                { SQUIGLOLLI }
   | "=>"                                { FATRARROW }
+  | "=@"                                { FATLOLLI }
   | "-."                                { MINUSDOT }
   | '-'                                 { MINUS }
   | '('                                 { LPAREN }