The Essence of Generalized Algebraic Data Types

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

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.

Original languageEnglish
JournalProceedings of the ACM on Programming Languages
Volume8
IssuePOPL
Pages (from-to)695-723
Number of pages29
ISSN2475-1421
DOIs
Publication statusPublished - Jan 2024

Keywords

  • Generalized Algebraic Data Types
  • Logical Relations

Fingerprint

Dive into the research topics of 'The Essence of Generalized Algebraic Data Types'. Together they form a unique fingerprint.

Cite this