性能类型系统

Question

是否存在试图形式化程序性能特性的(静态)类型系统？我似乎找不到这样的企图。

由于类型系统是程序员库中对程序进行声明的最强大的工具之一，而且由于在许多情况下性能是至关重要的，因此似乎不难想象有人试图创建一个类型系统，该系统至少会对程序的存储和运行时特性做出一些声明。

Answer 1

您可以想象一个类型系统，其复杂程度足以与程序的WCET或复杂性相关。然后，问题是让声音类型分析器(或检查器)--即输入规则--使之成为可能，并有效地实现它，使之变得相当有用。

大多数类型系统非常简单，可以在实践中快速计算(至少对于人类开发人员可以手工编写的合理程序集是如此)。

一些学术编程语言(如AGDA)具有非常复杂的类型系统，它们是图灵全的，因此它们的编译器可能需要大量(也许是无限)的时间。

(如果我完全理解的话，Jérémie Salvucci在巴黎LIP6的PhD工作与你的问题有很大关系；我已经给他发了一封电子邮件；你可能会找区域和类型。)

但是，要注意赖斯定理 & 停止问题。类型系统可能并不总是您希望它们成为的灵丹妙药(请参阅旧的没有银弹书)。

Answer 2

似乎极有可能创建一个类型系统，对类型的性能特征进行分类(例如，“串行访问的快/慢”、“随机访问的快/慢”、“内存效率/效率低”)。这些特征可以是抽象的类型，以一种更具体的方式从它们继承到层次结构中。但是，使用这些类型的任何程序的性能将取决于它们的实际使用/访问方式。为了使类型系统对程序本身进行声明，这些类型的使用(访问)将自己表示为类型。这意味着放弃使用内置控制结构(例如for/while循环)，而使用实现它们的类型。因此，层次结构可以具有抽象的串行访问类型和子类列表-串行访问、树-串行访问类型等等。这样，使用效率至少可以部分地由这些类型的组合和相互应用来表示。

在像Haskell这样的函数式语言中--它几乎没有控制结构--在我看来，这是相当实用和可执行的。然而，在Java中，这样的系统似乎难以实现(与其说是从实现上，不如说是从结果的可执行性/可信赖性)。

Haskell已经允许我们明确地说明一个程序有多少是纯的，并提供了将特定活动限制在密封盒内的方法。由于Haskell中的并行/并发是实现通过类型系统的，因此可以认为它已经是实现(您想要的)方式的一部分。相比之下，命令式语言(甚至是静态类型化的语言，比如Java)为编码器提供了许多方法来颠覆这种尝试。