Published: 5th June 2014|
|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|
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:
Relational Parametricity beyond Type Abstraction
Logical Relations for Monads by Categorical TT-Lifting
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
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 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.