Skip to main content

How to Take the Inverse of a Type

Marshall, Daniel, Orchard, Dominic A. (2022) How to Take the Inverse of a Type. In: Leibniz International Proceedings in Informatics. Proceedings of 36th European Conference on Object-Oriented Programming (ECOOP 2022). . Dagstuhl ISBN 978-3-95977-225-9. (doi:10.4230/LIPIcs.ECOOP.2022.5) (KAR id:98022)

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.

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.4230/LIPIcs.ECOOP.2022.5
Uncontrolled keywords: linear types, regular types, algebra of programming, derivatives
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: Engineering and Physical Sciences Research Council (https://ror.org/0439y7842)
Depositing User: Dominic Orchard
Date Deposited: 15 Nov 2022 15:40 UTC
Last Modified: 27 Feb 2024 11:13 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/98022 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.