.png)
3 days ago
7
The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.
Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone
The GMT offsets shown reflect the offsets at the moment of the conference.
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full programSpecify a time band
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 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.
