NL-FP Day 2020:

The Netherlands Functional Programming Day is an annual gathering of researchers, students, and practitioners sharing a common interest in functional programming. The day features talks that cover the latest advances in research, teaching and applications in the area of functional programming and (implementation of) functional languages.

Coffee and lunch breaks provide ample opportunity for networking with your colleagues and meeting new people. Experts and newcomers to the field are equally welcome. Colleagues from neighboring countries are more than welcome to attend; the language of the FP Day is English.

The NL-FP Day 2020 takes place on Friday, January 10, 2020 and will be hosted by the University of Amsterdam in the historic Doelenzaal of the Amsterdam University Library, Singel 425, right in the heart of Amsterdam.

The Netherlands Functional Programming Day 2020 is generously sponsored by the Informatics Institute of the University of Amsterdam.

Call for presentations:

The FP Day consists of a number of contributed talks. Work in progress talks are just as welcome as talks about mature work recently presented at international conferences.

Please, upload your talk proposals via EasyChair including a short abstract for the FP Day programme.

Deadline: December 17, 2019.

Registration:

Participation is free of charge, but registration is required.

Deadline: December 20, 2019

Registration is now closed.

Programme:

• 09:45 - 10:15 Arrival Doelenzaal, Amsterdam University Library
• 10:15 - 10:20 Welcome to the FP Day, Clemens Grelck
• 10:20 - 10:45 PloNK: Functional Probabilistic NetKAT, Alexander Vandenbroucke
• 10:45 - 11:10 Piecewise Relative Observational Purity, Seyed Haeri
• 11:10 - 11:40 Coffee and tea break
• 11:40 - 12:05 Futhark: a Functional Array Language, Troels Henriksen
• 12:05 - 12:30 Tensor Comprehensions in SaC, Sven-Bodo Scholz
• 12:30 - 14:00 Lunch break
• 14:00 - 14:25 Mu: Easy Microservices using Type-level Techniques, Alejandro Serrano
• 14:25 - 14:50 A New View on Parser Combinators, Pieter Koopman
• 14:50 - 15:15 Lazy Interworking of Compiled and Interpreted Code, Camil Staps
• 15:15 - 15:45 Coffee and tea break
• 15:45 - 16:10 A DSL for Fluorescence Microscopy (experience report), Birthe van den Berg
• 16:10 - 16:35 Clash 1.0: the Tricks we used for our new API, Martijn Bastiaan
• 16:35 - 17:00 A Symbolic Execution Semantics for TopHat, Markus Klinik
• 17:00 - 17:15 Closing, announcements, everything else
• 17:15 - 17:45 Drinks
• 18:00 Dinner

Lunch

We have lunch in the Cafe of the University of Amsterdam's Allard Pierson Museum, a 5-minute walk from the University Library. The address is Oude Turfmarkt 127, 1012 GC Amsterdam.

Dinner

As usual, the NL-FP Day ends with a dinner in a near-by restaurant. The dinner is optional and at your own cost.

We have an Indonesian Rijstafel in Restaurant Puri Mas, another 5-mniute walk from the University Library. The address is Lange Leidsedwarsstraat 37-41, 1017 NG Amsterdam. The price per person is EUR 27,50 plus drinks.

Abstracts:

PloNK: Functional Probabilistic NetKAT

Alexander Vandenbroucke, KU Leuven

This work presents PloNK, a functional probabilistic network programming language that extends Probabilistic NetKAT (PNK). Like PNK, it enables probabilistic modelling of network behaviour, by providing probabilistic choice and infinite iteration (to simulate looping network packets). Yet, unlike PNK, it also offers abstraction and higher-order functions to make programming much more convenient.

The formalisation of PloNK is challenging for two reasons: Firstly, network programming induces multiple side effects (in particular, parallelism and probabilistic choice) which need to be carefully controlled in a functional setting. Our system uses an explicit syntax for thunks and sequencing which makes the interplay of these effects explicit. Secondly, measure theory, the standard domain for formalisations of (continuous) probablistic languages, does not admit higher-order functions. We address this by leveraging omega-Quasi Borel Spaces (omegaQBSes), a recent advancement in the domain theory of probabilistic programming languages.

