Ur: Statically-Typed Metaprogramming with Type-Level Record Computation

Dependent types provide a strong foundation for specifying and verifying rich properties of programs through type-checking. The earliest implementations combined dependency, which allows types to mention program variables; with type-level computation, which facilitates expressive specifications that compute with recursive functions over types. While many recent applications of dependent types omit the latter facility, we argue in this paper that it deserves more attention, even when implemented without dependency. In particular, the ability to use functional programs as specifications enables statically-typed metaprogramming: programs write programs, and static type-checking guarantees that the generating process never produces invalid code. Since our focus is on generic validity properties rather than full correctness verification, it is possible to engineer type inference systems that are very effective in narrow domains. As a demonstration, we present Ur, a programming language des...

• Type: Conference
• Year: 2010
• Where: PLDI
• Authors: Adam Chlipala
• Keywords: Fancy Types, Keywords Dependent Types, PLDI 2010, Programming Languages, Static Type-checking Guarantees