Published: 30th June 2022
DOI: 10.4204/EPTCS.360
ISSN: 2075-2180


Proceedings Ninth Workshop on
Mathematically Structured Functional Programming
Munich, Germany, 2nd April 2022

Edited by: Jeremy Gibbons and Max S. New

Jeremy Gibbons and Max S. New
Invited Talk: Going Without: A Linear Modality and its Role
Valeria de Paiva
Combinatory Adjoints and Differentiation
Martin Elsman, Fritz Henglein, Robin Kaarsgaard, Mikkel Kragh Mathiesen and Robert Schenck
LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes
Mathieu Montin, Amélie Ledein and Catherine Dubois
Tableless Calculation of Circular Functions on Dyadic Rationals
Peter Kourzanov
The Programming of Algebra
Fritz Henglein, Robin Kaarsgaard and Mikkel Kragh Mathiesen
Sikkel: Multimode Simple Type Theory as an Agda Library
Joris Ceulemans, Andreas Nuyts and Dominique Devriese
What Makes a Strong Monad?
Dylan McDermott and Tarmo Uustalu
On Structuring Functional Programs with Monoidal Profunctors
Alexandre Garcia de Oliveira, Mauro Jaskelioff and Ana Cristina Vieira de Melo


This volume contains the proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022), which took place on the 2nd of April as a satellite of European Joint Conferences on Theory & Practice of Software (ETAPS 2022).

The MSFP workshop highlights applications of mathematical structures to programming applications. We promote the use of category theory, type theory, and formal language semantics to the development of simple and reasonable programs. As the range of papers presented in this year's workshop shows, this continues to be a fruitful interface

We are honoured to host the following invited speaker:

We are grateful to our programme committee: We would also like to thank the ETAPS 2022 organizers and the EPTCS staff.

Jeremy Gibbons and Max S. New, April 2022

Going Without: A Linear Modality and its Role

Valeria de Paiva (Topos Institute, USA)

Linear type theories have been with us for more than 25 years, from the beginning of Linear Logic, and they still have much to teach us. I want to discuss and compare four linear type theories and show how an overlooked system has much potential to help with open issues in modal type theory. We discuss the Linear Lambda Calculus (Benton et al), Plotkin and Barber's DILL (Dual Intuitionistic Linear Logic) and Benton's Linear-non-Linear (LNL) type theories. Then we recall how DILL can be transformed into ILT (Intuitionistic and Linear Type Theory), as described by Maietti et al 2000, a type theory without a modality, but with two functions spaces, and what we gain with this transformation. Finally, we speculate on how this transformation might be helpful for other modal type theories, their models and envisaged applications.