论文标题
MTL类型类的方程推理
Equational Reasoning for MTL Type Classes
论文作者
论文摘要
直接在方程推理中直接使用代码中发生的定义的能力是功能编程的关键优势之一。除非指定特定的实例类型，否则这是不可能的，因为对于不同的实例，类方法可以不同。为了允许在所有情况下进行统一的推理，Haskell库中的许多类型类都与评论中指定的法律（Axioms）一起，预计所有实例都将遵循（尽管Haskell无法强制强制）。对于Monad Transformer库（MTL）中引入的类型类别，尚未指定此类定律；然而，文献和Haskell邮件列表中已经出现了一些公理。本文调查了一组适用于有关类型类别的方法和Monadwriter方法的方程推理的法律，还审查了Monaderror和Monadstate类的类似早期建议。对于Monadreader和Monadwriter，就不同的操作集而言，两种替代公理的等效性结果。作为场边，注意到不同类别方法的模式可能会激发MTL中的新发展。
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.
