CIF: Small: Rich Type Inference for Functional Programming

计算机软件的正确性常常依赖于它在执行过程中对特定于应用程序的不变量的遵守。这些不变量是复杂的，通常涉及系统许多不同部分之间的关系，并且是隐式的，通常从未在程序文本中正式表示。然而，违反这些不变量会导致大量错误和安全漏洞。因此，程序员使用静态类型系统来捕获这些不变量，并允许使用自动化工具来检查它们是否得到维护。用于类型推断的算法允许复杂类型保持隐式，从而简化了软件开发和维护，同时仍然可以随时用于文档和执行。虽然最近的类型系统扩展极大地丰富了静态类型语言的表达能力，但类型推断算法却没有跟上。本研究评估SMT（可满足模理论）解算器整合到工业强度函数式程式设计语言的类型推断演算法。特别是，它与微软剑桥研究院的研究人员合作，扩展了格拉斯哥Haskell编译器（GHC）的类型推断算法。GHC是一个成熟的、开源的Haskell编译器，由于其丰富的类型系统，它在工业界越来越受欢迎。该项目还包括以高级本科/硕士课程的形式进行教育和推广，并直接支持博士生。

The correctness of computer software often relies on its adherence to application-specific invariants during the course of its execution. These invariants are complex, often involving relationships between many different parts of the system, and implicit, often never formally expressed in the text of the program. Violating these invariants, however, leads to numerous bugs and security holes. As a result, programmers employ static type systems to capture these invariants and enable the use of automated tools to check that they are maintained. Algorithms for type inference allow complex types to remain implicit, easing software development and maintenance, while still readily available for documentation and enforcement. While recent type system extensions greatly enrich the expressiveness of statically typed languages, type inference algorithms have not kept pace. This research evaluates the integration of SMT (Satisfiability Modulo Theory) solvers into the type inference algorithm of an industrial-strength functional programming language. In particular, in collaboration with researchers at Microsoft Research Cambridge, it extends the type inference algorithm of the Glasgow Haskell Compiler (GHC). GHC is a mature, open source, Haskell Compiler that is gaining popularity in industry due to its rich type system. The project also includes education and outreach components in the form of an advanced undergraduate/masters level course and in the direct support of Ph.D. students.