Workshop Haskell 2019 – Author Index 
Contents 
Abstracts 
Authors

A B C D E F G H J K L M N P R S W X
Adam, Justus 
Haskell '19: "STCLang: State Thread Composition ..."
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism
Sebastian Ertel, Justus Adam, Norman A. Rink, Andrés Goens, and Jeronimo Castrillon (Huawei Technologies, Germany; TU Dresden, Germany) Dataflow execution models are used to build highly scalable parallel systems. A programming model that targets parallel dataflow execution must answer the following question: How can parallelism between two dependent nodes in a dataflow graph be exploited? This is difficult when the dataflow language or programming model is implemented by a monad, as is common in the functional community, since expressing dependence between nodes by a monadic bind suggests sequential execution. Even in monadic constructs that explicitly separate state from computation, problems arise due to the need to reason about opaquely defined state. Specifically, when abstractions of the chosen programming model do not enable adequate reasoning about state, it is difficult to detect parallelism between composed stateful computations. In this paper, we propose a programming model that enables the composition of stateful computations and still exposes opportunities for parallelization. We also introduce smap, a higherorder function that can exploit parallelism in stateful computations. We present an implementation of our programming model and smap in Haskell and show that basic concepts from functional reactive programming can be built on top of our programming model with little effort. We compare these implementations to a stateoftheart approach using monadpar and LVars to expose parallelism explicitly and reach the same level of performance, showing that our programming model successfully extracts parallelism that is present in an algorithm. Further evaluation shows that smap is expressive enough to implement parallel reductions and our programming model resolves shortcomings of the streambased programming model for current stateoftheart big data processing systems. Article Search Info 

Ariola, Zena M. 
Haskell '19: "Making a Faster Curry with ..."
Making a Faster Curry with Extensional Types
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones (University of Oregon, USA; Microsoft Research, UK) Curried functions apparently take one argument at a time, which is slow. So optimizing compilers for higherorder languages invariably have some mechanism for working around currying by passing several arguments at once, as many as the function can handle, which is known as its arity. But such mechanisms are often adhoc, and do not work at all in higherorder functions. We show how extensional, callbyname functions have the correct behavior for directly expressing the arity of curried functions. And these extensional functions can stand sidebyside with functions native to practical programming languages, which do not use callbyname evaluation. Integrating callbyname with other evaluation strategies in the same intermediate language expresses the arity of a function in its type and gives a principled and compositional account of multiargument curried functions. An unexpected, but significant, bonus is that our approach is equally suitable for a callbyvalue language and a callbyneed language, and it can be readily integrated into an existing compilation framework. Article Search 

Bunkenburg, Niels 
Haskell '19: "Verifying Effectful Haskell ..."
Verifying Effectful Haskell Programs in Coq
Jan Christiansen, Sandra Dylus, and Niels Bunkenburg (Flensburg University of Applied Sciences, Germany; University of Kiel, Germany) We show how various Haskell language features that are related to ambient effects can be modeled in Coq. For this purpose we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad results in nonstrictly positive types when transforming recursive data types likes lists. Such nonstrictly positive types are not accepted by Coq's termination checker. Therefore, instead of a model that is generic over any monad, the approach we build on uses a specific monad instance, namely the free monad in combination with containers, to model various kinds of effects. This model allows effectgeneric proofs. In this paper we consider ambient effects that may occur in Haskell, namely partiality, errors, and tracing, in detail. We observe that, while proving propositions that hold for all kinds of effects is attractive, not all propositions of interest hold for all kinds of effects. Some propositions fail for certain effects because the usual monadic translation models callbyname and not callbyneed. Since modeling the evaluation semantics of callbyneed in the presence of effects like partiality is complex and not necessary to prove propositions for a variety of effects, we identify a specific class of effects for which we cannot observe a difference between callbyname and callbyneed. Using this class of effects we can prove propositions for all effects that do not require a model of sharing. Article Search 

Castrillon, Jeronimo 
Haskell '19: "STCLang: State Thread Composition ..."
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism
Sebastian Ertel, Justus Adam, Norman A. Rink, Andrés Goens, and Jeronimo Castrillon (Huawei Technologies, Germany; TU Dresden, Germany) Dataflow execution models are used to build highly scalable parallel systems. A programming model that targets parallel dataflow execution must answer the following question: How can parallelism between two dependent nodes in a dataflow graph be exploited? This is difficult when the dataflow language or programming model is implemented by a monad, as is common in the functional community, since expressing dependence between nodes by a monadic bind suggests sequential execution. Even in monadic constructs that explicitly separate state from computation, problems arise due to the need to reason about opaquely defined state. Specifically, when abstractions of the chosen programming model do not enable adequate reasoning about state, it is difficult to detect parallelism between composed stateful computations. In this paper, we propose a programming model that enables the composition of stateful computations and still exposes opportunities for parallelization. We also introduce smap, a higherorder function that can exploit parallelism in stateful computations. We present an implementation of our programming model and smap in Haskell and show that basic concepts from functional reactive programming can be built on top of our programming model with little effort. We compare these implementations to a stateoftheart approach using monadpar and LVars to expose parallelism explicitly and reach the same level of performance, showing that our programming model successfully extracts parallelism that is present in an algorithm. Further evaluation shows that smap is expressive enough to implement parallel reductions and our programming model resolves shortcomings of the streambased programming model for current stateoftheart big data processing systems. Article Search Info 

