WG211/M23Kovács

Polarized lambda calculus at runtime, dependent type theory at compile time (András Kovács)

I present a particular two-level theory where the object-level is a simply-typed polarized lambda calculus with computation types (functions, computational products) and value types (ADTs, closures), and the meta-level is a standard dependent type theory. This appears to be an excellent setting for a wide range of staged programming. The polarization gives us precise control over closures and call arities, in a lightweight way. The computational products can be used to generate well-typed mutual blocks with no overhead in downstream compilation. I develop two applications. First a staged monad transformer library. Second, a staged stream library, where we have very concise definitions for zipping and concatMap with guaranteed fusion, and streams are also parameterized over monads, so that state transitions can produce monadic effects. For concatMap, I essentially rely on a generativity axiom, which internally states that certain metaprograms cannot analyze object terms. This is somewhat similar to internal parametricity statements in type theories. There are two implementation for these developments, one in typed Template Haskell, with some compromises due to the lack of polarization and dependent types, and one in Agda.