ICFP Workshops 2023
28th ACM SIGPLAN International Conference on Functional Programming (ICFP 2023)

Title Page

Welcome from the Chairs
This is the prelude of the 16th ACM SIGPLAN Haskell Symposium, which was held on 8-9 September 2023 in Seattle, Washington, United States, co-located with ICFP 2023.

Haskell 2023 Organization
Haskell Symposium 2023 Program Committee

Haskell for Choice-Based Learning (Keynote)
Ningning Xie 
(Google DeepMind, Canada; University of Toronto, Canada)
Machine learning has achieved many successes during the past decades, spanning domains of game-playing, protein folding, competitive programming, and many others. However, while there have been major efforts in building programming techniques and frameworks for machine learning programming, there has been very little study of general language design for machine learning programming.
We pursue such a study in this talk, focusing on choice-based learning, particularly where choices are driven by optimizations. This includes widely-used decision-making models and techniques (e.g., Markov decision processes or gradient descent) which provide frameworks for describing systems in terms of choices (e.g., actions or parameters) and their resulting feedback as losses (dually, rewards).
We propose and give evidence for the following thesis: languages for choice-based learning can be obtained by combining two paradigms, algebraic effects and handlers, and the selection monad. We provide a prototype implementation as a Haskell library and present a variety of programming examples for choice-based learning: stochastic gradient descent, hyperparameter tuning, generative adversarial networks, and reinforcement learning.

@InProceedings{Haskell23p1, author = {Ningning Xie}, title = {Haskell for Choice-Based Learning (Keynote)}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {1--1}, doi = {10.1145/3609026.3615580}, year = {2023}, } Publisher's Version

The Evolution of Effects (Keynote)
Nicolas Wu 
(Imperial College London, UK)
Functional programming has been celebrated for its promise of pure functions, delivering referential transparency and elegant reasoning about programs. However, real-world applications are not pure, and necessitate interaction with the outside world, introducing computational effects such as IO, state, and exceptions. The journey to harmonize these seemingly contradictory paradigms has led to a fascinating evolution of effectful programming in Haskell.
The introduction of monads as a practical programming tool was a pivotal discovery, enabling controlled sequencing of effectful computations and addressing the challenge of handling side effects in a pure language. However, it soon became evident that the lack of modularity in composing effects using monads posed a limitation to effectful programming. To overcome this obstacle, monad transformers emerged as a solution, providing a composable manner of building effects on top of one another.
More recent advancements have led to algebraic effects as an alternative framework that is easy to extend, particularly as domain-specific languages crafted to work in specific contexts. Nevertheless, these effects are not without quirks and limitations, leading to the development of higher-order effects. These higher-order effects extend the capabilities of algebraic effects, providing greater flexibility for expressing effectful computations, while also shedding light on the connection between the monad approach and the algebraic approach to effects.
This talk will survey the historical milestones that have shaped the landscape of effectful programming in Haskell, exploring the transition from monads to monad transformers and the emergence of algebraic and higher-order effects.

@InProceedings{Haskell23p2, author = {Nicolas Wu}, title = {The Evolution of Effects (Keynote)}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {2--2}, doi = {10.1145/3609026.3615581}, year = {2023}, } Publisher's Version

This Is Driving Me Loopy: Efficient Loops in Arrowized Functional Reactive Programs
Finnbar Keating  and Michael B. Gale 
(University of Warwick, UK; GitHub, UK)
Arrowized Functional Reactive Programming (AFRP) is one approach to writing reactive programs declaratively, based on the arrows abstraction in Haskell. While AFRP elegantly expresses the relationships between inputs and outputs of a reactive system, na'ive implementations suffer from poor performance. In particular, the loop combinator depends on lazy semantics: this inflicts the overheads of lazy evaluation and simultaneously prevents existing optimisation techniques from being applied to it.
We present a novel program transformation which utilises the Arrow and ArrowLoop laws to transform typical uses of loop into restricted forms that have an execution order that is known at compile-time and therefore can be executed strictly. We evaluate the performance gained from our transformations and prove that the transformations are correct.

