Free theorems involving type constructor classes: functional pearl
Free theorems involving type constructor classes: functional pearl
复制标题
涉及类型构造函数类的自由定理：函数珍珠
DOI：
10.1145/1596550.1596577
复制
发表时间：
2009
影响因子：
4.6
通讯作者：
J. Voigtländer
中科院分区：
文献类型：
--
作者：
J. Voigtländer
自由定理很有魅力，它允许仅从程序的（多态）类型推导出有关程序的有用语句。我们不仅展示了如何从普通类型的多态性，而且还从受类约束限制的类型构造函数的多态性中获得这些定理。我们的主要应用领域是 monad，它构成了 Haskell 可能最流行的类型构造函数类。为了展示更广泛的范围，我们还采用一种透明的方式将差异列表引入程序中，并赋予简洁且通用的正确性证明。
Free theorems are a charm, allowing the derivation of useful statements about programs from their (polymorphic) types alone. We show how to reap such theorems not only from polymorphism over ordinary types, but also from polymorphism over type constructors restricted by class constraints. Our prime application area is that of monads, which form the probably most popular type constructor class of Haskell. To demonstrate the broader scope, we also deal with a transparent way of introducing difference lists into a program, endowed with a neat and general correctness proof.
快速而宽松的推理在道德上是正确的
影响因子：
--
作者：
Danielsson N
通讯作者：
Danielsson N