数据类型通用编程方法的正式比较
摘要：数据类型通用编程通过使函数能够在不同类型上统一操作，增加了程序的抽象性和重用性。多年来已经提出了许多泛型编程的方法，其中大多数用于Haskell，但最近也用于依赖类型的语言，例如Agda。不同的方法在表达能力、易用性和实现技术方面有所不同。虽然在比较不同方法方面已经做了一些工作，但据我们所知，还没有人试图在不同方法之间形式上证明关系。因此，我们提出了对泛型编程库的形式比较。我们展示了如何在Agda中形式化不同的方法，包括一个共归表示，然后建立将这些方法彼此关联的定理。我们提供了一种包含一个方法在另一个方法中的构造性证明，可以用来在不同库之间进行转换，有助于减少代码重复。我们的形式化还有助于清楚地了解每种方法的潜力，特别是与不同的泛型视图及其表达能力相关的方面。
作者：Jos''e Pedro Magalh~aes, Andres L"oh
论文ID：1202.2920
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-02-15