TY - GEN
T1 - Restrictable Variants
T2 - 37th European Conference on Object-Oriented Programming, ECOOP 2023
AU - Madsen, Magnus
AU - Starup, Jonathan Lindegaard
AU - Lutze, Matthew
N1 - Publisher Copyright:
© Magnus Madsen, Jonathan Lindegaard Starup, and Matthew Lutze;
PY - 2023/7
Y1 - 2023/7
N2 - 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.
AB - 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.
KW - Boolean unification
KW - extensible variants
KW - refinement types
KW - restrictable variants
UR - http://www.scopus.com/inward/record.url?scp=85168864725&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.ECOOP.2023.17
DO - 10.4230/LIPIcs.ECOOP.2023.17
M3 - Article in proceedings
AN - SCOPUS:85168864725
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 17:1-17:27
BT - 37th European Conference on Object-Oriented Programming, ECOOP 2023
A2 - Ali, Karim
A2 - Salvaneschi, Guido
PB - Schloss Dagstuhl--Leibniz-Zentrum für Informatik
Y2 - 17 July 2023 through 21 July 2023
ER -