License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.8.2.1
URN: urn:nbn:de:0030-drops-161991
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16199/
Go back to Dagstuhl Artifacts Series

Marshall, Daniel ; Orchard, Dominic

How to Take the Inverse of a Type (Artifact)

pdf-format:
DARTS-8-2-1.pdf (0.5 MB)

Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy.

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.

BibTeX - Entry

@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.dagstuhl.de/opus/volltexte/2022/16199},
  URN =		{urn:nbn:de:0030-drops-161991},
  doi =		{10.4230/DARTS.8.2.1},
  annote =	{Keywords: linear types, regular types, algebra of programming, derivatives}
}

Keywords: linear types, regular types, algebra of programming, derivatives
Collection: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Issue Date: 2022
Date of publication: 23.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI