Effect Sugar

Links has fine-grained syntactic sugar for Effects that allows one to select exactly what (de)sugaring they want. This syntactic sugar is concerned only with types (both inferred and provided by user).

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] 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
                 ^

[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
```
[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 longer/more realistic example see [2])
```
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.

Desugaring: Operation Propagation and Aliases

When effect_sugar is true (and irrespective of effect_sugar_policy), the desugaring pass tries to detect when there is an effect row missing as the last argument to a type application (see alias_omit above, this is the inverse). When this is the case, a new effect row with the implicit shared effect variable is inserted in that place.

The desugaring pass also propagates operation labels: this means that it will collect all operation labels associated with each effect variable (separately!), and then inserts each label as polymorphic in its presence (with a fresh presence variable) into the rows that have that variable and do not already contain the label.

This is a form of kind inference and unification that happens during the desugaring pass.

An example:

sig handleL : (() {L:()|_}~> ()) -> (() ~> ())
fun handleL(f) {
  fun () {
    handle(f()) { case L(resume) -> resume(()) }
  }
}
# handleL = fun : (HasL ({ |a})) -> () {L{_}|a}~> ()

Note that this is compatible with type aliases containing operation labels within: these labels will also be propagated across the type. Example:

typename HasL = () {L:()|_}~> ();
# HasL = a::Eff.() {L:() {}-> ()|a::Eff}~> ()

sig handleL : (HasL) -> (() ~> ())
fun handleL(f) {
  fun () {
    handle(f()) { case L(resume) -> resume(()) }
  }
}
# handleL = fun : (HasL ({ |a})) -> () {L{_}|a}~> ()

Footnotes

[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.

[2]: This is an excerpt from a program that uses Maps based on trees. The keys are allowed to be arbitrary types, and hence we need to provide an ordering function.

typename Ord = [| Lower | Greater | Equal |];
typename Order(a) = (a, a) ~> Ord;
# Order(a, e::Eff) = (a, a) ~e~> Ord;

typename Tree(a, b) = mu t. [| Node:(left:t, key:a, value:b, right:t) | Leaf |];
typename Map(a, b) = (ord:Order(a), tree:Tree(a,b));
# Map(a, b, e::Eff) = (ord:Order(a, { |e}), tree:Tree(a,b));

[...]

sig upd_map : (a, b, Map(a,b)) ~> Map(a,b)
# sig upd_map : (a, b, Map(a,b,{ |e})) ~e~> Map(a,b,{ |e})
#                                 ^-----^--------------^
fun upd_map(key, value, mp) {
  var (ord=ord, tree=tree) = mp;
  (mp with tree = upd_tree(ord, key, value, tree))
}

The intended (and inferred) type of upd_map is:

upd_map : (a, b, Map(a,b,{ |e})) ~e~> Map(a,b,{ |e})
                            ^-----^--------------^

where the effect variable e is shared across both the aliases and the arrow - this is because here, to transform a Map, we need to use the helper it carries around.

The type that resulted from desugaring (before this PR) was however:

upd_map : (a, b, Map(a,b,{ |e})) ~f~> Map(a,b,{ |e})
                            ^--------------------^

where e ≠ f.

Provide feedback

Saved searches