Aseem Rastogi, Microsoft Research, India
Guido Martínez, CIFASIS-CONICET, Argentina
Aymeric Fromherz, Microsoft Research & CMU, USA
Tahina Ramananandro, Microsoft Research, USA
Nikhil Swamy, Microsoft Research, USA
(In submission)
Proving properties about effectful programs is hard. New application-specific abstractions based on indexed monads can help simplify programming and proving. However, existing languages lack support to develop and use such abstractions.
The main contribution of this paper is a type-and-effect system that enables program proof developers to design new effect-typing disciplines based on indexed monads, making proofs simpler and more abstract and allowing programs to be developed in a direct, applicative syntax while automatically elaborating them into a core language of pure, total functions where the monadic structure is made explicit.
We have implemented our system as a new feature in the F⭑ programming language, enhancing its existing user-defined effect system to cover all forms of indexed monads. In doing so, we have also simplified the core language of F⭑, allowing us to derive basic Dijkstra monad constructions in F⭑ that were previously primitive.
Finally, we present several case studies developing new indexed monad constructions to structure program proofs in settings including information flow control, algebraic effects, and low-level binary format parsers.