Effect Sugar

Links has fine-grained syntactic sugar for Effects that allows one to select exactly what (de)sugaring they want.

Most of the syntactic sugar is only active when the setting effect_sugar is set to true. When this is the case, the fine-grained effect_sugar_policy is used to select which components of the effect sugar one wants to activate.

The available options for effect_sugar_policy are listed below. This setting is a multi-option, meaning one can select multiple of these, separated by commas, e.g.:

@set effect_sugar_policy "presence_omit,alias_omit,contract_operation_arrows;"

All options also have shortcuts, meaning the above is equivalent to:

@set effect_sugar_policy "pres,alias,contract;"

Before describing the different parts of effect sugar, note that Links also has meta-options for convenient selecting of multiple of these:

• all - enables all of the options
• none - disables all of the options
• default - resets the setting to default, which is currently:
  • presence_omit
  • alias_omit
  • contract_operation_arrows
  • arrows_curried_hide_fresh

Note that when setting default, you still need to surround it in quotes.

A short version of this documentation is available in Links by entering:

@help effect_sugar_policy;

Parts of Effect Sugar and associated options

Shared Effect Variables

The basis of large part of the effect sugar is that some effect variables are shared across multiple effect rows. Row polymorphism requires that all rows with a particular row variable mention the same labels - however, we do not need to always see these, and this introduces noise in the types.

There is also the Implicit Shared Effect Variable which gets the special status. It behaves like any shared effect variable, but can be kept hidden. The last (rightmost arrow or type alias, sometimes not exclusively, see final_arrow below) effect variable in a type will be assumed to be this ISEV.

Sugar options

Different options affect the Roundtrip[^1] printer output [O], the input (parser or desugaring) [I], or both [IO].

• [O] presence_omit [shortcut pres] - hide presence-polymorphic operations in open effect rows

  sig handleE : (() {E:() {}-> ()|e}~> ()) -> (() {E{_}|e}~> ())
                                                  ^^^^^^^^
  fun handleE(f) {
    fun () {
      handle(f()) { case E(resume) -> resume(()) }
    }
  }
  ↦
  handleE : (() {E:() {}-> ()|e}~> ()) -> () { |e}~> ()
                                             ^^^^^
  ↦ (this is on an arrow, so it reduces further to)
  handleE : (() {E:() {}-> ()|_}~> ()) -> () ~> ()
                                             ^^
  

  • [I]: The inverse of pres is performed by default if effect_sugar is true. See below in Desugaring: Operation Propagation and Aliases.

• [O] alias_omit [shortcut alias] - hide empty (or emptied using presence_omit above) effect rows in the last argument of type alias applications

  typename Ord = [| Lower | Greater | Equal |];
  typename Order(a, e::Eff) = (a, a) ~e~> Ord;
  
  sig ord : Order(a, { |_})
                     ^^^^^
  fun ord(x, y) { if (x == y) Equal else if (x < y) Lower else Greater }
  ↦
  ord : Order(a)
             ^^^
  

  • [I]: The inverse of alias is performed by default if effect_sugar is true. See below in Desugaring: Operation Propagation and Aliases.

• [O] arrows_show_implicit_effect_variable [shortcut show_implicit] - display the implicit shared effect on function arrows, and hide fresh effect variables instead. See examples from #986 at the bottom.

  # without `arrows_show_implicit_effect_variable`:
  
  sig map : ((a) ~e~> b, [a]) ~e~> [b]
                 ^^^^         ^^^^
  fun map(f, lst) { switch(lst) { case [] -> [] case (x::xs) -> f(x) :: map(f, xs) }}
  ↦
  map : ((a) ~> b, [a]) ~> [b]
             ^^         ^^
  
  sig map' : ((a) ~e~> b) -> ([a]) ~e~> [b]
                  ^^^^             ^^^^
  fun map'(f)(lst) { switch(lst) { case [] -> [] case (x::xs) -> f(x) :: map'(f)(xs) }}
  ↦
  map' : ((a) ~> b) -_-> ([a]) ~> [b]
              ^^    ^^^^         ^^
                    ||||
                    (fresh variables appearing; note that in this particular case of
                     a curried function, the next setting
                     `arrows_curried_hide_fresh` may take effect,
                     however, in general, fresh vars will appear)
  
  ↦ (with `arrows_show_implicit_effect_variable`)
  map : ((a) ~b~> c, [a]) ~b~> [c]
             ^^^^         ^^^^
  map' : ((a) ~b~> c) -> ([a]) ~b~> [c]
              ^^^^    ^^       ^^^^
  

• [O] arrows_curried_hide_fresh [shortcut chf] - in curried functions, the "collection" arrows (function being partially applied to arguments, collecting them) are assumed to have fresh effect variable, and these are not shown. See examples from #986 at the bottom.

  # see above, without `arrows_show_implicit_effect_variable`
  
  # without `arrows_curried_hide_fresh`:
  map' : ((a) ~> b) -_-> ([a]) ~> [b]
                    ^^^^
  ↦ (action of `arrows_curried_hide_fresh`)
  map' : ((a) ~> b) -> ([a]) ~> [b]
                    ^^
  

