  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.