Christiansen, Jan 
Haskell '19: "Verifying Effectful Haskell ..."
Verifying Effectful Haskell Programs in Coq
Jan Christiansen, Sandra Dylus, and Niels Bunkenburg (Flensburg University of Applied Sciences, Germany; University of Kiel, Germany) We show how various Haskell language features that are related to ambient effects can be modeled in Coq. For this purpose we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad results in nonstrictly positive types when transforming recursive data types likes lists. Such nonstrictly positive types are not accepted by Coq's termination checker. Therefore, instead of a model that is generic over any monad, the approach we build on uses a specific monad instance, namely the free monad in combination with containers, to model various kinds of effects. This model allows effectgeneric proofs. In this paper we consider ambient effects that may occur in Haskell, namely partiality, errors, and tracing, in detail. We observe that, while proving propositions that hold for all kinds of effects is attractive, not all propositions of interest hold for all kinds of effects. Some propositions fail for certain effects because the usual monadic translation models callbyname and not callbyneed. Since modeling the evaluation semantics of callbyneed in the presence of effects like partiality is complex and not necessary to prove propositions for a variety of effects, we identify a specific class of effects for which we cannot observe a difference between callbyname and callbyneed. Using this class of effects we can prove propositions for all effects that do not require a model of sharing. Article Search 

Derhaeg, Michiel 
Haskell '19: "Bidirectional Type Class Instances ..."
Bidirectional Type Class Instances
Koen Pauwels, Georgios Karachalias, Michiel Derhaeg, and Tom Schrijvers (KU Leuven, Belgium; Guardsquare, n.n.) GADTs were introduced in Haskell’s ecosystem more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be surprisingly difficult to provide an instance for even the simplest of type classes. In this paper we identify the source of this shortcoming and address it by introducing a conservative extension to Haskell’s type classes: Bidirectional Type Class Instances. In essence, under our interpretation class instances correspond to logical biimplications, in contrast to their traditional unidirectional interpretation. We present a fullyfledged design of bidirectional instances, covering the specification of typing and elaboration into System FC, as well as an algorithm for type inference and elaboration. We provide a proofofconcept implementation of our algorithm, and revisit the metatheory of type classes in the presence of our extension. Article Search 

Devriese, Dominique 
Haskell '19: "Modular Effects in Haskell ..."
Modular Effects in Haskell through Effect Polymorphism and Explicit Dictionary Applications: A New Approach and the μVeriFast Verifier as a Case Study
Dominique Devriese (Vrije Universiteit Brussel, Belgium) In applications with a complex structure of side effects, effects should be dealt with modularly: components should be programmed against abstract effect interfaces that other components can instantiate as required, and reusable effect patterns should be factored out from the rest of the application. In this paper, we study a new, general approach to achieve this in Haskell by combining effect polymorphism and the recently proposed coherent explicit dictionary applications. We demonstrate the elegance and generality of our approach in μVeriFast: a Haskellbased reimplementation of the semiautomatic separationlogicbased verification tool VeriFast. This implementation features a complex interplay of advanced side effects: a backtracking search of program paths with angelic and demonic nondeterminism, interaction with an underlying offtheshelf SMT solver, and mutable state that is either backtracked or not during the search. Our use of effect polymorphism improves over the current nonmodular implementation of VeriFast, allows us to nicely factor out the backtracking search pattern as a new AssumeAssert monad, and enables advanced features involving effects, such as the nonintrusive addition of a graphical symbolic debugger based on delimited continuations. Article Search Artifacts Available 

Downen, Paul 
Haskell '19: "Making a Faster Curry with ..."
Making a Faster Curry with Extensional Types
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones (University of Oregon, USA; Microsoft Research, UK) Curried functions apparently take one argument at a time, which is slow. So optimizing compilers for higherorder languages invariably have some mechanism for working around currying by passing several arguments at once, as many as the function can handle, which is known as its arity. But such mechanisms are often adhoc, and do not work at all in higherorder functions. We show how extensional, callbyname functions have the correct behavior for directly expressing the arity of curried functions. And these extensional functions can stand sidebyside with functions native to practical programming languages, which do not use callbyname evaluation. Integrating callbyname with other evaluation strategies in the same intermediate language expresses the arity of a function in its type and gives a principled and compositional account of multiargument curried functions. An unexpected, but significant, bonus is that our approach is equally suitable for a callbyvalue language and a callbyneed language, and it can be readily integrated into an existing compilation framework. Article Search 

