ICFP Workshops 2020
25th ACM SIGPLAN International Conference on Functional Programming (ICFP 2020)
Powered by
Conference Publishing Consulting

25th ACM SIGPLAN International Conference on Functional Programming (ICFP 2020), August 23–28, 2020, Virtual Event, USA

ICFP Workshops 2020 – Proceedings

Contents - Abstracts - Authors

19th ACM SIGPLAN International Workshop on Erlang (Erlang 2020)

Frontmatter

Title Page


Message from the Chairs
It is our great pleasure to welcome you to the Nineteenth ACM SIGPLAN Erlang Workshop (Erlang’20), which is once again co-located with the annual International Conference on Functional Programming (ICFP), held as a virtual event this year. The workshop continues the tradition of being a forum for presenting research efforts and experience reports on all aspects of theory, implementation, and applications of the Erlang language and BEAM-related technologies, covering topics such as functional programming, distribution, concurrency, and scalability. The Erlang model of concurrent programming has been widely emulated, for example by Akka in Scala, Java and now Swift, and a wave of exciting programming languages are being developed on top of the Erlang VM (BEAM), such as Elixir or adaptations of Clojure.
The call for papers attracted this year a total of 8 submissions, each of which were carefully reviewed by at least four program committee members. To ensure fairness and preserve the anonymity of all authors and reviewers, papers authored by PC chairs were handled out-of-band by Natalia Chechina. The reviews were handled using the HotCRP system using "tokens", a mechanism designed to keep the reviewers anonymous even from the chairs. This year, a new initiative started to team up practitioners with experienced researchers to support them in writing their first research paper. One paper emerging from such a collaboration was submitted and also accepted for publication in the standard review process. In total, the program committee accepted four long and one short paper for publication.
Additionally, the steering committee invited the founders of Avassa for a panel discussion to talk about Erlang-fuelled inventions. The discussion will be led by Johnny Winn, who is also the host of the Elixir Fountain Podcast.
Putting together Erlang’20 has been a team effort. First of all, we thank the panellists and the authors of all submitted papers for allowing us to assemble an inspiring and appealing program. We express our gratitude to all members of the program committee, who reviewed the papers in a timely manner despite the situation due to COVID-19, providing constructive criticism and suggestions for improvement. We also greatly appreciate the efforts of this year’s ICFP Chairs, led by Stephanie Weirich as General Chair, and the workshop co-chairs, Jennifer Hackett and Leonidas Lampropoulos, who diligently answered our questions and guided us through the organisational process. Special thanks go to the virtualization committee of ICFP’20 for taking care of the online meeting arrangements: your hard work makes our experiences great. We would also like to thank the members of the Erlang Workshop’s Steering Committee for their guidance and to the Ericsson OTP team for maintaining the Erlang’20 web site. Finally, we thank ACM SIGPLAN for their continued support.
We hope that these proceedings will serve as a valuable reference for Erlang and BEAM-based language researchers, implementors, and practitioners, and that you will find this year’s program appealing and thought-provoking.

Papers

Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
Péter Bereczky, Dániel Horpácsi, and Simon J. Thompson
(Eötvös Loránd University, Hungary; University of Kent, UK)
This research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations of Erlang programs. In order to formally reason about the definition of a programming language and the software built using it, we need a mathematically rigorous description of that language.
In this paper, we present an extended natural semantics for Core Erlang based on our previous formalisation implemented with the Coq Proof Assistant. This extension includes the concepts of exceptions and side effects, moreover, some modifications and updates are also discussed. Then we describe theorems about the properties of this formalisation (e.g. determinism), formal expression evaluation and equivalence examples. These equivalences can be interpreted as simple local refactorings.

Publisher's Version Article Search
Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+
Peter Zeller, Annette Bieniusa, and Carla Ferreira
(TU Kaiserslautern, Germany; Nova University of Lisbon, Portugal)
Distributed systems are inherently complex as they need to address the interplay between features like communication, concurrency, and failure. Due to the inherent complexity of these interacting features, it is typically not possible to systematically test these kind of systems; yet, unexpected and unlikely combinations of events might cause corner cases that are hard to find. But since these systems are running typically for long durations, these events are likely to materialize eventually and must be handled correctly. Caught in such a dilemma, students are able to experience the benefits of applying verification tools to check their own algorithms and implementations. Having executable models with automatically generated executions allows them to experiment with different solutions by iteratively adapting and refining their algorithms.
In this experience report, we report on our experience of teaching verification in a (hands-on) distributed systems course. We argue that broadcast algorithms provide a sweet spot in design and verification complexity. To this end, we give an implementation of these algorithms in Erlang and derive a TLA+ specification. TLA+ is a formal language for describing and reasoning about distributed and concurrent systems and provides a model checker, TLC, among other things. Our study reveals interesting parallels between the Erlang and TLA+ code, while exposing the challenges of formally modeling communication and parallelism in distributed systems. Presenting selected aspects of our course design, we aim to motivate the feasibility and need for introducing verification in close correspondence to programming tasks.

