Type Classes and Overloading in Higher-Order Logic
Type Classes and Overloading in Higher-Order Logic
复制标题
高阶逻辑中的类型类和重载
DOI：
10.1007/bfb0028402
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
M. Wenzel
中科院分区：
文献类型：
--
作者：
M. Wenzel
类型类和重载是独立的概念，它们都可以添加到Church和Gordon传统的简单高阶逻辑中，而不需要更多的逻辑表达能力。特别是，模型理论问题不受影响。我们的元学结果可以作为像Isabelle/Pure这样的系统的基础，为用户提供haskell风格的有序多态性作为扩展的语法特性。后者可用于描述具有单一载波类型和固定操作签名的简单抽象理论。
Type classes and overloading are shown to be independent concepts that can both be added to simple higher-order logics in the tradition of Church and Gordon, without demanding more logical expressiveness. In particular, model-theoretic issues are not affected. Our metalogical results may serve as a foundation of systems like Isabelle/Pure that offer the user Haskell-style order-sorted polymorphism as an extended syntactic feature. The latter can be used to describe simple abstract theories with a single carrier type and a fixed signature of operations.