Dylus, Sandra 
Haskell '19: "Verifying Effectful Haskell ..."
Verifying Effectful Haskell Programs in Coq
Jan Christiansen, Sandra Dylus, and Niels Bunkenburg (Flensburg University of Applied Sciences, Germany; University of Kiel, Germany) We show how various Haskell language features that are related to ambient effects can be modeled in Coq. For this purpose we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad results in nonstrictly positive types when transforming recursive data types likes lists. Such nonstrictly positive types are not accepted by Coq's termination checker. Therefore, instead of a model that is generic over any monad, the approach we build on uses a specific monad instance, namely the free monad in combination with containers, to model various kinds of effects. This model allows effectgeneric proofs. In this paper we consider ambient effects that may occur in Haskell, namely partiality, errors, and tracing, in detail. We observe that, while proving propositions that hold for all kinds of effects is attractive, not all propositions of interest hold for all kinds of effects. Some propositions fail for certain effects because the usual monadic translation models callbyname and not callbyneed. Since modeling the evaluation semantics of callbyneed in the presence of effects like partiality is complex and not necessary to prove propositions for a variety of effects, we identify a specific class of effects for which we cannot observe a difference between callbyname and callbyneed. Using this class of effects we can prove propositions for all effects that do not require a model of sharing. Article Search 

Ekblad, Anton 
Haskell '19: "Scoping Monadic Relational ..."
Scoping Monadic Relational Database Queries
Anton Ekblad (Chalmers University of Technology, Sweden) We present a novel method for ensuring that relational database queries in monadic embedded languages are wellscoped, even in the presence of arbitrarily nested joins and aggregates. Demonstrating our method, we present a simplified version of Selda, a monadic relational database query language embedded in Haskell, with full support for nested inner queries. To our knowledge, Selda is the first relational database query language to support fully general inner queries using a monadic interface. In the Haskell community, monads are the de facto standard interface to a wide range of libraries and EDSLs. They are well understood by researchers and practitioners alike, and they enjoy first class support by the standard libraries. Due to the difficulty of ensuring that inner queries are wellscoped, database interfaces in Haskell have previously either been forced to forego the benefits of monadic interfaces, or have had to do without the generality afforded by inner queries. Article Search 

Ertel, Sebastian 
Haskell '19: "STCLang: State Thread Composition ..."
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism
Sebastian Ertel, Justus Adam, Norman A. Rink, Andrés Goens, and Jeronimo Castrillon (Huawei Technologies, Germany; TU Dresden, Germany) Dataflow execution models are used to build highly scalable parallel systems. A programming model that targets parallel dataflow execution must answer the following question: How can parallelism between two dependent nodes in a dataflow graph be exploited? This is difficult when the dataflow language or programming model is implemented by a monad, as is common in the functional community, since expressing dependence between nodes by a monadic bind suggests sequential execution. Even in monadic constructs that explicitly separate state from computation, problems arise due to the need to reason about opaquely defined state. Specifically, when abstractions of the chosen programming model do not enable adequate reasoning about state, it is difficult to detect parallelism between composed stateful computations. In this paper, we propose a programming model that enables the composition of stateful computations and still exposes opportunities for parallelization. We also introduce smap, a higherorder function that can exploit parallelism in stateful computations. We present an implementation of our programming model and smap in Haskell and show that basic concepts from functional reactive programming can be built on top of our programming model with little effort. We compare these implementations to a stateoftheart approach using monadpar and LVars to expose parallelism explicitly and reach the same level of performance, showing that our programming model successfully extracts parallelism that is present in an algorithm. Further evaluation shows that smap is expressive enough to implement parallel reductions and our programming model resolves shortcomings of the streambased programming model for current stateoftheart big data processing systems. Article Search Info 

Finkbeiner, Bernd 
Haskell '19: "Synthesizing Functional Reactive ..."
Synthesizing Functional Reactive Programs
Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito (Saarland University, Germany; Yale University, USA) Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), resulting from TSL synthesis, are turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a realworld kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic ThreepennyGUI library, and to hardware using the Applicative hardware description language ClaSH. Article Search 

Goens, Andrés 
Haskell '19: "STCLang: State Thread Composition ..."
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism
Sebastian Ertel, Justus Adam, Norman A. Rink, Andrés Goens, and Jeronimo Castrillon (Huawei Technologies, Germany; TU Dresden, Germany) Dataflow execution models are used to build highly scalable parallel systems. A programming model that targets parallel dataflow execution must answer the following question: How can parallelism between two dependent nodes in a dataflow graph be exploited? This is difficult when the dataflow language or programming model is implemented by a monad, as is common in the functional community, since expressing dependence between nodes by a monadic bind suggests sequential execution. Even in monadic constructs that explicitly separate state from computation, problems arise due to the need to reason about opaquely defined state. Specifically, when abstractions of the chosen programming model do not enable adequate reasoning about state, it is difficult to detect parallelism between composed stateful computations. In this paper, we propose a programming model that enables the composition of stateful computations and still exposes opportunities for parallelization. We also introduce smap, a higherorder function that can exploit parallelism in stateful computations. We present an implementation of our programming model and smap in Haskell and show that basic concepts from functional reactive programming can be built on top of our programming model with little effort. We compare these implementations to a stateoftheart approach using monadpar and LVars to expose parallelism explicitly and reach the same level of performance, showing that our programming model successfully extracts parallelism that is present in an algorithm. Further evaluation shows that smap is expressive enough to implement parallel reductions and our programming model resolves shortcomings of the streambased programming model for current stateoftheart big data processing systems. Article Search Info 

