Welcome

The Dutch Functional Programming Day (also known as FP Dag) 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 and colleagues from neighbouring countries are welcome to attend; the language of the FP Day is English.

Dinner at Vakwerkhuis

*Registration for dinner is full.

Addres Vakwerkhuis: Professor Snijdersstraat 2, 2628 RA, Delft

(Approx. 10 minute walking distance from the Aula Conference Centre). If you ticked the dinner box in the registration form you can expect a delicious buffet including vegetarian and vegan options. If you have other dietary restrictions, please use the contact details below to inform us.

Speakers & Abstracts

A Mondiac Framework for Name Resolution in Multi-phased Type Checkers

Speaker: Aron Zwaan
Type: Academic
Topic: Type systems

Abstract: An important aspect of type checking is name resolution - i.e., determining the types of names by resolving them to a matching declaration. For most languages, we can give typing rules that define name resolution in a way that abstracts from what order different units of code should be checked in. However, implementations of type checkers in practice typically use multiple phases to ensure that declarations of resolvable names are available before names are resolved. This gives rise to a gap between typing rules that abstract from order of type checking and multi-phased type checkers that rely on explicit ordering.

This paper introduces techniques that reduce this gap. First, we introduce a monadic interface for phased name resolution which detects and rejects type checking runs with name resolution phasing errors where names were wrongly resolved because some declarations were not available when they were supposed to be. Second, building on recent work by Gibbons et al., we use applicative functors to compositionally map abstract syntax trees onto (phased) monadic computations that represent typing constraints. These techniques reduce the gap between type checker implementations and typing rules in the sense that (1) both are given by compositional mappings over abstract syntax trees, and (2) type checker cases consist of computations that roughly correspond to typing rule premises, except these are composed using monadic combinators. We demonstrate our approach by implementing type checkers for Mini-ML with Damas-Hindley-Milner type inference, and LM, a toy module language with a challenging import resolution policy.

Representing Syntax and Semantics

Speaker: Jaro Reinders
Type: Academic
Topic: Semantics

Abstract: In this presentation, we’re taking a look at syntax representations such as variants of De Bruijn indices and HOAS. We look at conversions between these representations. Finally, we apply what we learn to free monads which model the semantics of effectful programs.

When the Types Align: A coincidence of total and partial correctness with a slice of cubical Agda

Presenter: Cass Alexandru (coauthors: Jurriaan Rot & Niels van der Weide)
Type: Academic
Topic: Type systems

Abstract: Functional programmers are usually familiar with folds. Less commonly used are unfolds; these are operations for "growing" a datastructure and as such, their codomain usually includes infinite datastructures. In total languages s.a. Agda these have to be modeled as codata, which can be a hassle to deal with, and you want to avoid this if you know your unfolds should produce only finite datastructures. We take sorting algorithms defined using unfolds from the paper "Sorting with Bialgebras and Distributive Laws" (HJHWM, 2012) and recast intrininsically verified versions in the same categorical mold, discovering along the way how achieving partial correctness using a Higher Inductive Type for finite multisets also gives us total correctness, i.e. data instead of codata as the target of an unfold.

Functional influences on a Python-embedded scientific workflow library

Speaker: Ben Clifford
Type: Academic
Topic: Scientific computing

Abstract: Parsl is a library for implementing scientific workflows in Python. Although we rarely present it this way, there are a lot of functional programming influences in the implementation of Parsl, and in this talk I'll try to present both scientific workflows and Parsl from that angle.

First I'll introduce the very broad field of scientific workflow, and the corner of it that we work in. Then I'll talk about our core execution model that is based around futures with an applicative functor or monadic structure. I'll talk about how we override some Python syntax to get the behaviour we want, while still mostly looking like Python, and I'll talk about some of the history and human factors that drove us to consider Python as a host language. I'll also touch on some other Parsl topics that overlap with the functional community: for example, trying to understand equality between objects in different Python environments across time and space, especially functions; recording provenance of generated scientific outputs for reproducibility; how our programming interface has helped other people build compositional libraries for "doing science" on top of Parsl.

Salix: Elm-like Web Programming in Rascal

Speaker: Tijs van der Storm
Type: Academic
Topic: Web programming

Abstract: Elm is small purely functional language for web-programming designed by Evan Czaplicki. I’ve ported this language to Rascal as an embedded DSL/library. I will discuss some trade-offs and challenges in the design and demonstrate its abilities and limitations.

Making Haskell look like WebAssembly

Speaker: Alex Ionescu
Type: Academic
Topic: Web programming

Abstract: WebAssembly is a new portable low-level language meant to increase interoperability and security across the software ecosystem. In this talk, we'll explore `wasm-hs`, a domain-specific language for embedding WebAssembly in Haskell. We'll leverage Haskell's powerful type system to enforce the safety rules of WebAssembly, and we'll see how far we can overload Haskell's syntax to make it look and feel like WebAssembly.

Efficient functional programs - ideas from the Roc programming language

Speaker: Folkert de Vries
Type: Industrial
Topic: Efficiency

Abstract: Roc wants to be a fast, friendly, functional language. It relies heavily on academic research to realize this vision. In particular I'd like to talk about these 4 technical ideas and our experience implementing them.

• • platforms: users swapping out the language runtime
  • defunctionalization that preserves control/information flow
  • reference counting for opportunistic in-place mutation
  • structural sum types

File Format Migrations on the Type-Level

Speaker: Victor Miraldo
Type: Industrial
Topic: Type systems

Abstract:Have someone added a field to some JSON, which stays in a DB somewhere? Or worse, some engineer created a brand new XML tag meant to supersede two or three others on your proprietary settings file? Migrations are an unfortunate but constant challenge we face when dealing with production systems. At Channable, we were tired of relying on run-time checks and bit the bullet: we created a type-level abstraction to make sure that when we change
some existing file, we are forced to provide an upstream and downstream migration. On this session I'd like to show you how it looks, explain how it works and challenge you to help me make it better!

Harnessing the Power of Functional Programming for Resilient and Efficient Autonomous Control Systems

Speaker: Abdu Saif
Type: Academic
Topic: Applications

Abstract: As the demand for autonomous control systems continues to grow across various academic and industries, the need for robust, reliable, and efficient control algorithms becomes increasingly critical. The efficient control algorithms of autonomous control systems become paramount to establish a foundation for resilient and adaptive control solutions. This presentation explores the integration of functional programming (FP) paradigms within the MATLAB environment to design, develop, and test autonomous systems. By leveraging FP principles such as an immutable data structure, higher-order function that calculates the updated state control logic and updating the vehicle's state and displaying the position at each iteration. In this context, the design, development, and testing of autonomous systems aim to improve the Power Consumption Rate parameter. This parameter controls the rate at which power is consumed based on specific requirements and system characteristics over time.

Babashka: a meta-circular Clojure interpreter for the command line

Speaker: Michiel Borkent
Type: Industrial
Topic: Scripting and libraries

Abstract: Babashka is a Clojure interpreter for cross platform scripting. It is available as a single binary that starts instantly. It makes Clojure a viable replacement for writing bash scripts. Babashka comes with a handful of libraries out of the box (JSON, command line parsing, etc.) and supports loading libraries from the Clojure ecosystem. The interpreter is written in a meta-circular approach, akin to Structure and Interpretation of Computer Programs. It is compiled to a single binary using GraalVM native-image which is the reason it starts fast, but also uses less memory than a JVM, Clojure's original runtime. As such, babashka brings together many exciting technologies to broaden the reach of Clojure even more. This talk explores the high level use cases of babashka, its impact on the Clojure community, its history, technical implementation details and the author's approach to open source development.