3 Search Results for "Orchard, Dominic"

Document
Artifact
DOI: 10.4230/DARTS.8.2.1
How to Take the Inverse of a Type (Artifact)

Authors: Daniel Marshall and Dominic Orchard

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
In functional programming, regular types are a subset of algebraic data types formed from products and sums with their respective units. One can view regular types as forming a commutative semiring but where the usual axioms are isomorphisms rather than equalities. In the pearl, we show that regular types in a linear setting permit a useful notion of multiplicative inverse, allowing us to ‘divide’ one type by another. We begin with an exploration of the properties and applications of this construction, and this artifact includes examples in Haskell demonstrating its relevance to various topics from the literature including program calculation, Laurent polynomials, and derivatives of data types. Some examples from the paper require a richer setting than Haskell can offer; the artifact replays the first set of examples in Granule, while also presenting additional examples demonstrating further algebraic structure through linear functions that incorporate local side effects.
Cite as

Daniel Marshall and Dominic Orchard. How to Take the Inverse of a Type (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 1:1-1:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{marshall_et_al:DARTS.8.2.1,
  author =	{Marshall, Daniel and Orchard, Dominic},
  title =	{{How to Take the Inverse of a Type (Artifact)}},
  pages =	{1:1--1:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Marshall, Daniel and Orchard, Dominic},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.1},
  URN =		{urn:nbn:de:0030-drops-161991},
  doi =		{10.4230/DARTS.8.2.1},
  annote =	{Keywords: linear types, regular types, algebra of programming, derivatives}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.5
How to Take the Inverse of a Type

Authors: Daniel Marshall and Dominic Orchard

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
In functional programming, regular types are a subset of algebraic data types formed from products and sums with their respective units. One can view regular types as forming a commutative semiring but where the usual axioms are isomorphisms rather than equalities. In this pearl, we show that regular types in a linear setting permit a useful notion of multiplicative inverse, allowing us to "divide" one type by another. Our adventure begins with an exploration of the properties and applications of this construction, visiting various topics from the literature including program calculation, Laurent polynomials, and derivatives of data types. Examples are given throughout using Haskell’s linear types extension to demonstrate the ideas. We then step through the looking glass to discover what might be possible in richer settings; the functional language Granule offers linear functions that incorporate local side effects, which allow us to demonstrate further algebraic structure. Lastly, we discuss whether dualities in linear logic might permit the related notion of an additive inverse.
Cite as

Daniel Marshall and Dominic Orchard. How to Take the Inverse of a Type. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 5:1-5:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{marshall_et_al:LIPIcs.ECOOP.2022.5,
  author =	{Marshall, Daniel and Orchard, Dominic},
  title =	{{How to Take the Inverse of a Type}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{5:1--5:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.5},
  URN =		{urn:nbn:de:0030-drops-162339},
  doi =		{10.4230/LIPIcs.ECOOP.2022.5},
  annote =	{Keywords: linear types, regular types, algebra of programming, derivatives}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.15
Data-Flow Analyses as Effects and Graded Monads

Authors: Andrej Ivašković, Alan Mycroft, and Dominic Orchard

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
In static analysis, two frameworks have been studied extensively: monotone data-flow analysis and type-and-effect systems. Whilst both are seen as general analysis frameworks, their relationship has remained unclear. Here we show that monotone data-flow analyses can be encoded as effect systems in a uniform way, via algebras of transfer functions. This helps to answer questions about the most appropriate structure for general effect algebras, especially with regards capturing control-flow precisely. Via the perspective of capturing data-flow analyses, we show the recent suggestion of using effect quantales is not general enough as it excludes non-distributive analyses e.g., constant propagation. By rephrasing the McCarthy transformation, we then model monotone data-flow effects via graded monads. This provides a model of data-flow analyses that can be used to reason about analysis correctness at the semantic level, and to embed data-flow analyses into type systems.
Cite as

Andrej Ivašković, Alan Mycroft, and Dominic Orchard. Data-Flow Analyses as Effects and Graded Monads. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ivaskovic_et_al:LIPIcs.FSCD.2020.15,
  author =	{Iva\v{s}kovi\'{c}, Andrej and Mycroft, Alan and Orchard, Dominic},
  title =	{{Data-Flow Analyses as Effects and Graded Monads}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{15:1--15:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.15},
  URN =		{urn:nbn:de:0030-drops-123376},
  doi =		{10.4230/LIPIcs.FSCD.2020.15},
  annote =	{Keywords: data-flow analysis, effect systems, graded monads, correctness}
}
  • Refine by Author
  • 3 Orchard, Dominic
  • 2 Marshall, Daniel
  • 1 Ivašković, Andrej
  • 1 Mycroft, Alan

  • Refine by Classification
  • 3 Theory of computation → Type theory

  • Refine by Keyword
  • 2 algebra of programming
  • 2 derivatives
  • 2 linear types
  • 2 regular types
  • 1 correctness
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2022
  • 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