Hallahan, William T. 
Haskell '19: "G2Q: Haskell Constraint Solving ..."
G2Q: Haskell Constraint Solving
William T. Hallahan, Anton Xue, and Ruzica Piskac (Yale University, USA) Constraint solvers give programmers a useful interface to solve challenging constraints at runtime. In particular, SMT solvers have been used for a vast variety of different, useful applications, ranging from strengthening Haskell's type system to verifying network protocols. Unfortunately, interacting with constraint solvers directly from Haskell requires a great deal of manual effort. Data must be represented in and translated between two forms: that understood by Haskell, and that understood by the SMT solver. Such a translation is often done via printing and parsing text, meaning that any notion of type safety is lost. Furthermore, direct translations are rarely sufficient, as it typically takes many iterations on a design in order to get optimal  or even acceptable  performance from a SMT solver on large scale problems. This need for iteration complicates the translation issue: it is easy to introduce a runtime bug and frustrating to fix said bug. To address these problems, we introduce a new constraint solving library, G2Q. G2Q includes a quasiquoter that allows solving constraints written in Haskell itself, thus unifying data representation, ensuring correct typing, and simplifying development iteration. We describe the API to our library and its backend. Rather than a direct translation to SMT formulas, G2Q makes use of the G2 symbolic execution engine. This allows G2Q to solve problems that are out of scope when directly encoded as SMT formulas. Finally, we demonstrate the usability of G2Q via four example programs. Article Search 

Jaskelioff, Mauro 
Haskell '19: "Monad Transformers and Modular ..."
Monad Transformers and Modular Algebraic Effects: What Binds Them Together
Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff (KU Leuven, Belgium; University of Wrocław, Poland; Imperial College London, UK; National University of Rosario, Argentina) For over two decades, monad transformers have been the main modular approach for expressing purely functional sideeffects in Haskell. Yet, in recent years algebraic effects have emerged as an alternative whose popularity is growing. While the two approaches have been wellstudied, there is still confusion about their relative merits and expressiveness, especially when it comes to their comparative modularity. This paper clarifies the connection between the two approaches—some of which is folklore—and spells out consequences that we believe should be better known. We characterise a class of algebraic effects that is modular, and show how these correspond to a specific class of monad transformers. In particular, we show that our modular algebraic effects gives rise to monad transformers. Moreover, every monad transformer for algebraic operations gives rise to a modular effect handler. Article Search 

Karachalias, Georgios 
Haskell '19: "Bidirectional Type Class Instances ..."
Bidirectional Type Class Instances
Koen Pauwels, Georgios Karachalias, Michiel Derhaeg, and Tom Schrijvers (KU Leuven, Belgium; Guardsquare, n.n.) GADTs were introduced in Haskell’s ecosystem more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be surprisingly difficult to provide an instance for even the simplest of type classes. In this paper we identify the source of this shortcoming and address it by introducing a conservative extension to Haskell’s type classes: Bidirectional Type Class Instances. In essence, under our interpretation class instances correspond to logical biimplications, in contrast to their traditional unidirectional interpretation. We present a fullyfledged design of bidirectional instances, covering the specification of typing and elaboration into System FC, as well as an algorithm for type inference and elaboration. We provide a proofofconcept implementation of our algorithm, and revisit the metatheory of type classes in the presence of our extension. Article Search 

Kiss, Csongor 
Haskell '19: "Multistage Programs in Context ..."
Multistage Programs in Context
Matthew Pickering, Nicolas Wu, and Csongor Kiss (University of Bristol, UK; Imperial College London, UK) Crossstage persistence is an essential aspect of multistage programming that allows a value defined in one stage to be available in another. However, difficulty arises when implicit information held in types, type classes and implicit parameters needs to be persisted. Without a careful treatment of such implicit informationwhich are pervasive in Haskellsubtle yet avoidable bugs lurk beneath the surface. This paper demonstrates that in multistage programming care must be taken when representing quoted terms so that important implicit information is kept in context and not discarded. The approach is formalised with a typesystem, and an implementation in GHC is presented that fixes problems of the previous incarnation. Article Search 

Klein, Felix 
Haskell '19: "Synthesizing Functional Reactive ..."
Synthesizing Functional Reactive Programs
Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito (Saarland University, Germany; Yale University, USA) Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), resulting from TSL synthesis, are turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a realworld kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic ThreepennyGUI library, and to hardware using the Applicative hardware description language ClaSH. Article Search 

