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.