Preface

This volume contains the proceedings of the Seventh Workshop on Mathematically Structured Functional Programming (MSFP 2018), which took place 8th July 2018 in Oxford UK, as an affiliated workshop of FSCD 2018, part of the Federated Logic Conference (FLoC) 2018.

MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantics and type theory as they are increasingly reflected in programming practice, especially functional programming. As the range of papers presented in this year's workshop shows, this continues to be a fruitful interface.

This year, we were honoured to host two invited speakers:

• Tamara von Glehn
  Polynomial models of type theory
• Didier Remy
  Ornamentation put into practice in ML

New this year, we accepted presentation-only extended abstracts as well as full papers. We are grateful to our programme committee for carrying out the work of selecting the papers and extended abstracts. In the end, two extended abstracts were accepted for presentation, and and four full papers were accepted for presentation and inclusion in this proceedings.

The programme committee:

• Andreas Abel, Chalmers, Sweden
• Danel Ahman, INRIA Paris, France
• Robert Atkey, University of Strathclyde, UK (co-chair)
• Jeremy Gibbons, University of Oxford, UK
• Jennifer Hackett, University of Nottingham, UK
• Mauro Jaskelioff, Universidad Nacional de Rosario, Argentina
• Shin-ya Katsumata, National Institute of Informatics, Japan
• Sam Lindley, University of Edinburgh, UK (co-chair)
• Clare Martin, Oxford Brookes University, UK
• Shin-Cheng Mu, Academia Sinica, Taiwan
• Valeria de Paiva, Nuance Communications, US
• Alexandra Silva, University College London, UK

Robert Atkey and Sam Lindley, July 2018.

Polynomial Models of Type Theory

Polynomials (also known as containers) represent datatypes which, like polynomial functions, can be expressed using sums and products. Extending this analogy, I will describe the category of polynomials in terms of sums and products for fibrations. This category arises from a distributive law between the pseudomonad 'freely adding' indexed sums to a fibration, and its dual adding indexed products. A fibration with sums and products is essentially the structure defining a categorical model of dependent type theory. I will show how the process of adding sums to such a fibration is an instance of a general 'gluing' construction for building new models from old ones. In particular we can obtain new models of type theory in categories of polynomials. Finally, I will explore the properties of other type formers in these models, and consider which logical principles are and are not preserved by the construction.

Ornamentation put into Practice in ML

Ornaments have been introduced as a means to lift functions operating on some datatype into new functions operating on an ornamentation of this datatype, i.e., a variant of this datatype carrying additional information. A typical example consists in viewing lists as an ornamentation of natural numbers and then lifting the addition into the concatenation---the user just providing the missing parts of the code. Ornaments have first been introduced in Agda and extensively studied in a categorical setting.

We have been exploiting and adapting the idea of ornamentation in the context of ML. Here, we are interested in syntactic liftings where the lifted function is related to the original one as in the general setting but with a closer correspondence: on the one hand, the behavior (and ideally the computation steps) of the lifted function should coincide with the behavior of the original function, except for the additional user-provided code; on the other hand, the lifted code should be as close as possible to the code the user would have manually written.

Our approach is to first synthesize a generic version of the base program that can then be specialized to any ornamentation of the base version (including the base version as a particular case), and finally simplified. While the generic version of ML base code requires some form of dependent types to typecheck, we ensure by construction, using staged computation and dependent types, that each instantiation to concrete ornaments can be simplified back into ML code.

We use parametricity to show the correspondence between the base and lifted versions. We verified on (small) examples that the lifted code is often close to hand-written code.

This approach to ornamentation can be extended to perform disornamentation---with new design challenges and interesting applications. Ornamentation and disornamentation are just two examples of a more general type-based approach to code refactoring and evolution.