• [I] all_implicit_arrows_share [shortcut all_arrows]: All arrows with implicit effect variables will be unified. This is an experimental setting. It is related to chf above.

  sig f : (a) -> (b) -> (c) -> d
  ↦
  sig f : (a) -e-> (b) -e-> (c) -e-> d
  

• [O] contract_operation_arrows [shortcut contract] - contracts operation arrows in effect rows in the following cases:

  E:(a) {}-> b    ↦ E:(a) -> b
        ^^^^              ^^
  E:() {}-> a     ↦ E:a
    ^^                ^
  
  
  sig f : () {E:() {}-> a}-> a
  fun f() { do E };
  ↦
  f : () {E:a}-> a
  

  • [I]: The inverse of contract is performed always - irrespective of the effect_sugar setting.

• [IO] open_default [shortcut open] - effect rows are open by default; uses {fields| .} to mean a closed row

  # without `open_default`
  sig f : () {E:() {}-> a}-> a
             ^^^^^^^^^^^^^
  fun f() { do E }
  
  sig g : () {E:() {}-> a|_}-> a
             ^^^^^^^^^^^^^^^
  fun g() { do E }
  
  f : () {E:() {}-> a}-> a
               ^^    ^
  g : () {E:() {}-> a|_}-> a
               ^^    ^^^
  
  ↦ (applying `open_default`)
  f : () {E:() { | .}-> a| .}-> a
                 ^^^^    ^^^^
  g : () {E:() { | .}-> a}-> a
                 ^^^^    ^
  
  # this works well together with arrow contractions
  # (see the options above)
  
  ↦ (applying both `open_default` and `contract_operation_arrows`)
  f : () {E:() -> a| .}-> a
                   ^^^^
  g : () {E:() -> a}-> a
                   ^
  

• [I] final_arrow_shares_with_alias [shortcut final_arrow]:

  Where a last arrow is followed by a type alias containing an effect variable as its range, and the arrow has an implicit effect variable, the two may unify = share the effect variable.

  Consider the (minimal) example below:

  typename S(a) = (v:a, ord:(a,a) ~> Bool);
  # really S(a, e::Eff) = (v:a, ord:(a,a) ~e~> Bool);
  
  sig upd_s : (a, S(a)) ~> S(a)
  # sig upd_s : (a, S(a, { |e})) ~e~> S(a, { |e})
  #                         ^-----^-----------^
  fun upd_s(v', s) {
    if (s.ord(v', s.v))
      (s with v=v')
    else
      s
  }
  

  The above example is a structure which carries around some helper which has an effect variable, and this helper is used when transforming it. Following the original rules, this would desugar into:

  sig upd_s : (a, S(a, { |e})) ~f~> S(a, { |e})
                          ^-----------------^
  

  where e and f are different - this would, however be the wrong type.

  Instead the intended and inferred type is:

  sig upd_s : (a, S(a, { |e})) ~e~> S(a, { |e})
                          ^-----^-----------^
  

  where the effect variables on the arrow and the aliases unified.

  On the other hand, in some cases, we do not want these to unify; consider:

  sig handleOp : (Comp(a, {Op:()|_})) -> Comp(a)
  fun handleOp(f)() { handle(f()) { ... case Op(r) -> ... }}
  
  # we want the above to mean
  # sig handleOp : (Comp(a, {Op:()|e})) -f-> Comp(a, {Op{_}|e})
  #                                ^------------------------^
  

  where again e and f are different, except here this is intended.

  To this end, the effect desugaring pass introduces a fresh flexible effect variable on the last arrow (if its range is an alias that can have a shared effect), and the type inference will correctly unify/not unify it with the effect variable on alias.

  To illustrate, a signature like upd_s above transforms as follows:

  sig upd_s : (a, S(a)) ~> S(a)
  
  ↦ (effect sugar)
  sig upd_s : (a, S(a, { |e})) ~%f~> S(a, { |e})
                          ^------------------^
  
  ↦ (type inference/unification)
  (if the internal function is used)
  sig upd_s : (a, S(a, { |e})) ~e~> S(a, { |e})
                          ^-----^-----------^
  (otherwise)
  sig upd_s : (a, S(a, { |e})) ~f~> S(a, { |e})
                          ^-----------------^
                               e ≠ f
  

  This way, the two possibilities (exemplified by S, where the effect needs to be shared on the arrows transforming it; and Comp, where this is not the case) are transformed by desugaring and type inference to the intended types.

---

[^1]: The old printer also did some sugaring, mostly hiding the implicit shared effect variable. This is not described here, because I (Samo) know little about the details, and it is only affected by effect_sugar, not effect_sugar_policy.