如何在Liquid Haskell中安全使用Extensionality
摘要：依赖类型检查器是推理功能程序的一种强大方式。例如，可以证明慢速规范实现的属性，并将证明移植到行为相同的优化实现中。在没有功能外延性的情况下，证明必须涉及全应用的函数。当数据本身具有高阶表示时，全应用的证明面临严重的障碍！在处理一阶数据时，使用高阶函数时，全应用的证明会导致繁琐的重复。 虽然依赖类型理论通常与功能外延性公理一致，但具有语义子类型的精化类型系统不一致地处理功能外延性的愚蠢说法，导致不准确性。我们展示了这种不准确性，并在Liquid Haskell中开发了一种新的相等性方法：我们在一个称为PEq的库中定义了一个命题等式。使用PEq可以避免不准确性，同时在更高级别的类型中证明有用的等式；我们在几个案例研究中展示了它的用法。我们通过构建一个小模型并开发其元理论来验证PEq。此外，我们使用一个不具名的民间技术，在Liquid Haskell本身中证明了PEq的元属性，我们将其称为“优雅归纳”。
作者：Niki Vazou and Michael Greenberg
论文ID：2103.02177
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-07-20