5 Search Results for "Madsen, Magnus"

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-dev.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.18
Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism

Authors: Magnus Madsen and Jaco van de Pol

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

Abstract
We present purity reflection, a programming language feature that enables higher-order functions to inspect the purity of their function arguments and to vary their behavior based on this information. The upshot is that operations on data structures can selectively use lazy and/or parallel evaluation while ensuring that side effects are never lost or re-ordered. The technique builds on a recent Hindley-Milner style type and effect system based on Boolean unification which supports both effect polymorphism and complete type inference. We illustrate that avoiding the so-called 'poisoning problem' is crucial to support purity reflection. We propose several new data structures that use purity reflection to switch between eager and lazy, sequential and parallel evaluation. We propose a DelayList, which is maximally lazy but switches to eager evaluation for impure operations. We also propose a DelayMap which is maximally lazy in its values, but also exploits eager and parallel evaluation. We implement purity reflection as an extension of the Flix programming language. We present a new effect-aware form of monomorphization that eliminates purity reflection at compile-time. And finally, we evaluate the cost of this new monomorphization on compilation time and on code size, and determine that it is minimal.
Cite as

Magnus Madsen and Jaco van de Pol. Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 18:1-18:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{madsen_et_al:LIPIcs.ECOOP.2023.18,
  author =	{Madsen, Magnus and van de Pol, Jaco},
  title =	{{Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{18:1--18: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.18},
  URN =		{urn:nbn:de:0030-drops-182112},
  doi =		{10.4230/LIPIcs.ECOOP.2023.18},
  annote =	{Keywords: type and effect systems, purity reflection, lazy evaluation, parallel evaluation}
}
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-dev.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-dev.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}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.12
A Semantics for the Essence of React

Authors: Magnus Madsen, Ondřej Lhoták, and Frank Tip

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Traditionally, web applications have been written as HTML pages with embedded JavaScript code that implements dynamic and interactive features by manipulating the Document Object Model (DOM) through a low-level browser API. However, this unprincipled approach leads to code that is brittle, difficult to understand, non-modular, and does not facilitate incremental update of user-interfaces in response to state changes. React is a popular framework for constructing web applications that aims to overcome these problems. React applications are written in a declarative and object-oriented style, and consist of components that are organized in a tree structure. Each component has a set of properties representing input parameters, a state consisting of values that may vary over time, and a render method that declaratively specifies the subcomponents of the component. React’s concept of reconciliation determines the impact of state changes and updates the user-interface incrementally by selective mounting and unmounting of subcomponents. At designated points, the React framework invokes lifecycle hooks that enable programmers to perform actions outside the framework such as acquiring and releasing resources needed by a component. These mechanisms exhibit considerable complexity, but, to our knowledge, no formal specification of React’s semantics exists. This paper presents a small-step operational semantics that captures the essence of React, as a first step towards a long-term goal of developing automatic tools for program understanding, automatic testing, and bug finding for React web applications. To demonstrate that key operations such as mounting, unmounting, and reconciliation terminate, we define the notion of a well-behaved component and prove that well-behavedness is preserved by these operations.
Cite as

Magnus Madsen, Ondřej Lhoták, and Frank Tip. A Semantics for the Essence of React. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 12:1-12:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{madsen_et_al:LIPIcs.ECOOP.2020.12,
  author =	{Madsen, Magnus and Lhot\'{a}k, Ond\v{r}ej and Tip, Frank},
  title =	{{A Semantics for the Essence of React}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{12:1--12:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.12},
  URN =		{urn:nbn:de:0030-drops-131697},
  doi =		{10.4230/LIPIcs.ECOOP.2020.12},
  annote =	{Keywords: JavaScript, React, operational semantics, lifecycle, reconciliation}
}
  • Refine by Author
  • 5 Madsen, Magnus
  • 3 Starup, Jonathan Lindegaard
  • 2 Lhoták, Ondřej
  • 2 Lutze, Matthew
  • 1 Tip, Frank
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Program semantics
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Operational semantics

  • Refine by Keyword
  • 2 Boolean unification
  • 2 extensible variants
  • 2 refinement types
  • 2 restrictable variants
  • 1 Datalog
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 4 2023
  • 1 2020

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 Imprint Privacy Contact