Publisher's Version Article Search
Transformations towards Clean Functional Code
Boldizsár Poór, Melinda Toth, and István Bozó
(Eötvös Loránd University, Hungary)
The programming style has an impact on the readability and comprehensibility of the source code, and it may also affect run-time performance. This statement also holds for functional languages when the functional style is mixed with imperative design. In this paper, we present a couple of methods that can refactor imperatively styled Erlang source-code into a more functionally styled one. This can be done by transforming unnecessary calls to length, hd and tl into pattern matching or by lifting particular nested expressions. The results of our investigations indicate that these refactorings can not only shorten the length of the source code but also affect the complexity/readability. In this paper, we present some refactorings; moreover, real-life examples and data for its validation.

Publisher's Version Article Search
Secure Design and Verification of Erlang Systems
Viktória Fördős
(Cisco Systems, Sweden)
Security is a critical part of software development, companies have the utmost responsibility to protect their customers data against any threat. Secure design is a key enabler, since it cultivates security awareness in software projects from day zero. In this paper it is shown how to apply the principles of secure design to Erlang software projects. An Erlang specific method to identify trust zones is presented. The high risk vulnerabilities of the Erlang ecosystem are reviewed and grouped together using the CIA triad model. A dataflow based static analysis together with a prototype to verify security posture of a trust zone are introduced and evaluated using Riak Core as a case study.

Publisher's Version Article Search
Clojerl: The Expressive Power of Clojure on the BEAM
Juan Facorro and Natalia Chechina
(Bournemouth University, UK)
The development of new features and approaches in programming languages is a continuous and never-ending task, as languages are ultimately tools for expressing and solving problems. The past decade has seen a surge in languages implemented for the BEAM as part of a search to combine the fault-tolerance and scalability of the BEAM with a set of desired language features.
In this paper we present Clojerl, an implementation of the Clojure language with a rich set of data processing capabilities and the expressive power of Lisp for the BEAM. The main design principles of Clojerl are to provide (1) seamless interoperability with the BEAM to enable frictionless interaction with other BEAM languages and (2) portability with Clojure to enable existing Clojure code to run on the BEAM with little or no modifications. We evaluate Clojerl by running a set of experiments that analyse the performance of eight most widely used expressions. While the results of complex expressions show that Clojerl requires further optimisations, Clojerl significantly outperforms Clojure in a set of basic expressions, confirming that Clojerl has the potential to provide a competitive performance while offering a rich set of programming language features.

Publisher's Version Article Search

Frontmatter

Title Page


Message from the Chairs


Committees


Sponsors



13th ACM SIGPLAN International Haskell Symposium (Haskell 2020)

Frontmatter

Title Page


Welcome from the Chair
Welcome to the 13th 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 is held online on 27–28 August 2020, co-located with ICFP 2020.

Experience Reports

Describing Microservices using Modern Haskell (Experience Report)
Alejandro Serrano and Flavio Corpa
(47 Degrees, Spain)
We present Mu, a domain specific language to describe and develop microservices in Haskell. At its core, Mu provides a type level representation of schemas, which we leverage in various ways. These schemas can be automatically imported from industry-standard interface definition languages.
Mu uses many of the type level extensions to GHC, and techniques such as (data type) generic programming and attribute grammars. Apart from the description of the library, we discuss a series of shortcomings in current GHC/Haskell, mostly related to the friendliness of the exposed library interface once complex types enter the scene.

Publisher's Version Article Search
Eliminating Bugs with Dependent Haskell (Experience Report)
Noam Zilberstein
(Facebook, USA)
Using dependent types in production code is a practical way to eliminate errors. While there are many examples of using dependent Haskell to prove invariants about code, few of these are applied to large scale production systems. Critics claim that dependent types are only useful in toy examples and that they are impractical for use in the real world. This experience report analyzes real world examples where dependent types have enabled us to find and eliminate bugs in production Haskell code.

Publisher's Version Article Search