Lechner, Jakob 
Haskell '19: "Formal Verification of Spacecraft ..."
Formal Verification of Spacecraft Control Programs (Experience Report)
Andrey Mokhov, Georgy Lukyanov, and Jakob Lechner (Newcastle University, UK; RUAG Space, Austria) Verification of correctness of control programs is an essential task in the development of space electronics; it is difficult and typically outweighs design and programming tasks in terms of development hours. This experience report presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of lowlevel control programs executed on custom hardware. The verification approach is demonstrated on an industrial case study. We present REDFIN, a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage for state transformers, followed by examples of verification of simple control programs. Article Search 

Lukyanov, Georgy 
Haskell '19: "Formal Verification of Spacecraft ..."
Formal Verification of Spacecraft Control Programs (Experience Report)
Andrey Mokhov, Georgy Lukyanov, and Jakob Lechner (Newcastle University, UK; RUAG Space, Austria) Verification of correctness of control programs is an essential task in the development of space electronics; it is difficult and typically outweighs design and programming tasks in terms of development hours. This experience report presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of lowlevel control programs executed on custom hardware. The verification approach is demonstrated on an industrial case study. We present REDFIN, a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage for state transformers, followed by examples of verification of simple control programs. Article Search 

Mokhov, Andrey 
Haskell '19: "Formal Verification of Spacecraft ..."
Formal Verification of Spacecraft Control Programs (Experience Report)
Andrey Mokhov, Georgy Lukyanov, and Jakob Lechner (Newcastle University, UK; RUAG Space, Austria) Verification of correctness of control programs is an essential task in the development of space electronics; it is difficult and typically outweighs design and programming tasks in terms of development hours. This experience report presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of lowlevel control programs executed on custom hardware. The verification approach is demonstrated on an industrial case study. We present REDFIN, a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage for state transformers, followed by examples of verification of simple control programs. Article Search 

Németh, Boldizsár 
Haskell '19: "Working with Source Plugins ..."
Working with Source Plugins
Matthew Pickering, Nicolas Wu, and Boldizsár Németh (University of Bristol, UK; Imperial College London, UK; Eötvös Loránd University, Hungary) A modern compiler calculates and constructs a large amount of information about the programs it compiles. Tooling authors want to take advantage of this information in order to extend the compiler in interesting ways. Source plugins are a mechanism implemented in the Glasgow Haskell Compiler (GHC) which allow inspection and modification of programs as they pass through the compilation pipeline. This paper is about how to write source plugins. Due to their nature—they are ways to extend the compiler—at least basic knowledge about how the compiler works is critical to designing and implementing a robust and therefore successful plugin. The goal of the paper is to equip wouldbe plugin authors with inspiration about what kinds of plugins they should write and most importantly with the basic techniques which should be used in order to write them. Article Search 

Newton, Ryan R. 
Haskell '19: "Generic and Flexible Defaults ..."
Generic and Flexible Defaults for Verified, LawAbiding TypeClass Instances
Ryan G. Scott and Ryan R. Newton (Indiana University, USA) Dependently typed languages allow programmers to state and prove type class laws by simply encoding the laws as class methods. But writing implementations of these methods frequently give way to large amounts of routine, boilerplate code, and depending on the law involved, the size of these proofs can grow superlinearly with the size of the datatypes involved. We present a technique for automating away large swaths of this boilerplate by leveraging datatypegeneric programming. We observe that any algebraic data type has an equivalent representation type that is composed of simpler, smaller types that are simpler to prove theorems over. By constructing an isomorphism between a datatype and its representation type, we derive proofs for the original datatype by reusing the corresponding proof over the representation type. Our work is designed to be generalpurpose and does not require advanced automation techniques such as tactic systems. As evidence for this claim, we implement these ideas in a Haskell library that defines generic, canonical implementations of the methods and proof obligations for classes in the standard base library. Article Search 

Pauwels, Koen 
Haskell '19: "Bidirectional Type Class Instances ..."
Bidirectional Type Class Instances
Koen Pauwels, Georgios Karachalias, Michiel Derhaeg, and Tom Schrijvers (KU Leuven, Belgium; Guardsquare, n.n.) GADTs were introduced in Haskell’s ecosystem more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be surprisingly difficult to provide an instance for even the simplest of type classes. In this paper we identify the source of this shortcoming and address it by introducing a conservative extension to Haskell’s type classes: Bidirectional Type Class Instances. In essence, under our interpretation class instances correspond to logical biimplications, in contrast to their traditional unidirectional interpretation. We present a fullyfledged design of bidirectional instances, covering the specification of typing and elaboration into System FC, as well as an algorithm for type inference and elaboration. We provide a proofofconcept implementation of our algorithm, and revisit the metatheory of type classes in the presence of our extension. Article Search 

