Dynamic handlers

[forell]

Lexical effect handlers are nice and disciplined, but make some things, like lightweight threads, difficult to express. Fram used to allow first-class labels to be generated and then used by multiple handle expressions, but that functionality had to be removed when the return and finally clauses were moved from handle to first-class handler creation with handler in bc226d0, since the type and effect of the delimiter are no longer visible in the handler type.

Some form of dynamic handlers should be implemented in Fram. Part of the necessary work has already been done in c237db2, allowing convenient encoding of dynamic handlers in terms of shift₀ and reset₀, but nothing is exposed to the programmer yet. The old tests and example for first-class labels that were removed in bc226d0 should potentially be reintroduced in some way.

[ppolesiuk]

After discussion with @forell, we agreed on the approach to dynamic handlers. In general, dynamic handlers are just syntactic sugar to parametrized version of shift₀/reset₀ control operators. To be more specific, we should introduce the following changes and features. (Suggested concrete syntax is just a proposition, and I'm open to other suggestions.)

Label type

Label type contains a telescope of named parameters that describes types and values attached to the delimiter. This additional parameters allows to use encoding similar to the one proposed by Piróg et al., but simplified (where encoding of state monad is changed to the reader). For instance, the ecoding of backtracking effect will use the following label type, where DT and DE are delimiter's type and effect, as in Piróg et al.'s translation.

label E
  { DT, DE
  , flip : (Bool ->[|DE] DT) ->[|DE] DT
  , fail : {type T} -> (T ->[|DE] DT) ->[|DE] DT
  } @ DT / DE

The regular user should never see such a type due to syntactic sugar described later in this post.

Control effects

We can reuse effect construct for dynamic stuff. The effect construct always uses label named label, as we do for lexical handlers. Additionally, it binds named things of types and kinds described by a type of the label. For instance, we can write (assuming that the label has type shown above):

effect {flip} / k => flip k

However, the regular user should never use this construct (for dynamic stuff) directly.

Syntactic sugar for dynamic signatures

We can write signatures of dynamic effects in the following way.

dynsig BT =
  { flip : Bool
  , fail : { type T } => Bool
  }

Similarly to records, it can be desugared into ADT with a single constructor (named BT) with a single named parameter label of a type shown in Label type section, where E is the last parameter added to BT ADT. Additionally the following methods are generated.

method flip {E, self : BT E = BT { label }} = effect {flip} / k => flip k
method fail {E, type T, self : BT E = BT { label }} = effect {fail} / k => fail k

Dynamic handlers

Dynamic handler is just a reset₀ control operator parametrized by named things attached to the label type. For instance, for the backtracking handler we could write the following.

dynhandle l
  { flip = fn k => List.append (k True) (k False)
  , fail = fn _ => []
  }
  return x => [x]
in ...

Of course, we can omit DT and DE parameters, as they can be infered. But we can provide them if we want.

dynhandle l
  { DT = List _
  , flip = fn k => k True + k False
  , fail = fn _ => []
  }
  return x => [x]
in ...

The parameter l should have a label type or a record with label field of label type. I'm not sure if we want to allow both of these options. Allowing only the second seems reasonable, because the regular user will never see label types outside a record.

Generating fresh labels

Fresh labels can be generated by dynlabel construct (I prefer to use keyword different than label just to allow using label in places where a regular term identifier is expected). For instance, we can write:

dynlabel l = BT in ...

I can imagine, a more general dynamic signatures, that contains additional fields that are constant to the effect instance, but not to particular handler. These parameters could be passed at label allocation:

dynlabel l2 = GenSig { foo = 42, bar = 13 } in ...

If we use this approach, then the meaning of dynlabel could be the following: in dynlabel x = e the code e is executed in environment, where label identifier points to freshly allocated label. However this will require some changes in the type inference: we need to extend the environment by a variable label whose type is not known to be label yet, because we cannot guess exact list of named parameters. This can be easily achieved by allowing unification variables to describe type of the label.