Document Open Access Logo

Restrictable Variants: A Simple and Practical Alternative to Extensible Variants

Authors Magnus Madsen , Jonathan Lindegaard Starup , Matthew Lutze

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2023.17.pdf
  • Filesize: 1.06 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • restrictable variants
  • extensible variants
  • refinement types
  • Boolean unification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Magnus Madsen, Jonathan Lindegaard Starup, and Matthew Lutze. Restrictable Variants: A Simple and Practical Alternative to Extensible Variants. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 17:1-17:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ECOOP.2023.17

Author Details

Magnus Madsen
  • Department of Computer Science, Aarhus University, Denmark
Jonathan Lindegaard Starup
  • Department of Computer Science, Aarhus University, Denmark
Matthew Lutze
  • Department of Computer Science, Aarhus University, Denmark

Supplementary Materials

References

  1. Sheldon B. Akers. Binary decision diagrams. IEEE Transactions on computers, C-27(06), 1978. URL: https://doi.org/10.1109/TC.1978.1675141.
  2. Franz Baader. On the complexity of Boolean unification. Information Processing Letters, 67(4), 1998. URL: https://doi.org/10.1016/S0020-0190(98)00106-9.
  3. Gilles Barthe and Maria João Frade. Constructor subtyping. In Programming Languages and Systems: 8th European Symposium on Programming (ESOP), 1999. URL: https://doi.org/10.1007/3-540-49099-X_8.
  4. George Boole. The mathematical analysis of logic. Macmillan, Barclay and Macmillan, 1847. Google Scholar
  5. Alexandre Boudet, Jean-Pierre Jouannaud, and Manfred Schmidt-Schauss. Unification in Boolean rings and abelian groups. Journal of Symbolic Computation, 8(5), 1989. URL: https://doi.org/10.1016/S0747-7171(89)80054-9.
  6. Luís Caires and Bernardo Toninho. Refinement kinds: Type-safe programming with practical type-level computation. Proc. of the ACM on Programming Languages, 3(OOPSLA), 2019. URL: https://doi.org/10.1145/3360557.
  7. Giuseppe Castagna, Mickaël Laurent, Kim Nguyen, and Matthew Lutze. On type-cases, union elimination, and occurrence typing. Proc. of the ACM on Programming Languages, 6(POPL), 2022. URL: https://doi.org/10.1145/3462306.
  8. Luis Damas. Type assignment in programming languages. PhD thesis, The University of Edinburgh, 1984. Google Scholar
  9. Edsko de Vries, Rinus Plasmeijer, and David M Abrahamson. Uniqueness typing simplified. In Implementation and Application of Functional Languages: 19th International Workshop (IFL), 2008. URL: https://doi.org/10.1007/978-3-540-85373-2_12.
  10. Tim Freeman and Frank Pfenning. Refinement types for ML. In Proc. of the ACM SIGPLAN 1991 conference on Programming language design and implementation (PLDI), 1991. URL: https://doi.org/10.1145/113445.113468.
  11. Benedict R Gaster and Mark P Jones. A polymorphic type system for extensible records and variants. Technical report, University of Nottingham, 1996. Google Scholar
  12. Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In Proc. of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), 1991. URL: https://doi.org/10.1145/99583.99603.
  13. Mark P Jones. A theory of qualified types. Science of Computer Programming, 22(3), 1994. URL: https://doi.org/10.1016/0167-6423(94)00005-0.
  14. Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: type inference for generalised algebraic data types. Technical report, University of Pennsylvania, 2004. Google Scholar
  15. Andrew Kennedy and Claudio V. Russo. Generalized algebraic data types and object-oriented programming. In Proc. of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2005. URL: https://doi.org/10.1145/1094811.1094814.
  16. Daan Leijen. Extensible records with scoped labels. In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming (TFP), 2005. Google Scholar
  17. Daan Leijen. Koka: Programming with row polymorphic effect types. In Proc. 5th Workshop on Mathematically Structured Functional Programming (MSFP), 2014. URL: https://doi.org/10.4204/EPTCS.153.8.
  18. Daan Leijen. Type directed compilation of row-typed algebraic effects. In Proc. of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017. URL: https://doi.org/10.1145/3009837.3009872.
  19. Sam Lindley and James Cheney. Row-based effect types for database integration. In Proc. of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), 2012. URL: https://doi.org/10.1145/2103786.2103798.
  20. Leopold Löwenheim. Über das auflösungsproblem im logischen klassenkalkul. In Sitzungsberichte der Berliner Mathematischen Gesellschaft 7, 1908. Google Scholar
  21. Magnus Madsen. The principles of the Flix programming language. In Proc. of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), 2022. URL: https://doi.org/10.1145/3563835.3567661.
  22. Magnus Madsen and Ondřej Lhoták. Fixpoints for the masses: programming with first-class Datalog constraints. Proc. of the ACM on Programming Languages, 4(OOPSLA), 2020. URL: https://doi.org/10.1145/3428193.
  23. Magnus Madsen, Jonathan Lindegaard Starup, and Ondřej Lhoták. Flix: A meta programming language for Datalog. In Proc. of the 4th International Workshop on the Resurgence of Datalog in Academia and Industry (Datalog 2.0), 2022. Google Scholar
  24. Magnus Madsen and Jaco van de Pol. Polymorphic types and effects with Boolean unification. Proc. of the ACM on Programming Languages, 4(OOPSLA), 2020. URL: https://doi.org/10.1145/3428222.
  25. Magnus Madsen and Jaco van de Pol. Relational nullable types with Boolean unification. Proc. of the ACM on Programming Languages, 5(OOPSLA), 2021. URL: https://doi.org/10.1145/3485487.
  26. Andrew Marmaduke, Christopher Jenkins, and Aaron Stump. Zero-cost constructor subtyping. In Proc. of the 32nd Symposium on Implementation and Application of Functional Languages (IFL), 2020. URL: https://doi.org/10.1145/3462172.3462194.
  27. Urusula Martin and Tobias Nipkow. Boolean unification - the story so far. Journal of Symbolic Computation, 7(3), 1989. URL: https://doi.org/10.1016/S0747-7171(89)80013-6.
  28. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3), 1978. URL: https://doi.org/10.1016/0022-0000(78)90014-4.
  29. Shin-ichi Minato. Zero-suppressed BDDs for set manipulation in combinatorial problems. In Proc. of the 30th Design Automation Conference (DAC), 1993. URL: https://doi.org/10.1145/157485.164890.
  30. J Garrett Morris and James McKinna. Abstracting extensible data types: or, rows by any other name. Proc. of the ACM on Programming Languages, 3(POPL), 2019. URL: https://doi.org/10.1145/3290325.
  31. François Pessaux and Xavier Leroy. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems (TOPLAS), 22(2), 2000. URL: https://doi.org/10.1145/349214.349230.
  32. François Pottier and Yann Régis-Gianas. Stratified type inference for generalized algebraic data types. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2006. URL: https://doi.org/10.1145/1111037.1111058.
  33. Didier Rémy. Type inference for records in a natural extension of ML. Technical report, University of Pennsylvania, 1990. Google Scholar
  34. Alan JA Robinson and Andrei Voronkov. Handbook of automated reasoning, volume 1. Elsevier and MIT Press, 2001. Google Scholar
  35. Vincent Simonet and François Pottier. A constraint-based approach to guarded algebraic data types. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(1), 2007. URL: https://doi.org/10.1145/1180475.1180476.
  36. Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. Refinement types for Haskell. In Proc. of the 19th ACM SIGPLAN international conference on Functional programming (ICFP), 2014. URL: https://doi.org/10.1145/2628136.2628161.
  37. Mitchell Wand. Type inference for simple objects. In Proc. of the Fourth Annual Symposium on Logic in Computer Science, 1987. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact