Computational applications of calculi based on monads

Pietro Cenciarelli

Abstract:

This thesis studies various manifestations of monads in the mathematics of computation and presents three applications of calculi based on monads.

The view that monads provide abstract mathematical interpretations of computational phenomena led E. Moggi to use the internal language of a category with a strong monad, which he called the computational lambda calculus, for describing denotational semantics of programming languages. Moggi argued that models of complicated forms of computation could be described modularly by using semantic constructors for manipulating monads.

For the first application, we describe a theory of exceptions in the computational lambda calculus and give a computationally adequate interpretation of a fragment of ML, including the exception handling mechanism, in models of this theory. To our knowledge no other model of ML exceptions is available in the literature to date. We also show that normalization fails when exceptions are added to the simply typed lambda calculus.

Building on top of the computational lambda calculus, A.M. Pitts proposed a predicate calculus to reason about the evaluation properties of programs: the Evaluation Logic. Following the tenets of synthetic domain theory, we interpret this logic in an ambient category with set-like structure and a fully reflective subcategory of domains with a monad for interpreting computation. We establish abstract conditions under which the monad extends to the ambient category to ensure good interaction with the logical structure. We also show that a monad and first order logical structure yield suitable evaluation relations, which can be used to give a standard interpretation of Evaluation Logic when higher order structure is not available.

For the second application, we focus on side effects and investigate the use of Evaluation Logic in partial correctness reasoning. We show that, under fairly common circumstances, monads for side effects admit an extension to the ambient category which is more natural than that described for arbitrary monads and we validate special axioms for members of this class. The resulting theory of computation with side effects is then put to work on a textbook example of partial correctness specification.

For our third application, we consider Moggi's modular approach to denotational semantics. We develop the theory of this approach by determining which equations are preserved by a fairly general class of semantic constructors and which ones are reflected (conservativity). Moreover, we establish a correspondence between categories of computational models and categories of theories of the metalanguage, along the lines of Gabriel-Ulmer duality, in a type-theoretic framework. Using the Extended Calculus of Constructions, we develop a semantics for parallel composition by combining elementary notions of computation defined independently and we use LEGO to prove properties of such semantics formally.

ECS-LFCS-96-346.

This report is available in the following formats:

Previous | Index | Next