Type classes for mathematics in type theory
Type classes for mathematics in type theory
复制标题
DOI：
10.1017/s0960129511000119
复制
发表时间：
2011-08-01
影响因子：
0.5
通讯作者：
Van der Weegen, Eelis
中科院分区：
文献类型：
--
作者：
Spitters, Bas;Van der Weegen, Eelis
Coq 系统中引入一流类型类需要重新检查类型论中用于数学形式化的基本接口。我们提出了一套新的数学类型课程，并充分利用它们的独特功能，使以前被认为不可行的特别灵活的方法变得实用。因此，我们解决了传统的证明工程挑战，以及由于我们的雄心壮志而产生的新挑战，即在此基础上构建一个建设性分析库，其中任何抑制高效计算的抽象惩罚都被减少到最低限度。我们开发的基础包括代表标准代数层次结构的类型类，以及范畴论和通用代数的部分。在此基础上，我们为不同类型的数字构建了一组数学上合理的抽象接口，并使用分类语言和通用代数结构来简洁地表达。类型类的策略性使用使我们能够支持这些高级理论友好的定义，同时仍然能够实现高效的实现，而不受无端间接、转换或投影的阻碍。代数在语法和语义之间的相互作用中蓬勃发展。类似 Prolog 的类型类实例解析能力使我们能够方便地定义引用函数，从而方便了反射技术的使用。
The introduction of first-class type classes in the Coq system calls for a re-examination of the basic interfaces used for mathematical formalisation in type theory. We present a new set of type classes for mathematics and take full advantage of their unique features to make practical a particularly flexible approach that was formerly thought to be unfeasible. Thus, we address traditional proof engineering challenges as well as new ones resulting from our ambition to build upon this development a library of constructive analysis in which any abstraction penalties inhibiting efficient computation are reduced to a minimum. The basis of our development consists of type classes representing a standard algebraic hierarchy, as well as portions of category theory and universal algebra. On this foundation, we build a set of mathematically sound abstract interfaces for different kinds of numbers, succinctly expressed using categorical language and universal algebra constructions. Strategic use of type classes lets us support these high-level theory-friendly definitions, while still enabling efficient implementations unhindered by gratuitous indirection, conversion or projection.Algebra thrives on the interplay between syntax and semantics. The Prolog-like abilities of type class instance resolution allow us to conveniently define a quote function, thus facilitating the use of reflective techniques.