类型论中数学的类型类
Type Classes for Mathematics in Type Theory
摘要：
在Coq系统中引入第一类类型类要求重新检查用于类型论中数学形式化的基本接口。我们提出了一套新的类型类的数学，并充分利用其独特的功能，使实际的一个特别灵活的方法，以前认为是不可行的。因此，我们既解决了传统的证明工程的挑战，也解决了新的挑战，因为我们的目标是在此基础上建立一个建设性的分析库，在这个库中，抑制有效计算的抽象惩罚被减少到最低限度。我们开发的基础包括代表标准代数层次结构的类型类，以及范畴论和泛代数的部分。在此基础上，我们建立了一套数学健全的抽象接口，不同种类的号码，简洁地表示使用范畴语言和通用代数结构。类型类的策略性使用让我们支持这些高级理论友好的定义，同时仍然能够有效地实现不受无偿间接，转换或投影的阻碍。代数在语法和语义的相互作用下蓬勃发展。类型类实例解析的类似Prolog的能力允许我们方便地定义一个引用函数，从而方便了反射技术的使用。
英文摘要：
The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization 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 formerly thought infeasible. Thus, we address both 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 abstraction penalties inhibiting efficient computation are reduced to a minimum. The base 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
