< Back to previous page

Project

Implicit Type-Directed Code Generation

Many mainstream programming languages feature a static type system because it is such a light-weight and cost-effective way at identifying large classes of programmer mistakes at an early stage. This saves on damages caused by bugs and on programmer time to root them out. Less known is that static type systems can save developer time in a second way, by implicitly generating part of the program based on available type information. The most prominent such features are Haskell's type classes and Scala's implicit parameters, which are ubiquitous in Haskell/Scala programs and contribute much to their conciseness. Yet, there is still much untapped potential regarding expressiveness and robustness, which we aim to develop in this project to extend the usefulness and appeal of these features. Expressiveness comprises more flexible user control and more automatic reasoning power, while robustness means establishing (currently lacking) rock-solid mechanized proofs of key type system properties, like coherence, and correctness of inference.
Date:1 Oct 2020 →  Today
Keywords:programming languages, type systems, implicits, resolution, code generation
Disciplines:Language design, constructs and features, Programming languages and technologies