MTL型类的等式推理
Equational Reasoning for MTL Type Classes
摘要：
在等式推理中直接使用代码中出现的定义的能力是函数式编程的关键优势之一。这在Haskell类型的类方法中是不可能的，除非指定了特定的实例类型，因为类方法可以为不同的实例定义不同的方法。为了允许所有实例的统一推理，Haskell库中的许多类型类都带有在注释中指定的定律（公理），所有实例都应该遵循这些定律（尽管Haskell无法强制它）。对于在Monad Transformer Library（MTL）中引入的类型类，这样的定律还没有被指定;然而，在文献和Haskell邮件列表中已经出现了一些公理集。本文探讨了一套法律适用于等式推理的方法的类型类MonadReader和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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
