types - Scheme 编译器 Stalin 中的全局类型推断

Question

我正在研究 Scheme 编译器斯大林。它又大又复杂。另外，如果我理解正确的话，作者正计划写一系列详细介绍实现方面的论文，但从未有时间去做。

我感兴趣的斯大林方面是全局类型推断:根据它们在程序其他地方的使用情况推断事物的类型。斯大林真的这样做了吗？如果是，如何以及在其代码库中的位置？它是否使用了 Hindley-Milner 算法的变体/扩展？

Answer 1

来自 README :

Stalin does global static type analysis using a soft type system that supports recursive union types. Stalin can determine a narrow or even monomorphic type for each source code expression in arbitrary Scheme programs with no type declarations. This allows Stalin to reduce, or often eliminate, run-time type checking and dispatching. Stalin also does low-level representation selection on a per-expression basis. This allows the use of unboxed base machine data representations for all monomorphic types resulting in extremely high-performance numeric code.

来自 1997 talk by Siskind :

Stalin performs type inference using set-based analysis (SBA aka 0CFA). This analysis is augmented to support polyvariant procedure splitting. The results of SBA are used to reduce run-time type checking and dispatching. The results of SBA are also used to do low-level representation selection on a per-expression basis. This has two benefits. First, type tags can be eliminated for monotypes, allowing the use of base machine representations for primitive data. Second, boxing can be eliminated, alleviating the costs of indirection, allocation, and reclamation associated with boxing. Eliminating boxing requires that the run-time organization allow variables, parameters, structure slots, and vector slots to have different widths depending on the type of data that they hold. Furthermore, user-defined structures can be unboxed only if those structures are immutable. SBA is extended to determine data widths and mutability at compile time.

实际的类型推断算法似乎主要在源代码中实现
文件 source/stalin3b.sc .

SBA/0CFA 似乎是一个完全独立的算法
欣德利-米尔纳。但是，Hindley-Milner 也可用于实现软类型。

这是一个更好的 description of the 0CFAalgorithm .

相关论文有 Olin Shivers 1991 年的博士论文 Control-flow
分析高阶语言或驯服 Lambda 和 Flanagan &
Felleisen 1995 年的论文 Set-Based Analysis for Full Scheme 及其使用
在软打字。