Compiling Gradual Types with Evidence

Efficiently supporting sound gradual typing in a language with structural types is challenging. To date, the Grift compiler is the only close-to-the-metal implementation of gradual typing in this setting, exploiting coercions for runtime checks, and further extended with monotonic references for efficient access to statically-typed data structures. On the language design and semantics side, the Abstracting Gradual Typing (AGT) methodology has proven fruitful to elucidate existing designs and to innovate by deriving gradualizations of a wide variety of typing disciplines and language features. Grounded in abstract interpretation, the Curry-Howard inspired runtime semantics of AGT is based on the notion of evidence for consistent judgments that evolve during reduction, monitoring the plausibility of well-typedness. While expressive and versatile, it is unclear whether such evidence-based semantics are a viable route to realize an efficient implementation of gradual typing. In this work, we explore this question by designing, implementing, and evaluating an evidence-based compiler, called GrEv. We explain how to bridge the gap between the formal semantics and the GrEv compiler implementation, and identify novel monotonic semantics. We empirically evaluate the performance of GrEv on the Grift benchmark suite. The results show that an evidence-based compiler can be competitive with, and even faster than, a coercion-based compiler, exhibiting more stability across configurations on the static-to-dynamic spectrum. In addition to enriching the space of gradual typing compilers, this work opens a direct door to exploring efficient implementations of the many advanced gradual typing disciplines formally derived with AGT in the literature.