Search Results

Documents authored by Starup, Jonathan Lindegaard

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.17
Restrictable Variants: A Simple and Practical Alternative to Extensible Variants

Authors: Magnus Madsen, Jonathan Lindegaard Starup, and Matthew Lutze

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

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

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)

Copy BibTex To Clipboard

@InProceedings{madsen_et_al:LIPIcs.ECOOP.2023.17,
  author =	{Madsen, Magnus and Starup, Jonathan Lindegaard and Lutze, Matthew},
  title =	{{Restrictable Variants: A Simple and Practical Alternative to Extensible Variants}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{17:1--17:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.17},
  URN =		{urn:nbn:de:0030-drops-182109},
  doi =		{10.4230/LIPIcs.ECOOP.2023.17},
  annote =	{Keywords: restrictable variants, extensible variants, refinement types, Boolean unification}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.31
Breaking the Negative Cycle: Exploring the Design Space of Stratification for First-Class Datalog Constraints

Authors: Jonathan Lindegaard Starup, Magnus Madsen, and Ondřej Lhoták

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
The λ_Dat calculus brings together the power of functional and declarative logic programming in one language. In λ_Dat, Datalog constraints are first-class values that can be constructed, passed around as arguments, returned, composed with other constraints, and solved. A significant part of the expressive power of Datalog comes from the use of negation. Stratified negation is a particularly simple and practical form of negation accessible to ordinary programmers. Stratification requires that Datalog programs must not use recursion through negation. For a Datalog program, this requirement is straightforward to check, but for a λ_Dat program, it is not so simple: A λ_Dat program constructs, composes, and solves Datalog programs at runtime. Hence stratification cannot readily be determined at compile-time. In this paper, we explore the design space of stratification for λ_Dat. We investigate strategies to ensure, at compile-time, that programs constructed at runtime are guaranteed to be stratified, and we argue that previous design choices in the Flix programming language have been suboptimal.
Cite as

Jonathan Lindegaard Starup, Magnus Madsen, and Ondřej Lhoták. Breaking the Negative Cycle: Exploring the Design Space of Stratification for First-Class Datalog Constraints. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 31:1-31:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{starup_et_al:LIPIcs.ECOOP.2023.31,
  author =	{Starup, Jonathan Lindegaard and Madsen, Magnus and Lhot\'{a}k, Ond\v{r}ej},
  title =	{{Breaking the Negative Cycle: Exploring the Design Space of Stratification for First-Class Datalog Constraints}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{31:1--31:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.31},
  URN =		{urn:nbn:de:0030-drops-182244},
  doi =		{10.4230/LIPIcs.ECOOP.2023.31},
  annote =	{Keywords: Datalog, first-class Datalog constraints, negation, stratified negation, type system, row polymorphism, the Flix programming language}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.12
Restrictable Variants: A Simple and Practical Alternative to Extensible Variants (Artifact)

Authors: Magnus Madsen, Jonathan Lindegaard Starup, and Matthew Lutze

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
In this artifact, we provide an implementation of the λ^res_var calculus, as described in the related article. The implementation is an extension of the Flix programming language compiler, supporting restrictable variants and the two partial pattern-matching constructs: choose and choose-⋆. The artifact consists of the extended Flix compiler, a Visual Studio Code extension supporting common IDE features such as syntax highlighting and type hovering, and a collection of Flix files demonstrating the use of restrictable variants. The Flix files correspond to examples presented in the paper. Users are invited to modify the Flix files in order to observe the influence of their changes on the inferred types in the provided programs.
Cite as

Magnus Madsen, Jonathan Lindegaard Starup, and Matthew Lutze. Restrictable Variants: A Simple and Practical Alternative to Extensible Variants (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 12:1-12:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{madsen_et_al:DARTS.9.2.12,
  author =	{Madsen, Magnus and Starup, Jonathan Lindegaard and Lutze, Matthew},
  title =	{{Restrictable Variants: A Simple and Practical Alternative to Extensible Variants (Artifact)}},
  pages =	{12:1--12:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Madsen, Magnus and Starup, Jonathan Lindegaard and Lutze, Matthew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.12},
  URN =		{urn:nbn:de:0030-drops-182521},
  doi =		{10.4230/DARTS.9.2.12},
  annote =	{Keywords: restrictable variants, extensible variants, refinement types, Boolean unification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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