Functional Pearls

A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)
Andrej Ivašković and Alan Mycroft
(University of Cambridge, UK)
We present a new type-oriented framework for writing shared memory multithreaded programs that the Haskell type system guarantees are deadlock-free. The implementation wraps all concurrent computation inside a graded monad and assumes a total order is defined between locks. The grades within the type of such a computation specify which locks it acquires and releases. This information is drawn from an algebra that ensures that types can, in principle, be inferred in polynomial time.

Publisher's Version Article Search
Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)
Koen Claessen
(Chalmers University of Technology, Sweden)
We explicitly motivate the subtle intricacies of Hinze and Paterson's Finger Tree datastructure, by step-wise refining a naive implementation. The result is a new explanation of how Finger Trees work and why they have the particular structure they have, and also a small simplification of the original implementation.

Publisher's Version Article Search
Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
Richard A. Eisenberg
(Tweag I/O, France; Bryn Mawr College, USA)
A classic example of the power of generalized algebraic datatypes (GADTs) to verify a delicate implementation is the type-indexed expression AST. This functional pearl refreshes this example, casting it in modern Haskell using many of GHC's bells and whistles. The Stitch interpreter is a full executable interpreter, with a parser, type checker, common-subexpression elimination, and a REPL. Making heavy use of GADTs and type indices, the Stitch implementation is clean Haskell code and serves as an existence proof that Haskell's type system is advanced enough for the use of fancy types in a practical setting. The paper focuses on guiding the reader through these advanced topics, enabling them to adopt the techniques demonstrated here.

Publisher's Version Article Search Artifacts Available
Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)
Armando Santos and José N. Oliveira
(University of Minho, Portugal; INESC TEC, Portugal)
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory.

Publisher's Version Article Search Artifacts Available

Research Papers

Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality
Sander Kamps, Bastiaan Heeren, and Johan Jeuring
(Open University of the Netherlands, Netherlands)
Software metrics are used to measure the quality of a software system, and to understand the evolution of the system's quality over time. In this paper we report on an empirical study that investigates whether structural degradation in Haskell systems is related to decreasing software quality. For our study we use three metrics that measure internal attributes at the level of Haskell modules: intra-modular complexity (cohesion), inter-modular complexity (coupling), and module size. For these metrics, we calculate the Gini coefficient, which is a measure of the inequality in a distribution of values within a certain population, and the deviation of the population's central tendency from an empirically established ideal value. We develop a method to track the evolution, and measure the correlation between the calculated system-level information and post-release defects.
The results show that: (1) post-release defects are significantly correlated with the degree of inequality between the size of modules, (2) the inequality measure is able to indicate significant structural shifts in Haskell source code, and (3) the deviation of a population's central tendency from an ideal value can serve as a benchmark to evaluate the structural characteristics of a Haskell system. The results, however, do not show that a combined measure for inequality and ideal value deviation increases the ability to indicate the defect proneness of Haskell source code.

Publisher's Version Article Search Artifacts Available
Composing Effects into Tasks and Workflows
Yves Parès, Jean-Philippe Bernardy, and Richard A. Eisenberg
(Tweag I/O, France; University of Gothenburg, Sweden; Bryn Mawr College, USA)
Data science applications tend to be built by composing tasks: discrete manipulations of data. These tasks are arranged in directed acyclic graphs, and many frameworks exist within the data science community supporting such a structure, which is called a workflow. In realistic applications, we want to be able to both analyze a workflow in the absence of data, and to execute the workflow with data.
This paper combines effect handlers with arrow-like structures to abstract out data science tasks. This combination of techniques enables a modular design of workflows. Additionally, these workflows can both be analyzed prior to running (e.g., to provide early failure) and run conveniently. Our work is directly motivated by real-world scenarios, and we believe that our approach is applicable to new data science and machine learning applications and frameworks.

Publisher's Version Article Search Artifacts Available
Effect Handlers in Haskell, Evidently
Ningning Xie and Daan Leijen
(Microsoft Research, USA)
Algebraic effect handlers offer an alternative to monads to incorporate effects in Haskell. In recent work Xie _et al._ show how to give semantics to effect handlers in terms of plain polymorphic lambda calculus through _evidence translation_. Besides giving precise semantics, this translation also allows for potentially more efficient implementations. Here we present the first implementation of this technique as a library for effect handlers in Haskell. We show how the design naturally leads to a concise effect interface and how evidence translation enables evaluating _tail resumptive_ operations _in-place_. We give detailed benchmark results where our library performs well with respect to other approaches.

