[POPL'24] The Essence of Generalized Algebraic Data Types

The Essence of Generalized Algebraic Data Types (Video, POPL 2024)
Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, and Lars Birkedal
(Heriot-Watt University, UK; Aarhus University, Denmark; University of Cambridge, UK; Aarhus University, Denmark)

Abstract: This paper considers direct encodings of generalized algebraic data types (GADTs) in a minimal suitable lambda-calculus. To this end, we develop an extension of System Fω with recursive types and internalized type equalities with injective constant type constructors. We show how GADTs and associated pattern-matching constructs can be directly expressed in the calculus, thus showing that it may be treated as a highly idealized modern functional programming language. We prove that the internalized type equalities in conjunction with injectivity rules increase the expressive power of the calculus by establishing a non-macro-expressibility result in Fω, and prove the system type-sound via a syntactic argument. Finally, we build two relational models of our calculus: a simple, unary model that illustrates a novel, two-stage interpretation technique, necessary to account for the equational constraints; and a more sophisticated, binary model that relaxes the construction to allow, for the first time, formal reasoning about data-abstraction in a calculus equipped with GADTs.

Video Tags: Generalized Algebraic Data Types, Logical Relations, popl24main-p110-p, doi:10.1145/3632866, doi:10.5281/zenodo.10040534, orcid:0000-0001-5011-3458, orcid:0000-0002-7322-5644, orcid:0000-0002-0585-5564, orcid:0000-0003-1320-0098, Artifacts Available, Artifacts Evaluated — Reusable