Formal Verification of Monad Transformers

TL;DR

This paper introduces a domain-theoretic approach to formal verification of monad transformers, implemented in the Tycon library for Isabelle, enabling reasoning about axiomatic type classes without advanced type features.

Contribution

It develops a domain-theoretic model and a library that formalizes and verifies monad transformers in Isabelle, including invariants for their monad laws.

Findings

Successfully formalized three monad transformers in Isabelle

Established datatype invariants ensuring monad laws hold

Provided automation for class instantiation and subclass definition

Abstract

We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.