Constructive Type Classes in Isabelle
Constructive Type Classes in Isabelle
复制标题
伊莎贝尔的构造类型类
DOI：
10.1007/978-3-540-74464-1_11
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
M. Wenzel
中科院分区：
文献类型：
--
作者：
Florian Haftmann;M. Wenzel
我们在Isabelle的逻辑框架内重新考虑Haskell风格类型类的著名概念。到目前为止，Isabelle中的公理类型类仅仅将逻辑方面解释为类型上的谓词，而操作部分只是基于原始重载的约定。我们对构造类型类的更详细的方法提供了与Isabelle语言环境的无缝集成，Isabelle语言环境能够统一管理操作和逻辑属性。因此，我们联合收割机了类型类的便利性和区域设置的灵活性。此外，我们构造的字典条款来自类型系统的概念。这种额外的内部结构提供了令人满意的类型类基础，并支持进一步的应用，如代码生成和理论和定理的导出到没有类型类的环境中。
We reconsider the well-known concept of Haskell-style type classes within the logical framework of Isabelle. So far, axiomatic type classes in Isabelle merely account for the logical aspect as predicates over types, while the operational part is only a convention based on raw overloading. Our more elaborate approach to constructive type classes provides a seamless integration with Isabelle locales, which are able to manage both operations and logical properties uniformly. Thus we combine the convenience of type classes and the flexibility of locales. Furthermore, we construct dictionary terms derived from notions of the type system. This additional internal structure provides satisfactory foundations of type classes, and supports further applications, such as code generation and export of theories and theorems to environments without type classes.