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.
