2 Search Results for "Marshall, Daniel"

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}
}
  • Refine by Author
  • 2 Marshall, Daniel
  • 2 Orchard, Dominic

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

  • Refine by Keyword
  • 2 algebra of programming
  • 2 derivatives
  • 2 linear types
  • 2 regular types

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 2 2022

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