Danel Ahman: A fibrational view on computational effects
Abstract: In this talk, I will give an overview of my work on the interplay between dependent types and computational effects. In particular, I will discuss the syntax and semantics of a dependently typed lambda calculus with computational effects based on a clear distinction between values and computations akin to Call-By-Push-Value and the Enriched Effect Calculus. The distinctive feature of this calculus is the computational sigma-type, which provides a uniform treatment of type-dependency in sequential composition, and which can also be used to give semantics to the effect system of the Idris language. In the talk, I will also discuss how one can extend this calculus with algebraic effects and their handlers, and show that in addition to being a convenient programming abstraction, the latter also provide a useful mechanism for reasoning about effectful computations.
The fibrational semantics of this calculus demonstrates that similarly to well-known results from the simply typed setting, it is also natural to model computational effects in the dependently typed setting using monads and adjunctions. In the talk, I will also discuss various examples of such fibrational models, e.g., based on families fibrations and liftings of adjunctions; simple fibrations and models of the Enriched Effect Calculus; Eilenberg-Moore resolutions of split fibred monads; and the fibration of continuous families of cpos and liftings of CPO-enriched adjunctions, so as to model general recursion.
