Published: 5th June 2014
DOI: 10.4204/EPTCS.153
ISSN: 2075-2180

EPTCS 153

Proceedings 5th Workshop on
Mathematically Structured Functional Programming
Grenoble, France, 12 April 2014

Edited by: Paul Levy and Neel Krishnaswami

Preface
Invited Presentation: Relational Parametricity beyond Type Abstraction
Robert Atkey
1
Free Applicative Functors
Paolo Capriotti and Ambrus Kaposi
2
Monad Transformers for Backtracking Search
Jules Hedges
31
Normalization by Evaluation in the Delay Monad: A Case Study for Coinduction via Copatterns and Sized Types
Andreas Abel and James Chapman
51
Coherence for Skew-Monoidal Categories
Tarmo Uustalu
68
Invited Presentation: Logical Relations for Monads by Categorical TT-Lifting
Shin-ya Katsumata
78
Polymonadic Programming
Michael Hicks, Gavin Bierman, Nataliya Guts, Daan Leijen and Nikhil Swamy
79
Koka: Programming with Row Polymorphic Effect Types
Daan Leijen
100
Categorical Semantics for Functional Reactive Programming with Temporal Recursion and Corecursion
Wolfgang Jeltsch
127
Foundations of Total Functional Data-Flow Programming
Baltasar Trancón y Widemann and Markus Lepper
143

Preface

This volume contains the proceedings of the Fifth Workshop on Mathematically Structured Functional Programming (MSFP 2014), taking place on 12 April, 2014 in Grenoble, France, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014.

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.

We are honoured to host the following invited speakers:

We are grateful to our programme committee:

and to Guillaume Allais, Fredrik Nordvall Forsberg, and Neil Sculthorpe for additional reviewing. We would also like to thank the ETAPS 2014 organizers, and the EPTCS staff.

Neel Krishnaswami and Paul Blain Levy, April 2014


Relational Parametricity beyond Type Abstraction

Robert Atkey

John Reynolds' theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields "free" theorems about programs just from their types. The range of applications of relational parametricity is dazzling: including data type representations, non-inhabitation results, and program optimisation.

I will talk about recent work that has extended Reynolds' theory beyond invariance under changes of data type representation to other kinds of invariants. Quantifying over geometrical transformations allows for free theorems for programs that manipulate geometric data, capturing geometric invariance properties. Likewise, quantifying over distances yields free theorems capturing continuity properties. The range of applications of generalised relational parametricity is equally promising: for example, geometric free theorems can be connected to classical mechanics and Noether's theorem to yield physical conservation laws directly from types.


Logical Relations for Monads by Categorical TT-Lifting

Shin-ya Katsumata (Kyoto University)

Logical relations are widely used to study various properties of typed lambda calculi. By extending them to the lambda calculus with monadic types, we can gain understanding of the properties on functional programming languages with computational effects. Among various constructions of logical relations for monads, I will talk about a categorical TT-lifting, which is a semantic analogue of Lindley and Stark's leapfrog method.

After reviewing some fundamental properties of the categorical TT-lifting, we apply it to the problem of relating two monadic semantics of a call-by-value functional programming language with computational effects. This kind of problem has been considered in various forms: for example, the relationship between monadic style and continuation passing style representations of call-by-value programs was studied around '90s. We give a set of sufficient conditions to solve the problem of relating two monadic semantics affirmatively. These conditions are applicable to a wide range of such problems. If time permits, I will also talk about a variant of this result, namely a generic soundness for the effect systems over effect monoids.