多态可达性类型：在高阶泛型程序中追踪新鲜度、别名和分离
摘要：可达性类型是一个近期的提议，它在高阶但单态性设置中显示出了潜力，在受分离逻辑启发的基础上跟踪别名和分离。先前的lambda*可达性类型系统通过可达变量的集合来限定类型，并在两个术语具有不相交限定符时保证分离。然而，对于具有类型多态性和/或精确可达性多态性的朴素扩展是不完备的，使得lambda*不适用于实际语言的采用。结合精确、完备和参数化的可达性和类型多态性仍然是一个未解决的挑战。 本文对可达性追踪设计进行了重新思考，并提出了解决可达性多态性的关键挑战的解决方案。与原始设计中始终跟踪可达变量的传递闭包不同，我们只跟踪在单个步骤中可达的变量，并仅在必要时计算传递闭包，从而保留可以使用替换进行细化的已知变量上的可达性链。为了实现这个属性，我们引入了一个新的新鲜度限定符，它指示在评估步骤中可达性集合可能增长的变量。这些想法产生了简明类型的lambda钻石-演算，即无量词、轻量级的可达性多态性，以及具有类型和可达性限定符的有界参数化多态的F<:钻石-演算。我们在Coq中证明了类型的完备性和分离性质的保持。
作者：Guannan Wei, Oliver Brav{c}evac, Songlin Jia, Yuyan Bao, Tiark Rompf
论文ID：2307.13844
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-27