Peyton Jones, Simon 
Haskell '19: "Making a Faster Curry with ..."
Making a Faster Curry with Extensional Types
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones (University of Oregon, USA; Microsoft Research, UK) Curried functions apparently take one argument at a time, which is slow. So optimizing compilers for higherorder languages invariably have some mechanism for working around currying by passing several arguments at once, as many as the function can handle, which is known as its arity. But such mechanisms are often adhoc, and do not work at all in higherorder functions. We show how extensional, callbyname functions have the correct behavior for directly expressing the arity of curried functions. And these extensional functions can stand sidebyside with functions native to practical programming languages, which do not use callbyname evaluation. Integrating callbyname with other evaluation strategies in the same intermediate language expresses the arity of a function in its type and gives a principled and compositional account of multiargument curried functions. An unexpected, but significant, bonus is that our approach is equally suitable for a callbyvalue language and a callbyneed language, and it can be readily integrated into an existing compilation framework. Article Search 

Pickering, Matthew 
Haskell '19: "Multistage Programs in Context ..."
Multistage Programs in Context
Matthew Pickering, Nicolas Wu, and Csongor Kiss (University of Bristol, UK; Imperial College London, UK) Crossstage persistence is an essential aspect of multistage programming that allows a value defined in one stage to be available in another. However, difficulty arises when implicit information held in types, type classes and implicit parameters needs to be persisted. Without a careful treatment of such implicit informationwhich are pervasive in Haskellsubtle yet avoidable bugs lurk beneath the surface. This paper demonstrates that in multistage programming care must be taken when representing quoted terms so that important implicit information is kept in context and not discarded. The approach is formalised with a typesystem, and an implementation in GHC is presented that fixes problems of the previous incarnation. Article Search Haskell '19: "Working with Source Plugins ..." Working with Source Plugins Matthew Pickering, Nicolas Wu, and Boldizsár Németh (University of Bristol, UK; Imperial College London, UK; Eötvös Loránd University, Hungary) A modern compiler calculates and constructs a large amount of information about the programs it compiles. Tooling authors want to take advantage of this information in order to extend the compiler in interesting ways. Source plugins are a mechanism implemented in the Glasgow Haskell Compiler (GHC) which allow inspection and modification of programs as they pass through the compilation pipeline. This paper is about how to write source plugins. Due to their nature—they are ways to extend the compiler—at least basic knowledge about how the compiler works is critical to designing and implementing a robust and therefore successful plugin. The goal of the paper is to equip wouldbe plugin authors with inspiration about what kinds of plugins they should write and most importantly with the basic techniques which should be used in order to write them. Article Search 

Piróg, Maciej 
Haskell '19: "Monad Transformers and Modular ..."
Monad Transformers and Modular Algebraic Effects: What Binds Them Together
Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff (KU Leuven, Belgium; University of Wrocław, Poland; Imperial College London, UK; National University of Rosario, Argentina) For over two decades, monad transformers have been the main modular approach for expressing purely functional sideeffects in Haskell. Yet, in recent years algebraic effects have emerged as an alternative whose popularity is growing. While the two approaches have been wellstudied, there is still confusion about their relative merits and expressiveness, especially when it comes to their comparative modularity. This paper clarifies the connection between the two approaches—some of which is folklore—and spells out consequences that we believe should be better known. We characterise a class of algebraic effects that is modular, and show how these correspond to a specific class of monad transformers. In particular, we show that our modular algebraic effects gives rise to monad transformers. Moreover, every monad transformer for algebraic operations gives rise to a modular effect handler. Article Search 

Piskac, Ruzica 
Haskell '19: "G2Q: Haskell Constraint Solving ..."
G2Q: Haskell Constraint Solving
William T. Hallahan, Anton Xue, and Ruzica Piskac (Yale University, USA) Constraint solvers give programmers a useful interface to solve challenging constraints at runtime. In particular, SMT solvers have been used for a vast variety of different, useful applications, ranging from strengthening Haskell's type system to verifying network protocols. Unfortunately, interacting with constraint solvers directly from Haskell requires a great deal of manual effort. Data must be represented in and translated between two forms: that understood by Haskell, and that understood by the SMT solver. Such a translation is often done via printing and parsing text, meaning that any notion of type safety is lost. Furthermore, direct translations are rarely sufficient, as it typically takes many iterations on a design in order to get optimal  or even acceptable  performance from a SMT solver on large scale problems. This need for iteration complicates the translation issue: it is easy to introduce a runtime bug and frustrating to fix said bug. To address these problems, we introduce a new constraint solving library, G2Q. G2Q includes a quasiquoter that allows solving constraints written in Haskell itself, thus unifying data representation, ensuring correct typing, and simplifying development iteration. We describe the API to our library and its backend. Rather than a direct translation to SMT formulas, G2Q makes use of the G2 symbolic execution engine. This allows G2Q to solve problems that are out of scope when directly encoded as SMT formulas. Finally, we demonstrate the usability of G2Q via four example programs. Article Search Haskell '19: "Synthesizing Functional Reactive ..." Synthesizing Functional Reactive Programs Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito (Saarland University, Germany; Yale University, USA) Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), resulting from TSL synthesis, are turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a realworld kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic ThreepennyGUI library, and to hardware using the Applicative hardware description language ClaSH. Article Search 

