Algebraic effects

The algebraic effects system in Dex is (currently) very experimental and deliberately limited.

Effects definitions are given like so:

effect Exn
      V---- name
  ctl raise : (a: Type) ?-> Unit -> a
  ^-- policy  ^---------------------- signature

A new effect named Exn is introduced here by the Exn keyword. Effects are not parametric and there is no syntax for introducing binders at the effect level.

This effect declares one effect operation (but could declare several, each on its own line) named raise. Effect operations in Dex specify a resumption policy that is used to optimize certain special cases:

• ctl indicates that no special resumption policy is being followed. The operation might not resume, or it could resume multiple times (note: resuming more than once is not actually supported at this time).
• def indicates that the operation will resume exactly once, in tail position. This allows Dex to implement it as a dynamically scoped/virtual function.
• jmp indicates that the operation will not resume. This allows Dex to implement it using more conventional exception-handling mechanisms.