Implement default handlers

[dhil]

The task is to implement (user-definable) default handlers, a useful abstraction for modular programming. A default handler provides, as the name implies, a default interpretation of one or more given operations. A default handler is always invoked at the top-level, and it does not expose the continuation to programmers. Instead the return value of the handler is used as the interpretation of the operation.

Use case: Suppose you implement library X, whose public interface exposes some effectful functions, that may have a sensible default interpretation, but is left open to be extensible.

Since Links has structural operations, the default handler must necessarily be provided at the invocation site of an operation. Currently, I have the following syntax in mind

# Default handler for `Yield'.
fun consume(operation) { 
  switch (operation) {
    case Yield(_) -> ()
  }
}
fun yield(x) {do Yield(x) with consume}

The idea is that, if the operation Yield reaches the top-level, then the runtime invokes the provided function consume to give an interpretation to Yield. The interesting question is what are the types of yield and consume?

The function consume should take some reified operation as input, I reckon it could be typed naturally as consume : ([|Yield:_|]) -> ().

The type of yield is more interesting, because we cannot simply type it as

yield : (a) {Yield:(a) -> () |_}-> ()

because then we would be forced to supply a handler for Yield which defeats the purpose of default handlers. Similarly, we cannot type it as

yield : (a) {Yield{_} |_}-> ()

either, as this would lead to inconsistent (and aguably strange behaviour) for operations that are polymorphic in their presence. I think we need another notion of presence to signify that handling of a given operation is optional; I am not clear on the syntax yet, but perhaps something along the lines of

yield : (a) {Yield:?(a) -> () |_}-> ()

I suppose the question mark may be a no-go due to session type syntax. Nevertheless, the idea is that the row {Yield:?(a) -> () |_} would unify with {wild}. Similarly, the following should be true too {Yield:?(a) -> () |e} ~ {Yield:(a) -> () |f} == {Yield:(a) -> () |f'}. The last equation says that in the presence of non-optional operation, the Yield operation with a default interpretation will be handled by a regular user-defined handler for Yield.

[dhil]

Some of the syntax from the previous row-system still seems to be in place. For example, the surface syntax supports presence with a particular type (which is exactly the kind of thing I discussed above)

sig f : () {Foo{:Int}}-> ()
fun f() { () }

I guess the annotation Foo{:Int} used to mean that if Foo is present, then it has type Int. However, now it is interpreted the same as presence, that is Foo{:Int} and Foo:Int are interchangeable.

I suppose we can rewire the syntax back to its previous interpretation. Then the type of yield would be typeset as

yield : (a) {Yield{:(a) -> ()} |_}-> ()