Program

MPC 2022 will be run as a hybrid conference with both in-person and online talks. In-person talks will be broadcast online (link will be sent out closer to the date). Online talks will be broadcast both online and in the conference hall at CLAS.

I will present recent and ongoing work on giving a semantic foundation to training algorithms in machine learning using the categorical formalisms of lenses. Lenses provide a much needed unifying perspective on various classes of such algorithms, as well as offering a different style of specifying and proving properties of training protocols. They also enable the study of machine learning for new classes of models such as Boolean circuits and polynomial circuits. In the last part of the talk I will also discuss how this foundation informs the development of new tools for the formal verification of machine learning algorithms.

When modelling side-effects using a monad, we need to equip the monad with effectful operations. This can be done by noting that each algebra of the monad carries interpretations of the desired operations. We consider the analogous situation for graded monads, which are a generalization of monads that enable us to track quantitative information about side-effects. Grading makes a significant difference: while many graded monads of interest can be equipped with similar operations, the algebras often cannot. We explain where these operations come from for graded monads. To do this, we introduce the notion of flexibly graded monad, for which the situation is similar to the situation for ordinary monads. We then show that each flexibly graded monad induces a canonical graded monad in such a way that operations for the flexibly graded monad carry over to the graded monad. In doing this, we reformulate grading in terms of locally graded categories, showing in particular that graded monads are a particular kind of relative monad. We propose that locally graded categories are a useful setting for work on grading in general.

Structured recursion schemes have been widely used in constructing, optimising, and reasoning about programs over inductive and coinductive datatypes. Their plain forms, catamorphisms and anamorphisms, are restricted in expressiveness. Thus many generalisations have been proposed, which further lead to several unifying frameworks of structured recursion schemes. However, the existing work on unifying frameworks typically focuses on the categorical foundation, and thus is perhaps inaccessible to practitioners who are willing to apply recursion schemes in practice but are not versed in category theory. To fill this gap, this survey paper introduces structured recursion schemes from a practical point of view: a variety of recursion schemes are motivated and explained in contexts of concrete programming examples. The categorical duals of these recursion schemes are also explained.

Behavioural equivalence for functional languages with algebraic effects and general recursion is often difficult to formalize. When modelling the behaviour of higher-order programs, one often needs to employ multiple coinductive structures simultaneously. In this paper, we aim to simplify the issue with a single external stream monad dealing with recursion, and deal with the structures for modelling higher-order types in a purely inductive (finite) manner. We take a page from classical domain theory, modelling recursive programs as limits of increasing sequences of “finite” denotational elements. We carry around a single relation which contains all relevant information of behaviour: self-related elements are considered correct according to the denotational semantics, and two elements that are related both ways are considered equivalent. We implement equivalence of effectful programs using a relation lifting, creating a notion of behavioural equivalence for approximations. This is lifted to behavioural equivalence for recursive programs modelled by sequences of approximations, using a relator implementing a notion of weak similarity. We apply this to a fragment of call-by-push-value lambda calculus with algebraic effects, and establish a denotational equivalence which is sound with respect to an operational semantics, and sound with respect to contextual equivalence.

Weak distributive laws were considered recently in the work of Garner as a means of composing monads for which there is no strong distributive law. For example, the canonical weak distributive law exhibited in Garner’s work between the powerset and the ultrafilter monad can be used to exhibit the Vietoris monad on compact Hausdorff spaces as a weak lifting of the powerset monad. Other weak distributive laws were considered in our work with Alexandre Goy. In particular we obtained a weak distributive law between the powerset monad and the distribution monad, which exhibits the convex powerset monad on barycentric algebras as a weak lifting of the powerset monad.

One essential ingredient in the theory of weak distributive laws is the notion of semialgebras for a monad, that is, algebras for the underlying functor of the monad subject to the associativity axiom alone. In this talk I will discuss the algebraic nature of the semialgebras of a monad. If the underlying category has coproducts then semialgebras for a monad “ M” are in fact the Eilenberg-Moore algebras for a suitable monad structure on the functor “id + M “, which we call the semifree monad. Then I discuss how weak distributive laws between a monad “M” and “ T” can be seen as strong distributive laws between the semifree monad on “M ” and “T“, subject to an additional condition. This is joint work with Ralph Sarkis.

