Combining effects and coeffects via grading

Written by ciaran16 (Ciaran Lawlor)
Published: 2016-09-17 (last updated: 2016-09-22)

(I didn't follow most of this)

What are coeffects? Computations make changes to the context (effects) and make demands from the context (coeffects)

Per-variable coeffects.

Type and coeffect system, coeffect meta languages

Interaction of effects and coeffects.

Examples

  • security levels (coeffect) masking non-determinism (effect)
  • Exceptions (effect) change linear reuse bounds (coeffect)

Core calculus - linear-lambda calculus with effect and coeffect types.

Graded monads for effects and graded comonads for coeffects.

Conclusion

Foundation for considering effect-coeffect interaction.

Further possibilities - exceptions interacting with security levels, non-determinism with probabilistic variables.

Graded distributive laws useful in other contexts.