How to Take the Inverse of a Type (Artifact)

Authors Daniel Marshall , Dominic Orchard



PDF
Thumbnail PDF

Artifact Description

DARTS.8.2.1.pdf
  • Filesize: 0.49 MB
  • 3 pages

Document Identifiers

Author Details

Daniel Marshall
  • School of Computing, University of Kent, Canterbury, UK
Dominic Orchard
  • School of Computing, University of Kent, Canterbury, UK
  • Department of Computer Science and Technology, University of Cambridge, UK

Cite AsGet BibTex

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)
https://doi.org/10.4230/DARTS.8.2.1

Artifact

Artifact 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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • linear types
  • regular types
  • algebra of programming
  • derivatives

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
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