Restrictable Variants: A Simple and Practical Alternative to Extensible Variants

Magnus Madsen*, Jonathan Lindegaard Starup*, Matthew Lutze*

*Corresponding author for this work

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Abstract

We propose restrictable variants as a simple and practical alternative to extensible variants. Restrictable variants combine nominal and structural typing: a restrictable variant is an algebraic data type indexed by a type-level set formula that captures its set of active labels. We introduce new pattern-matching constructs that allows programmers to write functions that only match on a subset of variants, i.e., pattern-matches may be non-exhaustive. We then present a type system for restrictable variants which ensures that such non-exhaustive matches cannot get stuck at runtime. An essential feature of restrictable variants is that the type system can capture structure-preserving transformations: specifically the introduction and elimination of variants. This property is important for writing reusable functions, yet many row-based extensible variant systems lack it. In this paper, we present a calculus with restrictable variants, two partial pattern-matching constructs, and a type system that ensures progress and preservation. The type system extends Hindley-Milner with restrictable variants and supports type inference with an extension of Algorithm W with Boolean unification. We implement restrictable variants as an extension of the Flix programming language and conduct a few case studies to illustrate their practical usefulness.

Original languageEnglish
Title of host publication37th European Conference on Object-Oriented Programming, ECOOP 2023
EditorsKarim Ali, Guido Salvaneschi
PublisherSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Publication dateJul 2023
Pages17:1-17:27
Article number17
ISBN (Electronic)9783959772815
DOIs
Publication statusPublished - Jul 2023
Event37th European Conference on Object-Oriented Programming, ECOOP 2023 - Seattle, United States
Duration: 17 Jul 202321 Jul 2023

Conference

Conference37th European Conference on Object-Oriented Programming, ECOOP 2023
Country/TerritoryUnited States
CitySeattle
Period17/07/202321/07/2023
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume263
ISSN1868-8969

Keywords

  • Boolean unification
  • extensible variants
  • refinement types
  • restrictable variants

Fingerprint

Dive into the research topics of 'Restrictable Variants: A Simple and Practical Alternative to Extensible Variants'. Together they form a unique fingerprint.

Cite this