Fibred Computational Effects
share
Dependent types provide a lightweight and modular means to integrate programming and formal program verification. In particular, the types of programs written in dependently typed programming languages (Agda, Idris, F*, etc.) can be used to express specifications of program correctness. These specifications can vary from being as simple as requiring the divisor in the division function to be non-zero, to as complex as specifying the correctness of compilers of industrial-strength languages. Successful compilation of a program then guarantees that it satisfies its type-based specification. While dependent types allow many runtime errors to be eliminated by rejecting erroneous programs at compile-time, dependently typed languages are yet to gain popularity in the wider programming community. One reason for this is their limited support for computational effects, an integral part of all widely used programming languages, ranging from imperative languages, such as C, to functional languages, such as ML and Haskell. For example, in addition to simply turning their inputs to outputs, programs written in these programming languages can raise exceptions, access computer's memory, communicate over a network, render images on a screen, etc. Therefore, if dependently typed programming languages are to truly live up to their promise of seamlessly integrating programming and formal program verification, we must first understand how to properly account for computational effects in such languages. While there already exists work on this topic, ingredients needed for a comprehensive theory are generally missing. For example, foundations are often not settled; available effects may be limited; or effects may not be treated systematically. In this thesis we address these shortcomings by providing a comprehensive treatment of the combination of dependent types and general computational effects.
READ FULL TEXT