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 sequentially realizable linear functions allowing us to demonstrate further algebraic structure, and we discuss whether dualities in linear logic might permit the related notion of an additive inverse.
Fri 10 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30
|Type systemsExpert Discussion|
|How to Take the Inverse of a TypeECOOP 2022|
|Union and intersection contracts are hard, actuallyHub Talk|
Hub TalksLink to publication DOI
|Global Type Inference for Featherweight Generic JavaVCOOP 2022ECOOP 2022|