We believe that our work is not only useful for bringing abstraction to PNK, but that—as part of our contribution—we have developed the meta-theory for a probabilistic language that combines advanced features like higher-order functions, iteration and parallelism, which may inform similar meta-theoretic efforts.

Piecewise Relative Observational Purity

Seyed Haeri, UC Louvain

Distributed systems programming exhibits a considerable degree of mostly-functional behaviour. On the other hand, programming every distributed system with no side-effect whatsoever is not realistic. Observational purity lends itself as a plausible alternative.

To exercise that choice for programming distributed systems, we present the λ(port) family of λ-Calculi. Ports and pure blocks are two characteristics of this family. Ports are the only single source of side-effects in the λ(port) family. Pure blocks are their linguistic support for declaring observational purity. Notably, pure blocks specify which nodes in the distributed system they are pure for. We promote a programming paradigm, in which, the programmer strives to maximise pure blocks and only leave the unavoidably effectful computations outside. Our paradigm brings added value to speculative execution, mock testing, distributed garbage collection, partial order reduction, and treatments of flaky tests.

We start the λ(port) family from its most basic member, in which messages are delivered instantly. We prove that observational equivalences of the more basic members of the family are retained upon addition of message delay, message loss, node failure, and network partitions. As such, one can freely prove observational equivalences in the most basic member without worrying about any of the successor features.

Futhark: a Functional Array Language

Troels Henriksen, University of Copenhagen

Futhark is a purely functional data parallel functional language aimed at high-performance execution, in particular on GPUs. The goal is to provide a programming experience that is familiar to functional programmers, in particular involving the usual map/reduce/scan vocabulary and a programmer's view of multidimensional arrays as nested lists, yet with enough restrictions that an optimising compiler can convert it to very efficient code.

I will talk about the design of Futhark as a language, the implementation of its compiler (with a particular focus on handling nested parallelism), and a demonstration of how to it can be put to practical use.

Tensor Comprehensions in SaC

Sven-Bodo Scholz, Radboud University Nijmegen

Array comprehensions in principle are well established within the declarative community. When it comes to catering not only for arrays of fixed dimensionalities but for shape-invariant specifications as well, things become more challenging. The generality of such shape-invariant array expressions often requires complex and thus potentially error-prone boundary specifications of index ranges as well as non-trivial shape specifications.

In this talk, we propose a new form of array comprehensions named "Tensor Comprehensions" which allows such bounds and shapes to be partially or fully compiler inferred. In contrast to earlier work, this work builds on sophisticated partial evaluation technology to ensure a higher degree of shape and boundary inference than before.

The resulting notation combines the basic principle of array-comprehensions with syntactical shortcuts very close to those found in the so-called Tensor Notations used in Physics and Mathematics. As a result, complex operators with rich semantics can be defined more concisely than before.

Mu: Easy Microservices using Type-level Techniques

Alejandro Serrano, 47 Degrees

Microservices are a common architectural pattern nowadays. However, a lot of complexity happens "at the borders" of each microservice, that is, in the serialization and transport of information.

Mu is a Haskell library whose aim is for you to focus on the core logic, and not on those implementation details. With Mu you can use an existing schema (for example, in Protocol Buffers), turn it into type-level information, and then serve them in a variety of formats (like gRPC). Mu uses quite some GHC type-level machinery to achieve its goals. You can think of it as "Servant, but for microservices".

This talk explores both the practical usage of the library and some of the interesting design decisions.

A New View on Parser Combinators

Pieter Koopman, , Radboud University Nijmegen

Parser combinators offer a concise and fast way to produce reasonably efficient parsers. The combinator libraries themselves can be small and provide an elegant application of functional programming techniques. They are one of the success stories in functional programming that are also ported to many other languages.