Rink, Norman A. 
Haskell '19: "STCLang: State Thread Composition ..."
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism
Sebastian Ertel, Justus Adam, Norman A. Rink, Andrés Goens, and Jeronimo Castrillon (Huawei Technologies, Germany; TU Dresden, Germany) Dataflow execution models are used to build highly scalable parallel systems. A programming model that targets parallel dataflow execution must answer the following question: How can parallelism between two dependent nodes in a dataflow graph be exploited? This is difficult when the dataflow language or programming model is implemented by a monad, as is common in the functional community, since expressing dependence between nodes by a monadic bind suggests sequential execution. Even in monadic constructs that explicitly separate state from computation, problems arise due to the need to reason about opaquely defined state. Specifically, when abstractions of the chosen programming model do not enable adequate reasoning about state, it is difficult to detect parallelism between composed stateful computations. In this paper, we propose a programming model that enables the composition of stateful computations and still exposes opportunities for parallelization. We also introduce smap, a higherorder function that can exploit parallelism in stateful computations. We present an implementation of our programming model and smap in Haskell and show that basic concepts from functional reactive programming can be built on top of our programming model with little effort. We compare these implementations to a stateoftheart approach using monadpar and LVars to expose parallelism explicitly and reach the same level of performance, showing that our programming model successfully extracts parallelism that is present in an algorithm. Further evaluation shows that smap is expressive enough to implement parallel reductions and our programming model resolves shortcomings of the streambased programming model for current stateoftheart big data processing systems. Article Search Info 

Santolucito, Mark 
Haskell '19: "Synthesizing Functional Reactive ..."
Synthesizing Functional Reactive Programs
Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito (Saarland University, Germany; Yale University, USA) Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), resulting from TSL synthesis, are turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a realworld kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic ThreepennyGUI library, and to hardware using the Applicative hardware description language ClaSH. Article Search 

Schrijvers, Tom 
Haskell '19: "Monad Transformers and Modular ..."
Monad Transformers and Modular Algebraic Effects: What Binds Them Together
Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff (KU Leuven, Belgium; University of Wrocław, Poland; Imperial College London, UK; National University of Rosario, Argentina) For over two decades, monad transformers have been the main modular approach for expressing purely functional sideeffects in Haskell. Yet, in recent years algebraic effects have emerged as an alternative whose popularity is growing. While the two approaches have been wellstudied, there is still confusion about their relative merits and expressiveness, especially when it comes to their comparative modularity. This paper clarifies the connection between the two approaches—some of which is folklore—and spells out consequences that we believe should be better known. We characterise a class of algebraic effects that is modular, and show how these correspond to a specific class of monad transformers. In particular, we show that our modular algebraic effects gives rise to monad transformers. Moreover, every monad transformer for algebraic operations gives rise to a modular effect handler. Article Search Haskell '19: "Bidirectional Type Class Instances ..." Bidirectional Type Class Instances Koen Pauwels, Georgios Karachalias, Michiel Derhaeg, and Tom Schrijvers (KU Leuven, Belgium; Guardsquare, n.n.) GADTs were introduced in Haskell’s ecosystem more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be surprisingly difficult to provide an instance for even the simplest of type classes. In this paper we identify the source of this shortcoming and address it by introducing a conservative extension to Haskell’s type classes: Bidirectional Type Class Instances. In essence, under our interpretation class instances correspond to logical biimplications, in contrast to their traditional unidirectional interpretation. We present a fullyfledged design of bidirectional instances, covering the specification of typing and elaboration into System FC, as well as an algorithm for type inference and elaboration. We provide a proofofconcept implementation of our algorithm, and revisit the metatheory of type classes in the presence of our extension. Article Search 

Scott, Ryan G. 
Haskell '19: "Generic and Flexible Defaults ..."
Generic and Flexible Defaults for Verified, LawAbiding TypeClass Instances
Ryan G. Scott and Ryan R. Newton (Indiana University, USA) Dependently typed languages allow programmers to state and prove type class laws by simply encoding the laws as class methods. But writing implementations of these methods frequently give way to large amounts of routine, boilerplate code, and depending on the law involved, the size of these proofs can grow superlinearly with the size of the datatypes involved. We present a technique for automating away large swaths of this boilerplate by leveraging datatypegeneric programming. We observe that any algebraic data type has an equivalent representation type that is composed of simpler, smaller types that are simpler to prove theorems over. By constructing an isomorphism between a datatype and its representation type, we derive proofs for the original datatype by reusing the corresponding proof over the representation type. Our work is designed to be generalpurpose and does not require advanced automation techniques such as tactic systems. As evidence for this claim, we implement these ideas in a Haskell library that defines generic, canonical implementations of the methods and proof obligations for classes in the standard base library. Article Search 

