DROPS

Document

Artifact

How to Take the Inverse of a Type (Artifact)

Authors: Danielle 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

Danielle 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, Danielle 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, Danielle and Orchard, Dominic},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.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: Danielle 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

Danielle 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, Danielle 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.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}
}

Search Results

Documents authored by Marshall, Danielle

How to Take the Inverse of a Type (Artifact)

Abstract

Cite as

How to Take the Inverse of a Type

Abstract

Cite as

Thanks for your feedback!

Could not send message