In this paper, we illustrate that we can make the parser combinators more general by modeling them as a tagless domain specific language. The idea is to replace the ordinary combinators by a set of type constructor classes. By making different implementations of this class we can assign various interpretations of one and the same grammar specification. The set of type classes makes the DSL type-safe and extendable without needing to change existing parts and implementations. This enables us to make multiple interpretations, views, of the specified grammar. We show that apart from parsing based on this DSL one can show the implemented grammar, generate parse trees produced by the grammar without needing the corresponding input, generate inputs accepted by the grammar, adapt the grammar rules such that the parser combinators can handle left-recursion and so on. This makes our multi-view parser combinators more powerful than the existing approaches.

Lazy Interworking of Compiled and Interpreted Code

Camil Stap, Radboud University Nijmegen

More and more applications rely on the safe execution of code unknown at compile-time, for example in the implementation of web browsers and plugin systems. Furthermore, these applications usually require some form of communication between the added code and its embedder where data can be passed in both directions. In a functional language, these problems are theoretically the same, since functions are data. To demonstrate this, we describe the implementation of a serialization library for the language Clean, which internally uses an interpreter to evaluate code in a separate, sandboxed environment. The interpreter interworks at a low level with the host language, but required no changes to its runtime system, and is therefore easily ported to other contexts. We also use this setup on the web, to share lazy values between a (native Clean/iTasks) server and a client, running the interpreter in WebAssembly. The interface becomes simpler compared to the previous solution (which compiled Clean to JavaScript through SAPL) because data does not need to be converted any more.

A DSL for Fluorescence Microscopy (experience report)

Birthe van den Berg, KU Leuven

Fluorescence microscopy is a key tool in the life sciences to explore the inner workings of cells and tissues. Yet, the growing complexity of experimental equipment, such as microscopes, perturbation devices, etc., has become a pressing problem. Since manual operation is no longer manageable for the new research applications of high-content imaging, the field is in dire need of automation. We tackle these problems by advancing the state-of-the-art in programming languages to automate the equipment control and let operators in a declarative and user-friendly way set up their experiments. For this reason, Haskell is perfectly suited for the software that interfaces the hardware components (e.g., light source, filters, camera), constructs programs and so on.

For program construction, we use a deeply embedded domain-specific language (DSL) with a free-monad structure. Folds transform recursive functions into definitions. The field of fluorescence microscopy is an ideal application for these recent, theoretic program features. The Dedecker lab of the KU Leuven, which does research on fluorescence microscopy, offers a good opportunity to evaluate the software and to bring these concepts into practice. In this talk I present my experience of designing a deeply embedded DSL in Haskell for controlling fluorescence experiments. I will describe the added value of a free-monad structure and folds, the current implementation and the impact on the field of fluorescence microscopy, where the rate of discovery and innovation has increased significantly.

Clash 1.0: the Tricks we used for our new API

Martijn Bastiaan, QBayLogic

Clash is a BSD-licensed Haskell to hardware compiler, actively developed by QBayLogic and the Clash community. Last summer we released Clash 1.0, exactly 10 years after its first public release. This release packs a number of new features over the last release, including a redesigned API. In this presentation, we'll go over the reasons for this redesign and the techniques we used to design it.

A Symbolic Execution Semantics for TopHat

Markus Klinik, Radboud University Nijmegen

Task-Oriented Programming (TOP) is a programming paradigm that allows declarative specification of workflows. TOP is typically used in domains where functional correctness is essential, and where failure can have financial or strategical consequences. In this talk we aim to make formal verification of software written in TOP easier. Currently, only testing is used to verify that programs behave as intended.

We use symbolic execution to guarantee that no aberrant behaviour can occur. In previous work we presented TopHat, a formal language that implements the core aspects of TOP. In this talk we develop a symbolic execution semantics for TopHat. Symbolic execution allows to prove that a given property holds for all possible execution paths of TopHat programs.

We show that the symbolic execution semantics is consistent with the original TopHat semantics, by proving soundness and completeness. We present an implementation of the symbolic execution semantics in Haskell. By running example programs, we validate our approach. This work represents a step forward in the formal verification of TOP software.

Contact

Clemens Grelck, University of Amsterdam

M: c.grelck@uva.nl

W: https://staff.fnwi.uva.nl/c.u.grelck