Sullivan, Zachary 
Haskell '19: "Making a Faster Curry with ..."
Making a Faster Curry with Extensional Types
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones (University of Oregon, USA; Microsoft Research, UK) Curried functions apparently take one argument at a time, which is slow. So optimizing compilers for higherorder languages invariably have some mechanism for working around currying by passing several arguments at once, as many as the function can handle, which is known as its arity. But such mechanisms are often adhoc, and do not work at all in higherorder functions. We show how extensional, callbyname functions have the correct behavior for directly expressing the arity of curried functions. And these extensional functions can stand sidebyside with functions native to practical programming languages, which do not use callbyname evaluation. Integrating callbyname with other evaluation strategies in the same intermediate language expresses the arity of a function in its type and gives a principled and compositional account of multiargument curried functions. An unexpected, but significant, bonus is that our approach is equally suitable for a callbyvalue language and a callbyneed language, and it can be readily integrated into an existing compilation framework. Article Search 

Wu, Nicolas 
Haskell '19: "Monad Transformers and Modular ..."
Monad Transformers and Modular Algebraic Effects: What Binds Them Together
Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff (KU Leuven, Belgium; University of Wrocław, Poland; Imperial College London, UK; National University of Rosario, Argentina) For over two decades, monad transformers have been the main modular approach for expressing purely functional sideeffects in Haskell. Yet, in recent years algebraic effects have emerged as an alternative whose popularity is growing. While the two approaches have been wellstudied, there is still confusion about their relative merits and expressiveness, especially when it comes to their comparative modularity. This paper clarifies the connection between the two approaches—some of which is folklore—and spells out consequences that we believe should be better known. We characterise a class of algebraic effects that is modular, and show how these correspond to a specific class of monad transformers. In particular, we show that our modular algebraic effects gives rise to monad transformers. Moreover, every monad transformer for algebraic operations gives rise to a modular effect handler. Article Search Haskell '19: "Multistage Programs in Context ..." Multistage Programs in Context Matthew Pickering, Nicolas Wu, and Csongor Kiss (University of Bristol, UK; Imperial College London, UK) Crossstage persistence is an essential aspect of multistage programming that allows a value defined in one stage to be available in another. However, difficulty arises when implicit information held in types, type classes and implicit parameters needs to be persisted. Without a careful treatment of such implicit informationwhich are pervasive in Haskellsubtle yet avoidable bugs lurk beneath the surface. This paper demonstrates that in multistage programming care must be taken when representing quoted terms so that important implicit information is kept in context and not discarded. The approach is formalised with a typesystem, and an implementation in GHC is presented that fixes problems of the previous incarnation. Article Search Haskell '19: "Working with Source Plugins ..." Working with Source Plugins Matthew Pickering, Nicolas Wu, and Boldizsár Németh (University of Bristol, UK; Imperial College London, UK; Eötvös Loránd University, Hungary) A modern compiler calculates and constructs a large amount of information about the programs it compiles. Tooling authors want to take advantage of this information in order to extend the compiler in interesting ways. Source plugins are a mechanism implemented in the Glasgow Haskell Compiler (GHC) which allow inspection and modification of programs as they pass through the compilation pipeline. This paper is about how to write source plugins. Due to their nature—they are ways to extend the compiler—at least basic knowledge about how the compiler works is critical to designing and implementing a robust and therefore successful plugin. The goal of the paper is to equip wouldbe plugin authors with inspiration about what kinds of plugins they should write and most importantly with the basic techniques which should be used in order to write them. Article Search 

Xue, Anton 
Haskell '19: "G2Q: Haskell Constraint Solving ..."
G2Q: Haskell Constraint Solving
William T. Hallahan, Anton Xue, and Ruzica Piskac (Yale University, USA) Constraint solvers give programmers a useful interface to solve challenging constraints at runtime. In particular, SMT solvers have been used for a vast variety of different, useful applications, ranging from strengthening Haskell's type system to verifying network protocols. Unfortunately, interacting with constraint solvers directly from Haskell requires a great deal of manual effort. Data must be represented in and translated between two forms: that understood by Haskell, and that understood by the SMT solver. Such a translation is often done via printing and parsing text, meaning that any notion of type safety is lost. Furthermore, direct translations are rarely sufficient, as it typically takes many iterations on a design in order to get optimal  or even acceptable  performance from a SMT solver on large scale problems. This need for iteration complicates the translation issue: it is easy to introduce a runtime bug and frustrating to fix said bug. To address these problems, we introduce a new constraint solving library, G2Q. G2Q includes a quasiquoter that allows solving constraints written in Haskell itself, thus unifying data representation, ensuring correct typing, and simplifying development iteration. We describe the API to our library and its backend. Rather than a direct translation to SMT formulas, G2Q makes use of the G2 symbolic execution engine. This allows G2Q to solve problems that are out of scope when directly encoded as SMT formulas. Finally, we demonstrate the usability of G2Q via four example programs. Article Search 
35 authors
proc time: 1.81