Biblio

Meta-programs are programs that generate other programs, but in weakly type-safe systems, type-checking a meta-program only establishes its own type safety, and generated programs need additional type-checking after generation. Strong type safety of a meta-program implies type safety of any generated object program, a property with important engineering benefits. Current strongly type-safe systems suffer from expressivity limitations and cannot support many meta-programs found in practice, for example automatic generation of lenses. To overcome this, we move away from the idea of staged meta-programming. Instead, we use an off-the-shelf dependently-typed language as the meta-language and a relatively standard, intrinsically well-typed representation of the object language. We scale this approach to practical meta-programming, by choosing a high-level, explicitly typed intermediate representation as the object language, rather than a surface programming language. We implement our approach as a library for the Glasgow Haskell Compiler (GHC) and evaluate it on several meta-programs, including a deriveLenses meta-program taken from a real-world Haskell lens library. Our evaluation demonstrates expressivity beyond the state of the art and applicability to real settings, at little cost in terms of code size.

Indexed data types allow us to specify and verify many interesting invariants about finite data in a general purpose programming language. In this paper we investigate the dual idea: indexed codata types, which allow us to describe data-dependencies about infinite data structures. Unlike finite data which is defined by constructors, we define infinite data by observations. Dual to pattern matching on indexed data which may refine the type indices, we define copattern matching on indexed codata where type indices guard observations we can make. Our key technical contributions are three-fold: first, we extend Levy's call-by-push value language with support for indexed (co)data and deep (co)pattern matching; second, we provide a clean foundation for dependent (co)pattern matching using equality constraints; third, we describe a small-step semantics using a continuation-based abstract machine, define coverage for indexed (co)patterns, and prove type safety. This is an important step towards building a foundation where (co)data type definitions and dependent types can coexist.