ICFP Workshops 2021
26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021)

Title Page

Message from the Chairs
Welcome to the 14th ACM SIGPLAN Haskell Symposium! The focus of the Symposium is to present original research on Haskell and to discuss the practical experience of working with the language. Due to the COVID-19 pandemic, the Symposium was held online on 26-27 August 2021, co-located with ICFP 2021.

Deadlock-Free Session Types in Linear Haskell
Wen Kokke  and Ornela Dardha 
(University of Edinburgh, UK; University of Glasgow, UK)
Priority Sesh is a library for session-typed communication in Linear Haskell which offers strong compile-time correctness guarantees. Priority Sesh offers two deadlock-free APIs for session-typed communication. The first guarantees deadlock freedom by restricting the process structure to trees and forests. It is simple and composeable, but rules out cyclic structures. The second guarantees deadlock freedom via priorities, which allows the programmer to safely use cyclic structures as well.
Our library relies on Linear Haskell to guarantee linearity, which leads to easy-to-write session types and more idiomatic code, and lets us avoid the complex encodings of linearity in the Haskell type system that made previous libraries difficult to use.

Article Search

Evaluating Linear Functions to Symmetric Monoidal Categories
Jean-Philippe Bernardy  and Arnaud Spiwack
(University of Gothenburg, Sweden; Tweag, n.n.)
A number of domain specific languages, such as circuits or data-science workflows, are best expressed as diagrams of boxes connected by wires. Unfortunately, functional languages have traditionally been ill-equipped to embed this sort of languages. The Arrow abstraction is an approximation, but we argue that it does not capture the right properties.
A faithful abstraction is Symmetric Monoidal Categories (SMCs), but, so far, it hasn't been convenient to use. We show how the advent of linear typing in Haskell lets us bridge this gap. We provide a library which lets us program in SMCs with linear functions instead of SMC combinators. This considerably lowers the syntactic overhead of the EDSL to be on par with that of monadic DSLs. A remarkable feature of our library is that, contrary to previously known methods for categories, it does not use any metaprogramming.

Article Search Artifacts Available

Graded Monads and Type-Level Programming for Dependence Analysis
Finnbar Keating  and Michael B. Gale 
(University of Warwick, UK)
Programmers make assumptions about the order of memory operations, which are not captured in the operations' types and therefore cannot be enforced statically by a compiler. This can lead programmers to accidentally violate those assumptions if they are not careful. To address this issue, we encode the memory locations that are accessed by a given computation using a graded monad. We use the data flow dependencies which arise from this to construct a type-level graph that we analyse to automatically order the computations so that no dependencies are violated. This also allows for computations which have no dependencies on each other to be run concurrently.

Article Search

Haskell⁻¹: Automatic Function Inversion in Haskell
Finn Teegen , Kai-Oliver Prott , and Niels Bunkenburg 
(University of Kiel, Germany)
We present an approach for automatic function inversion in Haskell. The inverse functions we generate are based on an extension of Haskell's computational model with non-determinism and free variables. We implement this functional logic extension of Haskell via a monadic lifting of functions and type declarations. Using inverse functions, we additionally show how Haskell's pattern matching can be augmented with support for functional patterns, which enable arbitrarily deep pattern matching in data structures. Finally, we provide a plugin for the Glasgow Haskell Compiler to seamlessly integrate inverses and functional patterns into the language, covering almost all of the Haskell2010 language standard.

Article Search Artifacts Available

Practical Normalization by Evaluation for EDSLs
Nachiappan Valliappan, Alejandro Russo, and Sam Lindley
(Chalmers University of Technology, Sweden; University of Edinburgh, UK)
Embedded domain-specific languages (eDSLs) are typically implemented in a rich host language, such as Haskell, using a combination of deep and shallow embedding techniques. While such a combination enables programmers to exploit the execution mechanism of Haskell to build and specialize eDSL programs, it blurs the distinction between the host language and the eDSL. As a consequence, extension with features such as sums and effects requires a significant amount of ingenuity from the eDSL designer. In this paper, we demonstrate that Normalization by Evaluation (NbE) provides a principled framework for building, extending, and customizing eDSLs. We present a comprehensive treatment of NbE for deeply embedded eDSLs in Haskell that involves a rich set of features such as sums, arrays, exceptions and state, while addressing practical concerns about normalization such as code expansion and the addition of domain-specific features.

Article Search Artifacts Available

Design Patterns for Parser Combinators (Functional Pearl)
Jamie Willis  and Nicolas Wu 
(Imperial College London, UK)
Parser combinators are a popular and elegant approach for parsing in functional languages. The design and implementation of such libraries are well discussed, but having a well-designed library is only one-half of the story. In this paper we explore several reusable approaches to writing parsers in combinator style, focusing on easy to apply patterns to keep parsing code simple, separated, and maintainable.

Article Search Artifacts Available

Seeking Stability by Being Lazy and Shallow: Lazy and Shallow Instantiation Is User Friendly
Gert-Jan Bottu  and Richard A. Eisenberg 
(KU Leuven, Belgium; Tweag, USA)
Designing a language feature often requires a choice between several, similarly expressive possibilities. Given that user studies are generally impractical, we propose using stability as a way of making such decisions. Stability is a measure of whether the meaning of a program alters under small, seemingly innocuous changes in the code (e.g., inlining).
Directly motivated by a need to pin down a feature in GHC/Haskell, we apply this notion of stability to analyse four approaches to the instantiation of polymorphic types, concluding that the most stable approach is lazy (instantiate a polytype only when absolutely necessary) and shallow (instantiate only top-level type variables, not variables that appear after explicit arguments).

Preprint

Express: Applications of Dynamically Typed Haskell Expressions
Rudy Matela
This paper presents Express, a library for manipulating dynamically typed Haskell expressions involving function application and variables. Express works as a wrapper around the Data.Dynamic module and provides additional features such as: explicit encoding of function applicaion thus delayed application between values, support for variable placeholders and expression matching. This paper shows these additions make this library useful in generating program specifications, automated testing and program synthesis.

Preprint Info

Chesskell: A Two-Player Game at the Type Level
Toby Bailey and Michael B. Gale 
(University of Warwick, UK)
Extensions to Haskell's type system, as implemented in GHC, have given developers more tools to express the domain-specific rules and invariants of their programs in types. For these extensions to see mainstream adoption, their use in complex applications has to be practical. We present Chesskell, an EDSL for describing Chess games where a type-level model of the full FIDE ruleset prevents us from expressing games with invalid moves. Our work highlights current limitations when using GHC to express such complex rules due to the resulting memory usage and compile times, which we report on. We further present some approaches for working around those limitations.

Article Search Info

Safe Mutation with Algebraic Effects
Hashan Punchihewa and Nicolas Wu 
(Imperial College London, UK)
It can be difficult to write safe concurrent programs which use shared mutable state. Subtle mistakes can lead to data races that manifest as unexpected program behaviour. The prevailing approaches to solving this dilemma are to either eschew mutable state altogether, or design bespoke languages that prevent data races by design. This article introduces a third approach by showing how safe mutation can be integrated into a mainstream functional programming language with algebraic effects. This article produces a framework that tracks the use of mutable state and guarantees data race freedom at compile time.

Article Search