SHF: MEDIUM: Collaborative Research: The Theory and Practice of Dependent Types in Haskell

点击翻译按钮获取中文摘要

This project's overarching goal is to prevent bugs in software by extending the Haskell programming language to support dependent types. Haskell is used by researchers and programmers in industry to build a variety of software systems, such as financial analysis tools, interactive websites, data visualizations, and automated vehicle software. Dependent types are an up-and-coming technology that allows programmers to avoid bugs in their software, allowing them to include mathematical proofs of correctness in their code. These proofs are checked before the software ever runs, ruling out the possibility of failures, such as a crashed website. The intellectual merits are insights into the integration of advanced mathematical theories with an industrial-strength development tool (Haskell) and a deeper understanding of the mathematical principles that underlie the creation of correct software. The project's broader significance and importance are to give the technology industry access to dependent types for the first time, while creating opportunities for students (including those at one principal investigator's undergraduate women's college) to engage with this technology.The project includes both practical and foundational components. The Haskell type system, as implemented in the Glasgow Haskell Compiler (GHC) version 8.0, is able to simulate dependent types through the use of many language extensions. However, this use requires awkward encodings, and the extensions that support them complicate the language. In contrast, the Haskell type system envisioned by this project is based on a uniform approach to dependently typed programming that subsumes prior extensions. Part of this project involves replacing the core language of GHC with one based on dependent type theory, using relevance annotations to ensure that these extensions are backwards compatible. Furthermore, the project also introduces matchable functions, a qualifier that determines whether function applications can be analyzed via pattern matching, enabling the integration of dependent types with GHC's current type inference algorithm. Finally, this project includes an examination of the semantics of dependently typed programming languages with partiality.