Functionality from Structure
The ninth 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 2022 will be held on Saturday 2nd April 2022 in affiliation with ETAPS 2022 in Munich, Germany.
The proceedings have now been published as EPTCS Volume 360.
Valeria de Paiva, Topos Institute, USA, Going Without: A Linear Modality and its Role
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.
LIBNDT: Towards a formal library on spreadable properties over linked nested datatypes (Mathieu Montin, Amélie Ledein and Catherine Dubois)
Nested datatypes have been widely studied in the past 50 years, both theoretically using category theory, and practically in programming languages such as Haskell. They consist in recursive polymorphic datatypes where the type parameter changes throughout the recursion, and have a variety of applications such as modelling memory or modelling constraints over regular datatypes without relying on dependent types. In this work, we focus on a specific subset of nested datatypes which we call Linked Nested DataTypes (LNDT). We show that some usual datatypes such has List and Maybe, as well as some well-known nested datatypes such as Nest and even Bush can be built as various instances of LNDT. We proceed by presenting LIBNDT, a library, developed both in Agda and Coq, which focuses on the set of constructs that can be propagated directly from the parameter on which a LNDT is built, to the LNDT itself. These constructs are of two kinds, functions, such as folds and map, and properties, such as the congruence of map or the satisfaction of a given predicate for at least one, or all, elements of the structure. We make use of the dependent type system of both Coq and Agda to model the latter. We end by discussing several interesting topics that were raised throughout our development such as termination, comparison of our tools and the proof effort required to extend LIBNDT with additional elements.
Data Types with Negation (talk only) (Robert Atkey) (extended abstract)
Inductive data types are a foundational tool for representing data and knowledge in dependently typed programming languages. The user provides a collection of rules that determine positive evidence for membership in the type. Elimination of an inductive type corresponds to structural induction on its members. But what if our data modelling requires negative information as well as positive? For example, representing the result of a backtracking parser requires evidence that a certain parsing attempt *didn't* work. Standard formulations of inductive types do not allow negative information mixed with positive. Mixing positive and negative information has been studied in logic programming, resulting in concepts like Negation as Failure, stable model semantics, and well-founded semantics. Incorporating negative information into systems of rules leads us into the realm of non-monotonic logics, where simply adding knowledge does not necessarily preserve existing conclusions. We describe a way to understand data types with negative information in type theory by combining ideas from 3-valued stable models in logic programming and constructive negation (or refutation) from linear logic.
Sikkel: Multimode Simple Type Theory as an Agda Library (Joris Ceulemans, Andreas Nuyts and Dominique Devriese)
Many variants of type theory extend a basic theory with additional primitives or properties like univalence, guarded recursion or parametricity, to enable constructions or proofs that would be harder or impossible to do in the original theory. However, implementing such extended type theories (either from scratch or by modifying an existing implementation) is a big hurdle for their wider adoption. In this paper we present Sikkel, a library in the dependently typed programming language Agda that allows users to program in extended type theories. It uses a deeply embedded language that can be easily extended with additional type and term constructors, thus supporting a wide variety of type theories. Moreover, Sikkel has a type checker that is sound by construction in the sense that all well-typed programs are automatically translated to their semantics in a shallow embedding based on presheaf models. Additionally, our model supports combining different base categories by using modalities to transport definitions between them. This enables in particular a general approach for extracting definitions to the meta-level, so that we can use the extended type theories to define regular Agda functions and prove properties of them. In this paper, we demonstrate Sikkel theories with guarded recursion and parametricity, but other extensions can be easily plugged in. For now, Sikkel supports only simple type theories but its model already anticipates the future addition of dependent types and a universe.
What makes a strong monad (Dylan McDermott and Tarmo Uustalu)
Strong monads are important for several applications, in particular, in the denotational semantics of effectful languages, where strength is needed to sequence computations that have free variables. Strength is non-trivial: it can be difficult to determine whether a monad has any strength at all, and monads can be strong in multiple ways. We therefore review some of the most important known facts about strength and prove some new ones. In particular, we present a number of equivalent characterizations of strong functor and strong monad, and give some conditions that guarantee existence or uniqueness of strengths. We look at strength from three different perspectives: actions of a monoidal category V, enrichment over V, and powering over V. We are primarily motivated by semantics of effects, but the results are also useful in other contexts.
Tableless calculation of circular functions on dyadic rationals (Petr Kourzanov)
I would like to tell a story. A story about a beautiful mathematical relationship that elucidates the computational view on the classic subject of trigonometry. All stories need a language, and for this particular story an algorithmic language ought to do well. What makes a language algorithmic? From our perspective as the functional programming community, it should support expression of the computation rather than impose its own limitations on the algorithm. We develop a new algorithm for the computation of trigonometric functions on dyadic rationals, together with the language used to express it, in Scheme. We provide a mechanically-derived algorithm for the computation of the inverses of our target functions. We address efficiency and accuracy concerns that pertain to the implementation of the proposed algorithm either in hardware or software.
On Structuring Functional Programs with Monoidal Profunctors (Alexandre Garcia de Oliveira, Mauro Jaskelioff and Ana Cristina Vieira de Melo)
We study monoidal profunctors as a tool to reason and structure pure functional programs both from a categorical perspective and as a Haskell implementation. From the categorical point of view we approach them as monoids in a certain monoidal category of profunctors. We study properties of this monoidal category and construct and implement the free monoidal profunctor. We study the relationship of monoidal construction to optics, and introduce a promising generalization of the implementation which we illustrate by introducing effectful monoidal profunctors.
Combinatory adjoints and differentiation (Martin Elsman, Fritz Henglein, Robin Kaarsgaard, Mikkel Kragh Mathiesen and Robert Schenck)
Automatic differentiation is the discipline of computing derivatives for functions specified by programs. It has numerous applications in machine learning, computational science, quantitative finance and more. Traditionally it is formulated based on calculus, using a dual number interpretation for scalar values. In this paper we develop a compositional approach for automatic and symbolic differentation based on and motivated by categorical constructions on structured (particularly Hilbert) vector spaces in functional analysis, where derivatives are linear maps on abstract vectors rather than being limited to scalars or tensors (vectors, matrices, higher-rank tensors) of scalar values. We show that automatic differentiation can be decomposed into unrolling a program into a term denoting an analytic function with the same derivative at a given input as the original program, symbolically differentiating the function using a differential calculus for primitive functions and general rules for constant, linear and bilinear functions as well as rules for function combinators, and finally computing the (Hermitian) adjoint of the derivative symbolically without using matrices, which are too inefficient to use for functions on high-dimensional spaces. The resulting symbolic representation of a linear map can be interpreted as a data-parallel program ready for compilation to a modern GPU-architecture. This turns out to be behaviorally equivalent to reverse-mode automatic differentiation, but different in not using dual (scalar) numbers. In particular, it opens opportunities for optimization on high-dimensional functions, where matrices are too inefficient to represent linear maps. We illustrate the approach with examples from deep learning, where functions on (very) high-dimensional spaces are common.
The Programming of Algebra (Fritz Henglein, Mikkel Kragh Mathiesen and Robin Kaarsgaard)
We present module theory and linear maps as a powerful generalised and computationally efficient framework for the relational data model, which underpins today’s relational database systems. Based on universal constructions of modules we obtain compact and computationally efficient data structures for data collections corresponding to union and deletion, repeated union, Cartesian product and key-indexed data. Free modules naturally give rise to polysets, which generalise multisets and facilitate expressing database queries as multilinear maps with asymptotically efficient evaluation on polyset constructors. We introduce compact maps as a way of representing infinite (poly)sets constructible from an infinite base set and its elements by addition and subtraction. We show how natural joins generalise to algebraic joins, while intersection is implemented by a novel algorithm on nested compact maps that carefully avoids visiting parts of the input that do not contribute to the eventual output. Our algebraic framework leads to a worst-case optimal evaluation of cyclic relational queries, which is known to be impossible using textbook query optimisers that operate on lists of records only.
Contributed session 1: 10:30-12:30
10:30
Martin Elsman, Fritz Henglein, Robin Kaarsgaard, Mikkel Kragh Mathiesen and Robert Schenck,
Combinatory adjoints and differentiation (slides, video)
11:00
Mathieu Montin, Amélie Ledein and Catherine Dubois,
LIBNDT: Towards a formal library on spreadable properties over linked nested datatypes (slides, video)
11:30
Petr Kourzanov,
Tableless calculation of circular functions on dyadic rationals (slides, video)
12:00
Fritz Henglein, Mikkel Kragh Mathiesen and Robin Kaarsgaard,
The Programming of Algebra (slides, video)
Contributed session 2: 14:00-16:00
14:00
Robert Atkey,
Data Types with Negation (slides, video)
14:30
Joris Ceulemans, Andreas Nuyts and Dominique Devriese,
Sikkel: Multimode Simple Type Theory as an Agda Library (slides, video)
15:00
Dylan McDermott and Tarmo Uustalu,
What makes a strong monad (slides, video)
15:30
Alexandre Garcia de Oliveira, Mauro Jaskelioff and Ana Cristina Vieira de Melo,
On Structuring Functional Programs with Monoidal Profunctors (slides, video)
Keynote: 16:30-17:30
16:30
Valeria de Paiva,
Going Without: A Linear Modality and its Role (slides, video)
Submissions are welcomed on, but by no means restricted to, topics such as:
Please contact the programme chairs Max New and Jeremy Gibbons if you have any questions about the scope of the workshop.
We accept two categories of submission: full papers of no more than 15 pages that will appear in the proceedings, and extended abstracts of no more than 2 pages which we will post on the website, but which do not constitute formal publications and will not appear in the proceedings. References and appendices are not included in page limits. Appendices may not be read by reviewers.
Full papers (not two page talk abstracts) must report previously unpublished work and not be submitted concurrently to another conference with refereed proceedings. Accepted papers and talks must be presented at the workshop by at least one of the authors.
The proceedings will be published under the auspices of EPTCS with a Creative Commons license. Papers must be prepared in LaTeX using the EPTCS macro package.
We are using EasyChair to manage submissions.
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 organized 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 organized 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 organized 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 organized 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.