Kenji Maillard
INRIA
Designing Dijkstra Monads
Computational monads are a convenient algebraic gadget to uniformly represent a wide class of side effects in programming languages. Inspired by Dijkstra's work, we want to use predicate transformers to verify monadic programs. These predicate transformers can, however, be themselves uniformly represented as a monad. This observation led to a powerful verification technique in F*, which uses monads indexed by a predicate transformer monad, also known as Dijkstra monads. In previous work, we have shown that provided a syntactic presentation of a computational monad, we can mechanically derive the predicate transformer calculus and the Dijkstra monad. However, the class of computational monads that can be given such a syntactic presentation is somewhat restricted and does not account for interesting examples such as IO, nondeterminism, and probabilities. This new work explains how to go past these limitations by first decoupling the computational monad from the predicate transformer monad, only keeping the data of how to interpret the former in the latter, then showing how to recover Dijkstra monads from that data. The result is a unified framework encompassing monads merely axiomatized in the language, which enables reasoning about various new effects.
