Generic and flexible defaults for verified, law-abiding type-class instances
Generic and flexible defaults for verified, law-abiding type-class instances
复制标题
经过验证、遵守法律的类型类实例的通用且灵活的默认值
DOI：
10.1145/3331545.3342591
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Newton, Ryan R.
中科院分区：
文献类型：
--
作者：
Scott, Ryan G.;Newton, Ryan R.
依赖类型语言允许程序员通过简单地将类型类法则编码为类方法来陈述和证明类型类法则。但是，这些方法的编写实现经常让位于大量的例行程序，样板代码，并根据所涉及的法律，这些证明的大小可以超线性增长的datasthees.We的大小提出了一种技术，利用数据类型泛型编程自动化了大量的这种样板。我们观察到，任何代数数据类型都有一个等价的表示类型，它由更简单、更小的类型组成，这些类型更容易证明定理。通过构造一个数据类型和它的表示类型之间的同构，我们通过重用表示类型上的相应证明来推导原始数据类型的证明。我们的工作是通用的，不需要先进的自动化技术，如战术系统。作为这一主张的证据，我们在Haskell库中实现了这些想法，该库定义了标准基础库中类的方法和证明义务的通用规范实现。
Dependently typed languages allow programmers to state and prove type class laws by simply encoding the laws as class methods. But writing implementations of these methods frequently give way to large amounts of routine, boilerplate code, and depending on the law involved, the size of these proofs can grow superlinearly with the size of the datatypes involved.We present a technique for automating away large swaths of this boilerplate by leveraging datatype-generic programming. We observe that any algebraic data type has an equivalentrepresentation typethat is composed of simpler, smaller types that are simpler to prove theorems over. By constructing an isomorphism between a datatype and its representation type, we derive proofs for the original datatype by reusing the corresponding proof over the representation type. Our work is designed to be general-purpose and does not require advanced automation techniques such as tactic systems. As evidence for this claim, we implement these ideas in a Haskell library that defines generic, canonical implementations of the methods and proof obligations for classes in the standard base library.
登录
查看更多内容
Haskell 的通用派生机制
影响因子：
2.3
作者：
José Pedro Magalhães;A. Dijkstra;J. Jeuring;Andres Löh
通讯作者：
Andres Löh
依赖类型理论中的泛型程序和证明的宇宙
DOI：
10.5555/985799.985801
发表时间：
2003
期刊：
Nord. J. Comput.
影响因子：
--
作者：
Marcin Benke;P. Dybjer;Patrik Jansson
通讯作者：
Patrik Jansson
使用构造类型理论验证 haskell 程序
DOI：
10.1145/1088348.1088355
发表时间：
2005
期刊：
ArXiv
影响因子：
--
作者：
Andreas Abel;Marcin Benke;Ana Bove;John Hughes;U. Norell
通讯作者：
U. Norell
轻柔的悬浮艺术
影响因子：
--
作者：
Chapman J
通讯作者：
Chapman J
使用单例进行依赖类型编程
DOI：
--
发表时间：
2013
期刊：
ACM SIGPLAN Symposium/Workshop on Haskell
影响因子：
--
作者：
R. Eisenberg;Stephanie Weirich
通讯作者：
Stephanie Weirich