Tracking control-flow linearity for effect handlers

control-flow-linearity-in-Links.md

@@ -0,0 +1,114 @@
+# Control-Flow Linearity
+
+Enable the feature of tracking control-flow linearity by passing the
+flag `--track-control-flow-linearity`. It is usually used with
+`--enabled-handlers`.
+
+## New constructs
+
+New types and kinds:
+
+* `A =@ B` is the signature for linear operations (`A => B` for unlimited operations)
+* `Lin` is the kind for linear effect variables (`Any` for effect
+  variables with no linear restriction)
+
+New terms:
+
+* `lindo L` invokes the linear operation `L`
+* `case <L =@ r> -> M` handles the linear operation `L`
+* `xlin` switches the current control flow to linear
+
+
+## Control flow
+
+We use the concept *control flow* to mean terms that are sequencing
+evaluated. Control flows carry effects that are invoked by the terms.
+In other words, the terms on the same control flow share effects.
+Since Links' effect system is based on row polymorphism, the effect
+types of all terms on the same control flow are unified.
+
+Function bodies introduce their own control flows. The computations
+being handled (the `M` in `handle M {...}`) also have their own
+control flows, which will be merged with the control flow outside
+after being handled.
+
+Control flows are unlimited by default. We are allowed use both
+unlimited and linear operations, but only unlimited variables. We can
+switch the current control flow to linear by invoking the keyword
+`xlin`. In a linear control flow, we are allowed to use both unlimited
+and linear variables, but only linear operations. Once the control
+flow is switched to linear, all invocations of unlimited operations in
+it (even before `xlin`) would cause type errors.
+
+## Examples
+
+1. We can mix linear and unlimited operations in an unlimited control
+   flow. The anonymous effect variable `_` has kind `Any` by default
+   which can be unified with any operations.
+
+    ```
+    links> fun() {do U; lindo L};
+    fun : () {L:() =@ a,U:() => ()|_}-> a
+    ```
+
+2. We can only invoke linear operations in a linear control flow. A
+   linear control flow allows the usage of the linear channel `ch`.
+   Now the effect variable `_` has kind `Lin` explicitly, which can
+   only be unified with linear operations of signatures `=@`.
+
+    ```
+    links> fun(ch:End) {xlin; lindo L; close(ch)};
+    fun : (End) {L:() =@ ()|_::Lin}~> ()
+    ```
+
+3. We can only handle linear operations using a linear handler
+   (indicated by `=@` in the clause) which guarantees the continuation
+   is used exactly once.
+
+    ```
+    links> handle ({xlin; lindo L + 40}) { case <L =@ r> -> xlin; r(2) };
+    42 : Int
+    ```
+
+4. We can handle unlimited operations before merging with a linear
+   control flow as long as we guarantee that they are all handled.
+   Note that after handling, the presence variable of `Choose` and row
+   variable are both linear.
+
+    ```
+    links> fun(ch:End) { xlin; close(ch); handle ({if (do Choose) 40 else 2}) {case <Choose => r> -> r(true) + r(false)} };
+    fun : (End) {Choose{_::Lin}|_::Lin}~> Int
+    ```
+
+5. When writing explicit quantifiers, we must explicitly annotate the
+   kinds of row variables using `e::Row(Lin)` or `e::Row(Any)`. If the
+   subkind is not specified, it means `Lin` in order to be compatible
+   with variants and records in Links.
+
+    ```
+    links> sig f:forall e::Row(Any). () {Get:() => Int|e}-> Int fun f() {do Get}; f();
+    f = fun : () {Get:() => Int|_}-> Int
+    ```
+
+## Design choices
+
+It is necessary to have `xlin` for the same reason of having `linfun`
+in Links. For example, neither of the following functions has a more
+general type than the other one.
+
+```
+links> fun(x) {lindo L; x};
+fun : (a) {L:() =@ ()|_}-> a
+links> fun(x) {xlin; lindo L; x};
+fun : (a::Any) {L:() =@ ()|_::Lin}-> a::Any
+```
+
+## Compatibility
+
+* Compatible with all previous handler tests (except part of
+  polymorphic operations and effect sugar).
+* Not entirely compatible with FreezeML, SessionFail, etc.
+* Passes all tests with the flag disabled, except
+  * `!FAILURE: Operation polymorphism (2)`
+  * `!FAILURE: Operation polymorphism (3)`
+  * `!FAILURE: Typecheck example file examples/handlers/monadic_reflection.links`

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
@@ -1324,6 +1325,20 @@ module Untyped = struct
   let name = "effects"
 
   let program state program' =
+    (* (
+      match program' with
+        | (bindings, body) ->
+      (match body with
+        | None -> ()
+        | Some body -> 
+            print_string "---------- BEGIN desugarEffects input -----------\n";
+            let () = print_string "bindings:\n" in
+            let _  = if (bindings = []) then () else (print_string -<- show_binding) <| List.hd bindings in print_string "\n";
+            print_string "body:\n";
+            (print_string -<- show_phrase) body;
+            print_string "\n";
+            print_string "---------- END desugarEffects input -----------\n";)
+    ); *)
     let open Types in
     let tyenv = Context.typing_environment (context state) in
     let program' = program tyenv.tycon_env program' in

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