András Kovács
Eötvös Loránd University
Fast elaboration for dependent type theories
Elaboration is the process which takes raw source syntax as input (in our case, dependently typed syntax), and returns explicit core terms, where all implicit surface-level features are resolved. It commonly includes type checking, unification, desugaring, and resolution of class instances and coercions. In Agda and Coq, elaboration performance is a commonly desired feature. In this talk, I focus on two core tasks in elaboration: conversion checking and generation of metavariable solutions. I argue that poor metavariable solutions are a frequent cause of asymptotic blowups in Agda and Coq. I present an environment machine which supports fast call-by-need conversion checking, and also allows us to readback core terms for relatively high-quality metavariable solutions. I argue that carefully chosen semantic values (here: values of certain abstract machines) should be viewed as the "core" representation, instead of conventional syntactic core terms. Syntactic core terms should be viewed as black-box machine code, supporting fast evaluation into semantic values, but not supporting much else. This system would be more complex than a minimal Coq-style core, but would yield significant speedups and simplifications when considering the whole elaboration pipeline.
