Abstracts.2020.NbE.CBPV

From Normalization by Evaluation to Call-By-Push-Value

by Andreas Abel

Abstract

In this talk, we study normalization by evaluation (NbE) for the simply-typed lambda calculus (STLC) with weak coproducts, i.e. disjoint sum types without η-equality.

NbE aims to use a standard interpreter for STLC combined with a reification or read-back function from values to normal forms.

A function f is reified to a λ-abstraction λx. t, but how to obtain the body t? It is the reification of f(u) where the "unknown" value u is a reflection of the variable x. The value space thus needs to include unknowns that represent free variables and can be read back as such. A systematic solution is to interpret types not simply as sets of values but as presheaves, i.e. context-indexed sets monotone in the context. Monotonicity, i.e. going to larger contexts, makes room for so-far unused variables that cannot be confused with the existing variables.

One topic of the talk will be the distinction of types that need to be interpreted as presheaves and those that can simply be context-indexed sets, and a comonad □ that mediates between them. We will recognize that all presheaves are coalgebras for □.

Normalization of variants (disjoint sums) poses an additional problem: case distinctions will get stuck on "unknown" scrutinees. Thus, values will in general be case trees splitting on a couple of unknowns before giving a value in each case. Case trees form a monad ◇ and the interpreter will consequently be a monadic interpreter.

A second topic of the talk will be the identification of types that are algebras for the monad ◇. Reviewing the grammar for □-coalgebras and ◇-algebras we rediscover the polarization of the types of call-by-push-value (CBPV).

Finally, we look at different embeddings of the STLC into CBPV and how this gives us different flavors of NbE: standard call-by-name NbE, call-by-value NbE, and "optimal" NbE.

Material

1. Andreas Abel and Christian Sattler. 2019. Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda-Calculus. PPDP 2019 paper, TYPES 2019 talk.
2. Andreas Abel. 2019. Normalization by Evaluation for Call-By-Push-Value. Agda code.
3. Andreas Abel. 2021. From Normalization by Evaluation to Call-By-Push-Value. Video recording.