Publisher's Version Article Search Artifacts Available
Scripted Signal Functions
David A. Stuart
Programming time-dependent signals like animations involves expressing both continuous and discrete changes in signal values. The method of functional reactive programming (FRP) represents this simply and effectively as discrete modes of an otherwise continuous signal. In variants of FRP based on arrows, programs are composed not of signals but rather functions on signals. Accordingly, these signal functions can switch between discrete modes of operation. However, the literature emphasizes expressions of mode switching that are unnecessarily limited. An analysis of their limitations indicates the need for two new, primitive transformations of signal functions. These transformations help to define a monad that represents signal function modes, and this allows programmers to express switching in an imperative, script-like style. This scripting interface gains flexibility and power from several novel operations, including a general-purpose mapping between modes and a combination that mixes two concurrent modes into one. We demonstrate its usefulness with several examples.

Publisher's Version Article Search
Staged Sums of Products
Matthew Pickering, Andres Löh, and Nicolas Wu
(University of Bristol, UK; Well-Typed LLP, UK; Imperial College London, UK)
Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.

Publisher's Version Article Search
Towards Secure IoT Programming in Haskell
Nachiappan Valliappan, Robert Krook, Alejandro Russo, and Koen Claessen
(Chalmers University of Technology, Sweden)
IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language in Haskell (eDSL) for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C’s pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern-matching in Haskell to write Haski programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on Zephyr OS.

Publisher's Version Article Search Artifacts Available

5th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2020)

Frontmatter

Title Page


Welcome from the Chairs
Welcome to the 5th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe'20), co-located with the International Conference on Functional Programming (ICFP 2020). The workshop aims to show how static type information may be used effectively in the development of computer programs.
TyDe is a merging of two previous workshops: the Workshop on Dependently Typed Programming and the Workshop on Generic Programming. These two research areas have a rich history and bridge both theory and practice. Novel techniques explored by both communities have gradually spread to more mainstream languages. This workshop aims to bring together leading researchers and practitioners in generic programming and dependently typed programming from around the world, and features contributions capturing the state of the art in these important areas.
The call for submissions sought both full papers (up to 12 pages, published in the ACM Digital Library) and extended abstracts (up to 2 pages, not formally published but posted on the workshop webpage). Each submission was evaluated by at least three members of the program committee: full papers for the novelty and significance of their results, and extended abstracts for relevance and interest to the TyDe community. We received 4 full papers and 7 extended abstracts, of which 2 and 7 respectively were accepted. The submission period overlapped substantially with the beginning of the COVID-19 pandemic, which likely contributed to a lower normal number of submissions compared to previous years. Nevertheless, the submissions that we received presented fascinating new ideas and results and we are pleased to be able to put together an excellent online program.

Papers

Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas Reynolds, William L. Harrison, Rohit Chadha, and Gerard Allwein
(University of Missouri, USA; Oak Ridge National Laboratory, USA; US Naval Research Laboratory, USA)
Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly-bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed λ-calculus called the bounded-time λ-calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well.

Publisher's Version Article Search
Practical Dependent Type Checking using Twin Types
Víctor López Juan and Nils Anders Danielsson
(Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
People writing proofs or programs in dependently typed languages can omit some function arguments in order to decrease the code size and improve readability. Type checking such a program involves filling in each of these implicit arguments in a type-correct way. This is typically done using some form of unification.
One approach to unification, taken by Agda, involves sometimes starting to unify terms before their types are known to be equal: in some cases one can make progress on unifying the terms, and then use information gleaned in this way to unify the types. This flexibility allows Agda to solve implicit arguments that are not found by several other systems. However, Agda's implementation is buggy: sometimes the solutions chosen are ill-typed, which can cause the type checker to crash.
With Gundry and McBride's twin variable technique one can also start to unify terms before their types are known to be equal, and furthermore this technique is accompanied by correctness proofs. However, so far this technique has not been tested in practice as part of a full type checker.
We have reformulated Gundry and McBride's technique without twin variables, using only twin types, with the aim of making the technique easier to implement in existing type checkers (in particular Agda). We have also introduced a type-agnostic syntactic equality rule that seems to be useful in practice. The reformulated technique has been tested in a type checker for a tiny variant of Agda. This type checker handles at least one example that Coq, Idris, Lean and Matita cannot handle, and does so in time and space comparable to that used by Agda. This suggests that the reformulated technique is usable in practice.

Publisher's Version Article Search

proc time: 4.4