Functionality from Structure
The tenth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control.
MSFP 2024 will be held on Monday 8th July 2024 in affiliation with ICALP/LICS/FSCD 2024 in Tallinn, Estonia.
The proceedings will be published in EPTCS, as in recent years.
Nathan Corbyn, University of Oxford, UK, Understanding the Classical Monad-Theory Correspondence
The original discovery of the correspondence between monads and theories dates back to the 1960s and has been generalised many times over. Arkor's 2022 thesis provides a clean and conceptual understanding of general monad-theory correspondences in terms of relative monads. While not necessary for the proofs of the simpler cases, I find this theoretical framework elucidating, particularly when viewed through the lens of promonads. In this talk, I'll walk through the concepts of Lawvere theory, promonad, relative monad and finitary monad, hoping to arrive at an intuitive explanation of the classical correspondence.
Exequiel Rivas, Procontainers for Idioms, Arrows and Monads
Containers, or polynomial functors, are a popular class of functors that is closed under a variety of operations, including coproducts, products, Day convolution and composition. Idioms and monads, two extremely successful interfaces for capturing computational effects in functional languages, are based on these last two operations between functors. However, a third popular interface of computational effects is missing from the picture: arrows, which are usually understood in terms of profunctors instead of functors. In this article we introduce a notion of procontainer, which is a class of profunctors closed also under operations of interest. We demonstrate how this notion allows to express the well-known connections between these three different interfaces for computational effects, when restricted to containers.
Danel Ahman and Gašper Žajdela, A Stateful Time-Aware Operational Semantics for Temporal Resources
By temporal resources we understand resources in programming whose usage is time-sensitive or -critical, and which, while perhaps already physically available to a program, can be used or acted upon only after a certain amount of time passes or some prescribed events take place. Such temporal aspects of resources can be naturally modularly captured with a combination of graded modal types and a graded-monadic effect system. In this paper, we develop this line of work further, by accompanying this modal approach with a stateful time-aware operational semantics, which in addition to explaining how programs behave computationally, can be used to analyse the time cost of such programs and which temporal resources they operate with. In addition to basic type-safety, we prove our semantics sound with respect to a temporal variant of the equational presentation of local state.
Alexandre Garcia de Oliveira, Folds, Scans, and Moore Machines as Monoidal Profunctor Homomorphisms
This work focuses on utilizing monoidal profunctor homomorphisms to establish connections between folds, scans, and Moore machines, employing monoidal profunctor homomorphisms as a fundamental tool for theoretical reasoning. Despite the recognized versatility of monoidal profunctors in other areas of functional programming, their application in linking these specific computational models has not been extensively explored. Folds and scans are analyzed as instances of a specific monoidal profunctor known as SISO (Structured Input-Structured Output). It is demonstrated that a Moore machine can also be effectively described as a lawful monoidal profunctor. This work establishes a clear connection by proving that there are structure-preserving maps from the SISO monoidal profunctor, representing folds and scans, to the Moore monoidal profunctor, therefore characterizing this relationship as a homomorphism. This exploration not only enhances the structuring of lawful and comprehensible programs but also fills a significant gap by establishing the utility of monoidal profunctors in a new context. This work asserts that the methodologies developed here can be applied to understand other complex computational processes and their laws.
Zachary Flores, Angelo Taranto, Yakir Forman and Eric Bond, Formalizing Operads for a Categorical Framework of DSL Composition (talk only)
How do you build strong type safety into a programming language? One answer to this problem is to provide a formalization for, if it exists, the denotational semantics of the programming language. Achieving such a formalization provides a high standard for ensuring the programming language is correct-by-construction. In our paper, we discuss steps toward building the foundation for the denotational semantics of a meta-language for composition of high-level abstractions of domain-specific languages using operads. The category of operads has properties that allow for the smooth composition of objects, allowing us to easily build larger structures from basic pieces. In particular, these properties provide an excellent ground to model our meta-language and its need to compose high-level abstractions of domain-specific languages. To take the first step towards this formalization, we formalize operads, as they are the basic pieces future work relies on. Throughout this paper, we discuss our formalization of the definition of an operad in the proof assistant Coq and an important instantiation of our definition in Coq which provides a concrete formalization of an example of an operad. As such, this work in Coq provides a formal mathematical basis for our meta-language development. Our work also provides, to our knowledge, the first known formalization of operads within a proof assistant that has significant automation, as well as a model of operads that does not rely on Homotopy Type Theory.
Chad Nester and Niels Voorneveld, Protocol Choice and Iteration for the Free Cornering (talk only)
Morphisms of monoidal categories often admit interpretation as processes, which produce and consume resources according to their type. The free cornering of a monoidal category augments it with corner cells, resulting in a double category. Processes become interacting processes, with the interaction governed by a simple system of protocol types. Alas, the system of protocol types that arises in this way is too simple to form the basis of a serious programming language: it lacks both protocol choice and the ability to iterate protocols. In recent work we extend the free cornering to support protocol choice and iteration. This requires more of the base category, which must now be a distributive monoidal category. We sketch the construction here. The resulting double category has a number of encouraging properties. For example, It admits the structure of a monoidal double category. The cells supporting protocol choice give products/coproducts in its category of horizontal cells, and the two iteration operations define a monad/comonad on the horizontal cells. Iteration admits a sensible coinductive reasoning principle.
Zev Shirazi, Commutative Codensity Monads and Probability Bimeasures (talk only)
Several well-studied probability monads have been expressed as codensity monads over small categories of stochastic maps, giving a limit description of spaces of probability measures. In this paper we show how properties of probability monads such as commutativity and affineness can arise from their codensity presentation. First we show that their codensity presentation is closely related to another characterisation of probability monads as terminal endofunctors admitting certain maps into the Giry monad, which allows us to generalise a result by Van Breugel on the Kantorovich monad. We then provide sufficient conditions for a codensity monad to lift to MonCat, and give a characterisation of exactly pointwise monoidal codensity monads; codensity monads that satisfy a strengthening of these conditions. We show that the Radon monad is exactly pointwise monoidal, and hence give a description of the tensor product of free algebras of the Radon monad in terms of Day convolution. Finally we show that the Giry monad is not exactly pointwise monoidal due to the existence of probability bimeasures that do not extend to measures, although its restriction to standard Borel spaces is. We introduce the notion of a *-monad and its Kleisli monoidal op-multicategory to describe the categorical structure that organises the spaces of probability polymeasures on measurable spaces.
Exequiel Rivas and Tarmo Uustalu, Concurrent Monads for Shared State (talk only)
In the context of programming with effects, sequential composition takes a special role as the primary control structure for combining computations. In this article, we advocate the idea that parallel composition should also be treated as a control structure, on the same footing as sequential composition. We promote the concept of concurrent monad, which axiomatizes both sequential and parallel composition, and illustrate the approach by describing two concurrent monads for shared state: one of resumptions, the other of finite multisets of traces.
Register for participation via the ICALP registration page. The early registration deadline was 17th May 2024.
We are pleased to announce that online participation is free for MSFP 2024: we will stream the talks over Zoom, and do our best to handle questions from online participants. To participate, please complete the online participation registration form by Saturday 6th July. On the Sunday evening before the workshop, we will email Zoom details to everyone who registered.
The workshop programme starts at 10:30, allowing participants to attend the LICS invited talk by Alexandra Silva. The last five (5) minutes of each slot are for questions.
Session 1: 10:30-12:30
10:30
Exequiel Rivas,
Procontainers for Idioms, Arrows and Monads
(slides, video)
11:10
Danel Ahman and Gašper Žajdela,
A Stateful Time-Aware Operational Semantics for Temporal Resources
(slides, video)
11:50
Alexandre Garcia de Oliveira,
Folds, Scans, and Moore Machines as Monoidal Profunctor Homomorphisms
(slides, video)
Session 2: 14:00-15:30
14:00
Zachary Flores, Angelo Taranto, Yakir Forman and Eric Bond,
Formalizing Operads for a Categorical Framework of DSL Composition
(video)
14:30
Chad Nester and Niels Voorneveld,
Protocol Choice and Iteration for the Free Cornering
(slides, video)
15:00
Zev Shirazi,
Commutative Codensity Monads and Probability Bimeasures
(slides, video)
Session 3: 16:00-17:30
16:00
Exequiel Rivas and Tarmo Uustalu,
Concurrent Monads for Shared State
(slides, video)
16:30
Nathan Corbyn, Keynote:
Understanding the Classical Monad-Theory Correspondence
(slides, video)
Submissions are welcomed on, but not restricted to, topics such as:
Please contact the programme chairs Favonia and Jeremy Gibbons if you have any questions about the scope of the workshop.
We accept two categories of submission:
A short abstract should be submitted by four days in advance of the paper deadline (for both full paper and extended abstract submissions). References and appendices are not included in page limits, but reviewers may or may not read appendices. Accepted papers and talks must be presented at the workshop by at least one of the authors.
We are using EasyChair to manage submissions.
The ninth MSFP Workshop was held online and in person on 2nd April 2022, in association with ETAPS in Munich, Germany. It was organised by Max New and Jeremy Gibbons, and featured an invited talk by Valeria de Paiva. The proceedings were published by EPTCS available here.
The eighth MSFP Workshop was held online in August 2020, originally planned as part of ETAPS. It was organised by Sam Lindley and Max New, and featured invited talks by Pierre-Marie Pedrot and Satnam Singh. The proceedings were published by EPTCS available here.
The seventh MSFP Workshop was held in July 2018, in Oxford, UK, as part of FLoC. It was organised by Robert Atkey and Sam Lindley, and featured invited talks by Tamara von Glehn and Didier Rémy. The proceedings were published by EPTCS available here.
The sixth MSFP Workshop was held in April 2016, in Eindhoven, Netherlands, just after ETAPS 2016. It was organised by Neelakantan Krishnaswami and Robert Atkey, and featured an invited talk by Fredrik Nordvall Forsberg. The proceedings wer published by EPTCS available here.
The fifth MSFP Workshop was held in April 2014, in Grenoble, France, just after ETAPS 2014. It was organised by Paul Levy and Neelakantan Krishnaswami, and featured invited talks from Robert Atkey and Shin-ya Katsumata. The proceedings were published by EPTCS, available here.
The fourth MSFP Workshop was held in March 2012, in Tallinn, Estonia, before ETAPS 2012. It was organised by James Chapman and Paul Levy, and featured invited talks from Danko Ilik and Neil Ghani. The proceedings were published by EPTCS, available here.
The third MSFP Workshop was held in September 2010, in Baltimore, Maryland, before ICFP 2010. It was organised by Venanzio Capretta and James Chapman, and featured invited talks from Martín Escardó and Amy Felty. The proceedings were published by ACM Press, available here.
The second MSFP Workshop was held in July 2008, at Reykjavik University, Iceland as part of ICALP 2008. It was organised by Conor McBride and Venanzio Capretta, and featured invited talks from Andrej Bauer and Dan Piponi. The proceedings were published in Electronic Notes in Theoretical Computer Science, v. 229, n. 5, available here.
The inaugural MSFP Workshop was held in July 2006, in Kuressaare, Estonia, a fine curtain-raiser for MPC and AMAST. It was organised by Tarmo Uustalu and Conor McBride, and featured invited talks from John Power and Andrzej Filinski. The proceedings were published in the British Computer Society's "Electronic Workshops in Computing" Series, available here.
Revised selected papers (with a full re-refereeing process) appeared as a special issue of the Journal of Functional Programming Volume 19 Issue 3-4.