空间高效的显式契约

高阶契约检查的标准算法可能导致无界的空间消耗，并可能破坏尾递归，改变程序的渐近空间复杂度。虽然渐进类型——中介无类型与有类型代码的契约——的空间效率已得到充分研究，但显式契约——检查比简单类型更强性质的契约，例如“是自然数”而非“是整数”——的可靠空间效率仍是一个未解决的问题。我们展示了如何为带有强谓词契约的显式契约实现可靠的（sound）空间效率。关键技巧是将契约检查分解为强制（coercions）：结构化的、带有归咎标注的检查列表。通过仔细防止重复强制的出现，我们可以在保持相同可观察行为的同时恢复空间效率。在此过程中，我们定义了一个空间效率框架，用三种不同的空间高效显式演算遍历了设计空间。我们考察了契约语义的多种正确性准则；最终得出一种基于强制的语言，其契约享有（极大）有界的、可靠的空间消耗——它们在观察上等价于标准的、空间低效的语义。