Layered Indexed Effects: Foundations and Applications of Effectful Dependently Typed Programming

Layered Indexed Effects

Foundations and Applications of Effectful Dependently Typed Programming

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)


Programming and reasoning about effects in a functional programming language is a long-standing research problem. While monads have been a widely adopted common basis for effects in general purpose languages like Haskell, to improve modularity, compositionality, and precision of static reasoning, many refinements and alternatives have been developed, including algebraic effects, graded monads, parameterized monads, Hoare monads, Dijkstra monads, productors, polymonads, and combinations thereof, to only name a few.

To benefit from all these approaches, we propose a new language feature, layered indexed effects, and implement it as an extension to the F⭑ programming language. Using our feature, programmers can extend F⭑ with user-defined effect disciplines in all the aforementioned styles. Layered indexed effects provide a type-and-effect directed elaboration algorithm which allows programs to be developed in applicative syntax and to be reasoned about in a programmer-chosen abstraction, hiding the underlying semantic representations that justify a given effect-typing discipline. Being dependently typed, F⭑ supports developing both the semantic models and reasoning about client programs within the same framework.

We evaluate our work on four case studies: a generic framework for operation-indexed algebraic effects and handlers, together with the derivation of a Hoare-style program logic to reason about their stateful behavior; a new graded monad for stateful information flow control; a library of verified low-level message formatters structured as a parameterized monad upon a Hoare monad; and a hierarchy of effects mixing graded monads, Hoare monads, polymonads and continuations, to structure programs and proofs in a concurrent separation logic. Additionally, layered indexed effects have also simplified the core of F⭑, allowing us to derive basic Dijkstra monad constructions in F⭑ that were previously primitive. Given our positive experience, we speculate that other dependently typed languages might benefit from layered indexed effects too.