Where do data structures come from? This paper explores how to systematically derive implementations of one-sided flexible arrays from a simple reference implementation. Using the dependently typed programming language Agda, each calculation constructs an isomorphic—yet more efficient—data structure using only a handful of laws relating types and arithmetic. Although these calculations do not generally produce novel data structures they do give insight into how certain data structures arise and how different implementations are related.

Functional programs with side effects represented by monads are amenable to equational reasoning. This approach to program verification is called monadic equational reasoning and has been experimented several times using proof assistants based on dependent type theory. These experiments have been performed in isolation using different proof assistants but they nevertheless reveal similar technical issues.

As an effort towards the construction of a reusable framework for monadic equational reasoning, we report on several practical improvements of Monae, a Coq library for monadic equational reasoning. First, to improve the scalability of Monae, we reimplement its hierarchy of effects using a generic tool to build hierarchies of mathematical structures. We show that this refactoring allows for easy extensions of the Monae hierarchy with new monad constructs. Second, we discuss a well-known but recurring technical difficulty due to the shallow embedding of monads in the proof assistant. Concretely, it often happens that the return type of monadic functions is not informative enough to complete formal proofs, in particular termination proofs. We explain library support to facilitate this kind of proof using standard Coq extensions. Third, we augment Monae with an improved theory about nondeterministic permutations. In particular, these technical contributions allow for a complete formalization of quicksort derivations by Mu and Chiang.

Neural networks are typically represented as data structures that are traversed either through iteration or by manual chaining of method calls. However, a deeper analysis reveals that structured recursion can be used instead, so that traversal is directed by the structure of the network itself. This paper shows how such an approach can be realised in Haskell, by encoding neural networks as recursive data types, and then their training as recursion scheme patterns. In turn, we promote a coherent implementation of neural networks that delineates between their structure and semantics, allowing for compositionality in both how they are built and how they are trained.

Subtypes are useful and ubiquitous, allowing important properties of data to be captured directly in types. However, the standard encoding of subtypes gives no control over when the reduction of subtyping proofs take place, which can have a significant impact on the performance of type-checking. In this article, we show how operations on a subtype can be represented in a more efficient manner that exhibits no reduction behaviour. We present the general form of the technique in Cubical Agda by exploiting its support by higher-inductive types, and demonstrate the practical use of the technique with a number of programming examples.

Featherweight Go (FG) is a minimal core calculus that includes essential Go features such as overloaded methods and interface types. The most straightforward semantic description of the dynamic behavior of FG programs is to resolve method calls based on run-time type information. A more efficient approach is to apply a type-directed translation scheme where interface-values are replaced by dictionaries that contain concrete method definitions. Thus, method calls can be resolved by a simple lookup of the method definition in the dictionary. Establishing that the target program obtained via the type-directed translation scheme preserves the semantics of the original FG program is an important task.

To establish this property we employ logical relations that are indexed by types to relate source and target programs. We provide rigorous proofs and give a detailed discussion of the many subtle corners that we have encountered including the need for a step-index due to recursive interfaces and method definitions.

An effectful traversal of a data structure iterates over every element, in some predetermined order, collecting computational effects in the process. Depth-first effectful traversal of a tree is straightforward to define in a compositional way, since it precisely follows the shape of the data. What about breadth-first effectful traversal? An indirect route is to factorize the data structure into shape (a structure of units) and contents (a vector of elements, in breadth-first order), traverse the vector, then rebuild the data structure with new contents. We show that this can instead be done directly, using staging. That staging is captured using a construction related to free applicative functors. Moreover, the staged traversals lend themselves well to fusion; we prove a novel fusion rule for effectful traversals, and use it in another solution to Bird’s “repmin” problem.

Every place in Pascal’s triangle enumerates the paths to that place, zig-zagging downwards from the top, but we can do more than count them. Binomial coefficients make for remarkable dependent types: bit vectors indexed by their length and one-count can document selections from data structures, or the embedding of a term’s support into its scope. They become all the more discriminating when you recognize that numerical indices are but the erasures of richer, individuating information. They compose in sequence categorically, and in parallel monoidally. Being made of bits, you can do Boolean logic with them, but with your eyes open as to their meaning. Working with Pascal’s Triangle, rendered into types, has changed the way I see and organise data in general, and syntactic data in particular. I shall recount my path to this place, and seek to find the meaning in the turns of my journey.

Speakers
  – Semantics for machine learning (Fabio Zanasi)
  – Types and functional programming for machine learning (Nicolas Wu)
  – Formalising machine learning (Reynald Affeldt)