Equational Reasoning for MTL Type Classes

TL;DR

This paper explores equational reasoning for Haskell MTL type classes, proposing axioms for MonadReader and MonadWriter, and establishing equivalences between different axiomatizations to improve reasoning about these classes.

Contribution

It introduces formal laws for MonadReader and MonadWriter, and proves equivalence between alternative axiomatizations, enhancing reasoning capabilities in Haskell's MTL.

Findings

Established equivalence of two axiomatizations for MonadReader.

Established equivalence of two axiomatizations for MonadWriter.

Identified patterns in method choices that could inspire new MTL developments.

Abstract

Ability to use definitions occurring in the code directly in equational reasoning is one of the key strengths of functional programming. This is impossible in the case of Haskell type class methods unless a particular instance type is specified, since class methods can be defined differently for different instances. To allow uniform reasoning for all instances, many type classes in the Haskell library come along with laws (axioms), specified in comments, that all instances are expected to follow (albeit Haskell is unable to force it). For the type classes introduced in the Monad Transformer Library (MTL), such laws have not been specified; nevertheless, some sets of axioms have occurred in the literature and the Haskell mailing lists. This paper investigates sets of laws usable for equational reasoning about methods of the type classes MonadReader and MonadWriter and also reviews analogous earlier proposals for the classes MonadError and MonadState. For both MonadReader and MonadWriter, an equivalence result of two alternative axiomatizations in terms of different sets of operations is established. As a sideline, patterns in the choice of methods of different classes are noticed which may inspire new developments in MTL.