Skip to content

Effect Sugar

Jump to bottom
Samuel Novák edited this page Aug 30, 2021 · 5 revisions

[WIP]

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

Different options affect the Roundtrip 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: (for a more elaborate/realistic example, see [1])

    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, in this PR, 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. [2]

    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.

Clone this wiki locally