如何在Liquid Haskell中安全地使用可拓性
How to Safely Use Extensionality in Liquid Haskell
摘要：
精化类型检查器是对函数式程序进行推理的一种强有力的方法。例如，可以证明一个缓慢的规范实现的属性，将证明移植到行为相同的优化实现。如果没有函数的可拓性，证明必须与完全应用的函数相关。当数据本身具有高阶表示时，完全应用的证明面临严重的障碍！在处理一阶数据时，完全应用的证明在使用高阶函数时会导致令人讨厌的重复。虽然依赖类型论通常与函数扩展性公理一致，但具有语义子类型的精化类型系统不一致地处理函数扩展性的朴素措辞，导致不合理。我们证明了这种不合理性，并在Liquid Haskell中开发了一种新的平等方法：我们在一个名为PEq的库中定义了一个命题平等。使用PEq避免了不健全，同时仍然证明有用的等式在更高的类型，我们证明了它的使用在几个案例研究。我们通过建立一个小模型并开发其元理论来验证PEq。此外，我们使用一种未命名的民间传说技术证明了液体Haskell本身内部PEq的元属性，我们称之为“经典归纳”。
英文摘要：
Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation, porting the proofs to an optimized implementation that behaves the same. Without functional extensionality, proofs must relate functions that are fully applied. When data itself has a higher-order representation, fully applied proofs face serious impediments! When working with first-order data, fully applied proofs lead to noisome duplication when using higher-order functions. While dependent type theories are typically consistent with functional extensionality axioms, refinement type systems with semantic subtyping treat naive phrasings of functional extensionality inconsistently, leading to unsoundness. We demonstrate this unsoundness and develop a new approach to equality in Liquid Haskell: we define a propositional equality in a library we call PEq. Using PEq avoids the unsoundness while still proving useful equalities at higher types; we demonstrate its use in several case studies. We validate PEq by building a small model and developing its metatheory. Additionally, we prove metaproperties of PEq inside Liquid Haskell itself using an unnamed folklore technique, which we dub `classy induction'.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