@InProceedings{Haskell23p3, author = {Finnbar Keating and Michael B. Gale}, title = {This Is Driving Me Loopy: Efficient Loops in Arrowized Functional Reactive Programs}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {3--17}, doi = {10.1145/3609026.3609726}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available

The Essence of Reactivity
Ivan Perez  and Frank Dedden 
(KBR @ NASA Ames Research Center, USA; System F Computing, Netherlands)
Reactive programming, functional reactive programming, event-based programming, stream programming, and temporal logic all share an underlying commonality: values can vary over time. These languages differ in multiple ways, including the nature of time itself (e.g., continuous or discrete, dense or sparse, implicit or explicit), on how much of the past and future can be referenced, on the kinds of values that can be represented, as well as the mechanisms used to evaluate expressions or formulas. This paper presents a series of abstractions that capture the essence of different forms of time variance. By separating the aspects that differentiate each family of formalisms, we can better express the commonalities and differences between them. We demonstrate our work with a prototype in Haskell that allows us to write programs in terms of a generic interface that can be later instantiated to different abstractions depending on the desired target.

@InProceedings{Haskell23p18, author = {Ivan Perez and Frank Dedden}, title = {The Essence of Reactivity}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {18--31}, doi = {10.1145/3609026.3609727}, year = {2023}, } Publisher's Version

An Exceptional Actor System (Functional Pearl)
Patrick Redmond  and Lindsey Kuper 
(University of California at Santa Cruz, USA)
The Glasgow Haskell Compiler is known for its feature-laden runtime system (RTS), which includes lightweight threads, asynchronous exceptions, and a slew of other features. Their combination is powerful enough that a programmer may complete the same task in many different ways --- some more advisable than others.
We present a user-accessible actor framework hidden in plain sight within the RTS and demonstrate it on a classic example from the distributed systems literature. We then extend both the framework and example to the realm of dynamic types. Finally, we raise questions about how RTS features intersect and possibly subsume one another, and suggest that GHC can guide good practice by constraining the use of some features.

@InProceedings{Haskell23p32, author = {Patrick Redmond and Lindsey Kuper}, title = {An Exceptional Actor System (Functional Pearl)}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {32--43}, doi = {10.1145/3609026.3609728}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available

Effect Handlers for Programmable Inference
Minh Nguyen , Roly Perera , Meng Wang , and Steven Ramsay 
(University of Bristol, UK)
Inference algorithms for probabilistic programming are complex imperative programs with many moving parts. Efficient inference often requires customising an algorithm to a particular probabilistic model or problem, sometimes called inference programming. Most inference frameworks are implemented in languages that lack a disciplined approach to side effects, which can result in monolithic implementations where the structure of the algorithms is obscured and inference programming is hard. Functional programming with typed effects offers a more structured and modular foundation for programmable inference, with monad transformers being the primary structuring mechanism explored to date.
This paper presents an alternative approach to inference programming based on algebraic effects. Using effect signatures to specify the key operations of the algorithms, and effect handlers to modularly interpret those operations for specific variants, we develop two abstract algorithms, or inference patterns, representing two important classes of inference: Metropolis-Hastings and particle filtering. We show how our approach reveals the algorithms’ high-level structure, and makes it easy to tailor and recombine their parts into new variants. We implement the two inference patterns as a Haskell library, and discuss the pros and cons of algebraic effects vis-à-vis monad transformers as a structuring mechanism for modular imperative algorithm design.

@InProceedings{Haskell23p44, author = {Minh Nguyen and Roly Perera and Meng Wang and Steven Ramsay}, title = {Effect Handlers for Programmable Inference}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {44--58}, doi = {10.1145/3609026.3609729}, year = {2023}, } Publisher's Version

Don’t Go Down the Rabbit Hole: Reprioritizing Enumeration for Property-Based Testing
Segev Elazar Mittelman , Aviel Resnick , Ivan Perez , Alwyn E. Goodloe , and Leonidas Lampropoulos 
(University of Maryland at College Park, USA; University of Pennsylvania, USA; KBR @ NASA Ames Research Center, USA; NASA Langley Research Center, USA)
In our implementation, we integrate a state-of-the-art enumeration-based property-based testing framework, LazySearch, with a state-of-the-art combinatorial testing tool, NIST’s ACTS, and demonstrate how it can significantly speed up the effectiveness of testing—up to more than 20× in the case of a prior System F case study from the literature.

@InProceedings{Haskell23p59, author = {Segev Elazar Mittelman and Aviel Resnick and Ivan Perez and Alwyn E. Goodloe and Leonidas Lampropoulos}, title = {Don’t Go Down the Rabbit Hole: Reprioritizing Enumeration for Property-Based Testing}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {59--71}, doi = {10.1145/3609026.3609730}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available

HasTEE: Programming Trusted Execution Environments with Haskell
Abhiroop Sarkar , Robert Krook , Alejandro Russo , and Koen Claessen 
(Chalmers University of Technology, Sweden)
Trusted Execution Environments (TEEs) are hardware enforced memory isolation units, emerging as a pivotal security solution for security-critical applications. TEEs, like Intel SGX and ARM TrustZone, allow the isolation of confidential code and data within an untrusted host environment, such as the cloud and IoT. Despite strong security guarantees, TEE adoption has been hindered by an awkward programming model. This model requires manual application partitioning and the use of error-prone, memory-unsafe, and potentially information-leaking low-level C/C++ libraries.
We address the above with HasTEE, a domain-specific language (DSL) embedded in Haskell for programming TEE applications. HasTEE includes a port of the GHC runtime for the Intel-SGX TEE.HasTEE uses Haskell’s type system to automatically partition an application and to enforce Information Flow Control on confidential data. The DSL, being embedded in Haskell, allows for the usage of higher-order functions, monads, and a restricted set of I/O operations to write any standard Haskell application. Contrary to previous work, HasTEE is lightweight, simple, and is provided as a simple security library; thus avoiding any GHC modifications. We show the applicability of HasTEE by implementing case studies on federated learning, an encrypted password wallet, and a differentially-private data clean room.

@InProceedings{Haskell23p72, author = {Abhiroop Sarkar and Robert Krook and Alejandro Russo and Koen Claessen}, title = {HasTEE: Programming Trusted Execution Environments with Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {72--88}, doi = {10.1145/3609026.3609731}, year = {2023}, } Publisher's Version Published Artifact Artifacts Available

Haskell Library for Safer Virtual Machine Introspection (Experience Report)
Takato Otsuka  and Hideya Iwasaki 
(University of Electro-Communications, Japan; Meiji University, Japan)
Virtual machine introspection (VMI) is a technique for inspecting a virtual machine from the outside, typically to analyze the operating system (guest OS) running on it. LibVMI is a C library for VMI and provides APIs for accessing guest OS's memory. However, in using LibVMI APIs directly in C, the programmer must compute target addresses in the kernel memory and then access them with their exact bit widths and types. This is an enormous burden for the programmer and is prone to introducing statically undetected but fatal errors. We create HaVMI, a Haskell library that facilitates VMI programming. HaVMI provides meta-functions for compile-time code generation by Template Haskell. These meta-functions make it easy to write safer VMI programs. HaVMI uses Haskell language features to detect the programmer's errors statically.

@InProceedings{Haskell23p89, author = {Takato Otsuka and Hideya Iwasaki}, title = {Haskell Library for Safer Virtual Machine Introspection (Experience Report)}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {89--96}, doi = {10.1145/3609026.3609732}, year = {2023}, } Publisher's Version

falsify: Internal Shrinking Reimagined for Haskell
Edsko de Vries 
(Well-Typed LLP, UK)
In unit testing we apply the function under test to known inputs and check for known outputs. By contrast, in property based testing we state properties relating inputs and outputs, apply the function to random inputs, and verify that the property holds; if not, we found a bug. Randomly generated inputs tend to be large and should therefore be minimised. Traditionally this is done with an explicitly provided shrinker, but in this paper we propose a way to write generators that obsoletes the need to write a separate shrinker. Inspired by the Python library Hypothesis, the approach can work even across monadic bind. Compared to Hypothesis, our approach is more suitable to the Haskell setting: it depends on a minimal set of core principles, and handles generation and shrinking of infinite data structures, including functions.

@InProceedings{Haskell23p97, author = {Edsko de Vries}, title = {falsify: Internal Shrinking Reimagined for Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {97--109}, doi = {10.1145/3609026.3609733}, year = {2023}, } Publisher's Version