Workshop Haskell 2022 – Author Index 
Contents 
Abstracts 
Authors

B C D E F G H I K L M N O P R S V W
Bazerman, Gershom 
Haskell '22: "A Totally Predictable Outcome: ..."
A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures
Gershom Bazerman (Arista Networks, USA) Functors with an instance of the Traversable type class can be thought of as data structures which permit a traversal of their elements. This has been made precise by the correspondence between traversable functors and finitary containers (also known as polynomial functors)  established in the context of total, necessarily terminating, functions. However, the Haskell language is nonstrict and permits functions that do not terminate. It has long been observed that traversals can at times in fact operate over infinite lists, for example in distributing the Reader applicative. The result of such a traversal remains an infinite structure, however it nonetheless is productive  i.e. successive amounts of finite computation yield either termination or successive results. To investigate this phenomenon, we draw on tools from guarded recursion, making use of equational reasoning directly in Haskell. @InProceedings{Haskell22p39, author = {Gershom Bazerman}, title = {A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {3953}, doi = {10.1145/3546189.3549915}, year = {2022}, } Publisher's Version 

Blanchette, Henry 
Haskell '22: "Liquid Proof Macros ..."
Liquid Proof Macros
Henry Blanchette , Niki Vazou , and Leonidas Lampropoulos (University of Maryland at College Park, USA; IMDEA Software Institute, Spain) Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users' burden of proof. However, this power does not come without a price: convincing Liquid Haskell that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell's inner workings. In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tacticinspired DSL interface for more concise and userfriendly proofs, and we demonstrate the capabilities of this framework by automating a wide variety of proofs from an existing Liquid Haskell benchmark. @InProceedings{Haskell22p27, author = {Henry Blanchette and Niki Vazou and Leonidas Lampropoulos}, title = {Liquid Proof Macros}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {2738}, doi = {10.1145/3546189.3549921}, year = {2022}, } Publisher's Version Info 

Cavalheiro, Gerson Geraldo Homrich 
Haskell '22: "Open Transactional Actions: ..."
Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell
Jonathas Augusto de Oliveira Conceição , André Rauber Du Bois , Samuel da Silva Feitosa , Gerson Geraldo Homrich Cavalheiro , and Rodrigo Geraldo Ribeiro (Federal University of Pelotas, Brazil; Federal University of Fronteira Sul, Brazil; Federal University of Ouro Preto, Brazil) This paper addresses the problem of accessing external resources from inside transactions in STM Haskell, and for that purpose introduces a new abstraction called Open Transactional Actions (OTAs) that provides a framework for wrapping nontransactional resources in a transactional layer. OTAs allow the programmer to access resources through IO actions, from inside transactions, and also to register commit and abort handlers: the former are used to make the accesses to resources visible to other transactions at commit time, and the latter to undo changes in the resource if the transaction has to roll back. OTAs, once started, are guaranteed to be executed completely before the hosting transaction can be aborted, guarantying that if a resource is accessed, its respective commit and abort actions will be properly registered. We believe that OTAs could be used by expert programmers to implement useful system libraries and also to give a transactional semantics to fast linearizable data structures, i.e., transactional boosting. As a proof of concept, we present examples that use OTAs to implement transactional file access and transactional boosted data types that are faster than pure STM Haskell in most cases. @InProceedings{Haskell22p54, author = {Jonathas Augusto de Oliveira Conceição and André Rauber Du Bois and Samuel da Silva Feitosa and Gerson Geraldo Homrich Cavalheiro and Rodrigo Geraldo Ribeiro}, title = {Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {5465}, doi = {10.1145/3546189.3549924}, year = {2022}, } Publisher's Version Info 

Chapman, James 
Haskell '22: "Reasonable Agda Is Correct ..."
Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
Jesper Cockx , Orestis Melkonian , Lucas Escot , James Chapman , and Ulf Norell (Delft University of Technology, Netherlands; University of Edinburgh, UK; Input Output, UK; University of Gothenburg, Sweden) Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda's support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda. We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience. This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked. @InProceedings{Haskell22p108, author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell}, title = {Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {108122}, doi = {10.1145/3546189.3549920}, year = {2022}, } Publisher's Version 

Cockx, Jesper 
Haskell '22: "Reasonable Agda Is Correct ..."
Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
Jesper Cockx , Orestis Melkonian , Lucas Escot , James Chapman , and Ulf Norell (Delft University of Technology, Netherlands; University of Edinburgh, UK; Input Output, UK; University of Gothenburg, Sweden) Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda's support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda. We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience. This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked. @InProceedings{Haskell22p108, author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell}, title = {Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {108122}, doi = {10.1145/3546189.3549920}, year = {2022}, } Publisher's Version 

Conceição, Jonathas Augusto de Oliveira 
Haskell '22: "Open Transactional Actions: ..."
Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell
Jonathas Augusto de Oliveira Conceição , André Rauber Du Bois , Samuel da Silva Feitosa , Gerson Geraldo Homrich Cavalheiro , and Rodrigo Geraldo Ribeiro (Federal University of Pelotas, Brazil; Federal University of Fronteira Sul, Brazil; Federal University of Ouro Preto, Brazil) This paper addresses the problem of accessing external resources from inside transactions in STM Haskell, and for that purpose introduces a new abstraction called Open Transactional Actions (OTAs) that provides a framework for wrapping nontransactional resources in a transactional layer. OTAs allow the programmer to access resources through IO actions, from inside transactions, and also to register commit and abort handlers: the former are used to make the accesses to resources visible to other transactions at commit time, and the latter to undo changes in the resource if the transaction has to roll back. OTAs, once started, are guaranteed to be executed completely before the hosting transaction can be aborted, guarantying that if a resource is accessed, its respective commit and abort actions will be properly registered. We believe that OTAs could be used by expert programmers to implement useful system libraries and also to give a transactional semantics to fast linearizable data structures, i.e., transactional boosting. As a proof of concept, we present examples that use OTAs to implement transactional file access and transactional boosted data types that are faster than pure STM Haskell in most cases. @InProceedings{Haskell22p54, author = {Jonathas Augusto de Oliveira Conceição and André Rauber Du Bois and Samuel da Silva Feitosa and Gerson Geraldo Homrich Cavalheiro and Rodrigo Geraldo Ribeiro}, title = {Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {5465}, doi = {10.1145/3546189.3549924}, year = {2022}, } Publisher's Version Info 

Du Bois, André Rauber 
Haskell '22: "Open Transactional Actions: ..."
Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell
Jonathas Augusto de Oliveira Conceição , André Rauber Du Bois , Samuel da Silva Feitosa , Gerson Geraldo Homrich Cavalheiro , and Rodrigo Geraldo Ribeiro (Federal University of Pelotas, Brazil; Federal University of Fronteira Sul, Brazil; Federal University of Ouro Preto, Brazil) This paper addresses the problem of accessing external resources from inside transactions in STM Haskell, and for that purpose introduces a new abstraction called Open Transactional Actions (OTAs) that provides a framework for wrapping nontransactional resources in a transactional layer. OTAs allow the programmer to access resources through IO actions, from inside transactions, and also to register commit and abort handlers: the former are used to make the accesses to resources visible to other transactions at commit time, and the latter to undo changes in the resource if the transaction has to roll back. OTAs, once started, are guaranteed to be executed completely before the hosting transaction can be aborted, guarantying that if a resource is accessed, its respective commit and abort actions will be properly registered. We believe that OTAs could be used by expert programmers to implement useful system libraries and also to give a transactional semantics to fast linearizable data structures, i.e., transactional boosting. As a proof of concept, we present examples that use OTAs to implement transactional file access and transactional boosted data types that are faster than pure STM Haskell in most cases. @InProceedings{Haskell22p54, author = {Jonathas Augusto de Oliveira Conceição and André Rauber Du Bois and Samuel da Silva Feitosa and Gerson Geraldo Homrich Cavalheiro and Rodrigo Geraldo Ribeiro}, title = {Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {5465}, doi = {10.1145/3546189.3549924}, year = {2022}, } Publisher's Version Info 

Escot, Lucas 
Haskell '22: "Reasonable Agda Is Correct ..."
Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
Jesper Cockx , Orestis Melkonian , Lucas Escot , James Chapman , and Ulf Norell (Delft University of Technology, Netherlands; University of Edinburgh, UK; Input Output, UK; University of Gothenburg, Sweden) Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda's support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda. We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience. This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked. @InProceedings{Haskell22p108, author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell}, title = {Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {108122}, doi = {10.1145/3546189.3549920}, year = {2022}, } Publisher's Version 

Feitosa, Samuel da Silva 
Haskell '22: "Open Transactional Actions: ..."
Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell
Jonathas Augusto de Oliveira Conceição , André Rauber Du Bois , Samuel da Silva Feitosa , Gerson Geraldo Homrich Cavalheiro , and Rodrigo Geraldo Ribeiro (Federal University of Pelotas, Brazil; Federal University of Fronteira Sul, Brazil; Federal University of Ouro Preto, Brazil) This paper addresses the problem of accessing external resources from inside transactions in STM Haskell, and for that purpose introduces a new abstraction called Open Transactional Actions (OTAs) that provides a framework for wrapping nontransactional resources in a transactional layer. OTAs allow the programmer to access resources through IO actions, from inside transactions, and also to register commit and abort handlers: the former are used to make the accesses to resources visible to other transactions at commit time, and the latter to undo changes in the resource if the transaction has to roll back. OTAs, once started, are guaranteed to be executed completely before the hosting transaction can be aborted, guarantying that if a resource is accessed, its respective commit and abort actions will be properly registered. We believe that OTAs could be used by expert programmers to implement useful system libraries and also to give a transactional semantics to fast linearizable data structures, i.e., transactional boosting. As a proof of concept, we present examples that use OTAs to implement transactional file access and transactional boosted data types that are faster than pure STM Haskell in most cases. @InProceedings{Haskell22p54, author = {Jonathas Augusto de Oliveira Conceição and André Rauber Du Bois and Samuel da Silva Feitosa and Gerson Geraldo Homrich Cavalheiro and Rodrigo Geraldo Ribeiro}, title = {Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {5465}, doi = {10.1145/3546189.3549924}, year = {2022}, } Publisher's Version Info 

Greenberg, Michael 
Haskell '22: "How to Safely Use Extensionality ..."
How to Safely Use Extensionality in Liquid Haskell
Niki Vazou and Michael Greenberg (IMDEA Software Institute, Spain; Stevens Institute of Technology, USA) Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation and port the proofs to an optimized pure implementation that behaves the same. But to reason about higherorder programs, we must reason about equalities between functions: we need a consistent encoding of functional extensionality. A natural but naive phrasing of the functional extensionality axiom (funExt) is inconsistent in refinement type systems with semantic subtyping and polymorphism: if we assume funExt, then we can prove false. We demonstrate the inconsistency and develop a new approach to equality in Liquid Haskell: we define a propositional equality in a library we call PEq. Using PEq avoids the inconsistency while proving useful equalities at higher types; we demonstrate its use in several case studies. We validate PEq by building a model and developing its metatheory. Additionally, we prove metaproperties of PEq inside Liquid Haskell itself using an unnamed folklore technique, which we dub 'classy induction'. @InProceedings{Haskell22p13, author = {Niki Vazou and Michael Greenberg}, title = {How to Safely Use Extensionality in Liquid Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {1326}, doi = {10.1145/3546189.3549919}, year = {2022}, } Publisher's Version 

Hollenbeck, Celeste 
Haskell '22: "Investigating Magic Numbers: ..."
Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler
Celeste Hollenbeck , Michael F. P. O'Boyle , and Michel Steuwer (University of Edinburgh, UK) Inlining is a widely studied compiler optimization that is particularly important for functional languages such as Haskell and OCaml. The Glasgow Haskell Compiler (GHC) inliner is a heuristic of such complexity, however, that it has not significantly changed for nearly 20 years. It heavily relies on hardcoded numeric constants, or magic numbers, based on outofdate intuition. Dissatisfaction with inlining performance has led to the widespread use of inlining pragmas by programmers. In this paper, we present an indepth study of the effect of inlining on performance in functional languages. We specifically focus on the inlining behavior of GHC and present techniques to systematically explore the space of possible magic number values, or configurations, and evaluate their performance on a set of realworld benchmarks where inline pragmas are present. Pragmas may slow down individual programs, but on average improve performance by 10%. Searching for the best configuration on a perprogram basis increases this performance to an average of 27%. Searching for the best configuration for each program is, however, expensive and unrealistic, requiring repeated compilation and execution. This paper determines a new single configuration that gives a 22% improvement on average across the benchmarks. Finally, we use a simple machine learning model that predicts the best configuration on a perprogram basis, giving a 26% average improvement. @InProceedings{Haskell22p81, author = {Celeste Hollenbeck and Michael F. P. O'Boyle and Michel Steuwer}, title = {Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {8194}, doi = {10.1145/3546189.3549918}, year = {2022}, } Publisher's Version 

Hubers, Alex 
Haskell '22: "Partial Type Constructors ..."
Partial Type Constructors in Practice
Apoorv Ingle , Alex Hubers , and J. Garrett Morris (University of Iowa, USA) Type constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only make sense for orderable elements, or embedded DSLs might only make sense for serializable return types. Jones et al. proposed a theory of partial type constructors, which guarantees that type applications are sensible, and extends higherorder abstractions to apply equally well to partial and total type constructors. This paper evaluates the practicality of partial type constructors, in terms of both language design and implementation. We extend GHC, the most widely used Haskell compiler, with support for partial type constructors, and test our extension on the compiler itself and its libraries. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design. @InProceedings{Haskell22p95, author = {Apoorv Ingle and Alex Hubers and J. Garrett Morris}, title = {Partial Type Constructors in Practice}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {95107}, doi = {10.1145/3546189.3549923}, year = {2022}, } Publisher's Version 

Ingle, Apoorv 
Haskell '22: "Partial Type Constructors ..."
Partial Type Constructors in Practice
Apoorv Ingle , Alex Hubers , and J. Garrett Morris (University of Iowa, USA) Type constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only make sense for orderable elements, or embedded DSLs might only make sense for serializable return types. Jones et al. proposed a theory of partial type constructors, which guarantees that type applications are sensible, and extends higherorder abstractions to apply equally well to partial and total type constructors. This paper evaluates the practicality of partial type constructors, in terms of both language design and implementation. We extend GHC, the most widely used Haskell compiler, with support for partial type constructors, and test our extension on the compiler itself and its libraries. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design. @InProceedings{Haskell22p95, author = {Apoorv Ingle and Alex Hubers and J. Garrett Morris}, title = {Partial Type Constructors in Practice}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {95107}, doi = {10.1145/3546189.3549923}, year = {2022}, } Publisher's Version 

Keller, Gabriele 
Haskell '22: "Embedded Pattern Matching ..."
Embedded Pattern Matching
Trevor L. McDonell , Joshua D. Meredith , and Gabriele Keller (Utrecht University, Netherlands; IOG, Australia) Haskell is a popular choice for hosting deeply embedded languages. A recurring challenge for these embeddings is how to seamlessly integrate user defined algebraic data types. In particular, one important, convenient, and expressive feature for creating and inspecting data—pattern matching—is not directly available on embedded terms. We present a novel technique, embedded pattern matching, which enables a natural and user friendly embedding of user defined algebraic data types into the embedded language, and allows programmers to pattern match on terms in the embedded language in much the same way they would in the host language. @InProceedings{Haskell22p123, author = {Trevor L. McDonell and Joshua D. Meredith and Gabriele Keller}, title = {Embedded Pattern Matching}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {123136}, doi = {10.1145/3546189.3549917}, year = {2022}, } Publisher's Version Info 

Lampropoulos, Leonidas 
Haskell '22: "Liquid Proof Macros ..."
Liquid Proof Macros
Henry Blanchette , Niki Vazou , and Leonidas Lampropoulos (University of Maryland at College Park, USA; IMDEA Software Institute, Spain) Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users' burden of proof. However, this power does not come without a price: convincing Liquid Haskell that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell's inner workings. In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tacticinspired DSL interface for more concise and userfriendly proofs, and we demonstrate the capabilities of this framework by automating a wide variety of proofs from an existing Liquid Haskell benchmark. @InProceedings{Haskell22p27, author = {Henry Blanchette and Niki Vazou and Leonidas Lampropoulos}, title = {Liquid Proof Macros}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {2738}, doi = {10.1145/3546189.3549921}, year = {2022}, } Publisher's Version Info 

Mastorou, Lykourgos 
Haskell '22: "Coinduction Inductively: Mechanizing ..."
Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
Lykourgos Mastorou , Nikolaos Papaspyrou , and Niki Vazou (National Technical University of Athens, Greece; IMDEA Software Institute, Spain; Google, Germany) Liquid Haskell is an inductive verifier that cannot reason about codata. In this work we present two alternative approaches, namely indexed and constructive coinduction, to consistently encode coinductive proofs in Liquid Haskell. The intuition is that indices can be used to enforce the base case in the setting of classical logic and the guardedness check in the constructive proofs. We use our encodings to machine check 10 coinductive proofs, about unary and binary predicates on infinite streams and lists, showcasing how an inductive verifier can be used to check coinductive properties of Haskell code. @InProceedings{Haskell22p1, author = {Lykourgos Mastorou and Nikolaos Papaspyrou and Niki Vazou}, title = {Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {112}, doi = {10.1145/3546189.3549922}, year = {2022}, } Publisher's Version 

McDonell, Trevor L. 
Haskell '22: "Embedded Pattern Matching ..."
Embedded Pattern Matching
Trevor L. McDonell , Joshua D. Meredith , and Gabriele Keller (Utrecht University, Netherlands; IOG, Australia) Haskell is a popular choice for hosting deeply embedded languages. A recurring challenge for these embeddings is how to seamlessly integrate user defined algebraic data types. In particular, one important, convenient, and expressive feature for creating and inspecting data—pattern matching—is not directly available on embedded terms. We present a novel technique, embedded pattern matching, which enables a natural and user friendly embedding of user defined algebraic data types into the embedded language, and allows programmers to pattern match on terms in the embedded language in much the same way they would in the host language. @InProceedings{Haskell22p123, author = {Trevor L. McDonell and Joshua D. Meredith and Gabriele Keller}, title = {Embedded Pattern Matching}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {123136}, doi = {10.1145/3546189.3549917}, year = {2022}, } Publisher's Version Info 

Melkonian, Orestis 
Haskell '22: "Reasonable Agda Is Correct ..."
Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
Jesper Cockx , Orestis Melkonian , Lucas Escot , James Chapman , and Ulf Norell (Delft University of Technology, Netherlands; University of Edinburgh, UK; Input Output, UK; University of Gothenburg, Sweden) Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda's support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda. We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience. This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked. @InProceedings{Haskell22p108, author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell}, title = {Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {108122}, doi = {10.1145/3546189.3549920}, year = {2022}, } Publisher's Version 

Meredith, Joshua D. 
Haskell '22: "Embedded Pattern Matching ..."
Embedded Pattern Matching
Trevor L. McDonell , Joshua D. Meredith , and Gabriele Keller (Utrecht University, Netherlands; IOG, Australia) Haskell is a popular choice for hosting deeply embedded languages. A recurring challenge for these embeddings is how to seamlessly integrate user defined algebraic data types. In particular, one important, convenient, and expressive feature for creating and inspecting data—pattern matching—is not directly available on embedded terms. We present a novel technique, embedded pattern matching, which enables a natural and user friendly embedding of user defined algebraic data types into the embedded language, and allows programmers to pattern match on terms in the embedded language in much the same way they would in the host language. @InProceedings{Haskell22p123, author = {Trevor L. McDonell and Joshua D. Meredith and Gabriele Keller}, title = {Embedded Pattern Matching}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {123136}, doi = {10.1145/3546189.3549917}, year = {2022}, } Publisher's Version Info 

Morris, J. Garrett 
Haskell '22: "Partial Type Constructors ..."
Partial Type Constructors in Practice
Apoorv Ingle , Alex Hubers , and J. Garrett Morris (University of Iowa, USA) Type constructors in functional programming languages are total: a Haskell programmer can equally readily construct lists of any element type. In practice, however, not all applications of type constructors are equally sensible: collections may only make sense for orderable elements, or embedded DSLs might only make sense for serializable return types. Jones et al. proposed a theory of partial type constructors, which guarantees that type applications are sensible, and extends higherorder abstractions to apply equally well to partial and total type constructors. This paper evaluates the practicality of partial type constructors, in terms of both language design and implementation. We extend GHC, the most widely used Haskell compiler, with support for partial type constructors, and test our extension on the compiler itself and its libraries. We show that introducing partial type constructors has a minimal impact on most code, but raises important questions in language and library design. @InProceedings{Haskell22p95, author = {Apoorv Ingle and Alex Hubers and J. Garrett Morris}, title = {Partial Type Constructors in Practice}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {95107}, doi = {10.1145/3546189.3549923}, year = {2022}, } Publisher's Version 

Norell, Ulf 
Haskell '22: "Reasonable Agda Is Correct ..."
Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
Jesper Cockx , Orestis Melkonian , Lucas Escot , James Chapman , and Ulf Norell (Delft University of Technology, Netherlands; University of Edinburgh, UK; Input Output, UK; University of Gothenburg, Sweden) Modern dependently typed languages such as Agda can be used to statically enforce the correctness of programs. However, they still lack the large ecosystem of a more popular language like Haskell. To combine the strength of both approaches, we present agda2hs, a tool that translates an expressive subset of Agda to readable Haskell, erasing dependent types and proofs in the process. Thanks to Agda's support for erasure annotations, this process is both safe and transparent to the user. Compared to other tools for program extraction, agda2hs uses a syntax that is already familiar to functional programmers, allows for both intrinsic and extrinsic approaches to verification, and produces Haskell code that is easy to read and audit by programmers with no knowledge of Agda. We present a practical use case of agda2hs at IOG to verify properties of a program generator. While both agda2hs and its ecosystem are still young, our experiences so far show that this is a viable approach to make verified functional programming available to a broader audience. This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked. @InProceedings{Haskell22p108, author = {Jesper Cockx and Orestis Melkonian and Lucas Escot and James Chapman and Ulf Norell}, title = {Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {108122}, doi = {10.1145/3546189.3549920}, year = {2022}, } Publisher's Version 

O'Boyle, Michael F. P. 
Haskell '22: "Investigating Magic Numbers: ..."
Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler
Celeste Hollenbeck , Michael F. P. O'Boyle , and Michel Steuwer (University of Edinburgh, UK) Inlining is a widely studied compiler optimization that is particularly important for functional languages such as Haskell and OCaml. The Glasgow Haskell Compiler (GHC) inliner is a heuristic of such complexity, however, that it has not significantly changed for nearly 20 years. It heavily relies on hardcoded numeric constants, or magic numbers, based on outofdate intuition. Dissatisfaction with inlining performance has led to the widespread use of inlining pragmas by programmers. In this paper, we present an indepth study of the effect of inlining on performance in functional languages. We specifically focus on the inlining behavior of GHC and present techniques to systematically explore the space of possible magic number values, or configurations, and evaluate their performance on a set of realworld benchmarks where inline pragmas are present. Pragmas may slow down individual programs, but on average improve performance by 10%. Searching for the best configuration on a perprogram basis increases this performance to an average of 27%. Searching for the best configuration for each program is, however, expensive and unrealistic, requiring repeated compilation and execution. This paper determines a new single configuration that gives a 22% improvement on average across the benchmarks. Finally, we use a simple machine learning model that predicts the best configuration on a perprogram basis, giving a 26% average improvement. @InProceedings{Haskell22p81, author = {Celeste Hollenbeck and Michael F. P. O'Boyle and Michel Steuwer}, title = {Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {8194}, doi = {10.1145/3546189.3549918}, year = {2022}, } Publisher's Version 

Papaspyrou, Nikolaos 
Haskell '22: "Coinduction Inductively: Mechanizing ..."
Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
Lykourgos Mastorou , Nikolaos Papaspyrou , and Niki Vazou (National Technical University of Athens, Greece; IMDEA Software Institute, Spain; Google, Germany) Liquid Haskell is an inductive verifier that cannot reason about codata. In this work we present two alternative approaches, namely indexed and constructive coinduction, to consistently encode coinductive proofs in Liquid Haskell. The intuition is that indices can be used to enforce the base case in the setting of classical logic and the guardedness check in the constructive proofs. We use our encodings to machine check 10 coinductive proofs, about unary and binary predicates on infinite streams and lists, showcasing how an inductive verifier can be used to check coinductive properties of Haskell code. @InProceedings{Haskell22p1, author = {Lykourgos Mastorou and Nikolaos Papaspyrou and Niki Vazou}, title = {Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {112}, doi = {10.1145/3546189.3549922}, year = {2022}, } Publisher's Version 

Ribeiro, Rodrigo Geraldo 
Haskell '22: "Open Transactional Actions: ..."
Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell
Jonathas Augusto de Oliveira Conceição , André Rauber Du Bois , Samuel da Silva Feitosa , Gerson Geraldo Homrich Cavalheiro , and Rodrigo Geraldo Ribeiro (Federal University of Pelotas, Brazil; Federal University of Fronteira Sul, Brazil; Federal University of Ouro Preto, Brazil) This paper addresses the problem of accessing external resources from inside transactions in STM Haskell, and for that purpose introduces a new abstraction called Open Transactional Actions (OTAs) that provides a framework for wrapping nontransactional resources in a transactional layer. OTAs allow the programmer to access resources through IO actions, from inside transactions, and also to register commit and abort handlers: the former are used to make the accesses to resources visible to other transactions at commit time, and the latter to undo changes in the resource if the transaction has to roll back. OTAs, once started, are guaranteed to be executed completely before the hosting transaction can be aborted, guarantying that if a resource is accessed, its respective commit and abort actions will be properly registered. We believe that OTAs could be used by expert programmers to implement useful system libraries and also to give a transactional semantics to fast linearizable data structures, i.e., transactional boosting. As a proof of concept, we present examples that use OTAs to implement transactional file access and transactional boosted data types that are faster than pure STM Haskell in most cases. @InProceedings{Haskell22p54, author = {Jonathas Augusto de Oliveira Conceição and André Rauber Du Bois and Samuel da Silva Feitosa and Gerson Geraldo Homrich Cavalheiro and Rodrigo Geraldo Ribeiro}, title = {Open Transactional Actions: Interacting with Nontransactional Resources in STM Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {5465}, doi = {10.1145/3546189.3549924}, year = {2022}, } Publisher's Version Info 

Schrijvers, Tom 
Haskell '22: "Oregano: Staging Regular Expressions ..."
Oregano: Staging Regular Expressions with Moore Cayley Fusion
Jamie Willis , Nicolas Wu , and Tom Schrijvers (Imperial College London, UK; KU Leuven, Belgium) Regular expressions are a tool for recognising regular languages, historically implemented using derivatives or nondeterministic finite automata. They are convenient for many lightweight parsing workloads, but their traditional formulation only lends them to matching text, not returning fullystructured results. This contrasts with other forms of parsing, where the aim is to extract meaningful data, for example abstract syntax trees. Yet, most regular expression libraries do not support this useful output, and those that do are often slower, and backed by parser combinator libraries. This paper presents Oregano, a redesign of regular expressions to make use of Moore machines as the underlying machinery; this way the regular expression matcher can produce results. We further show how to produce heterogeneous results, providing a classic applicative interface. To make this representation performant, we leverage the relationship between Cayley representations, continuationpassing style, and staged metaprogramming to generate performant code for regular expression matching with fullystructured results. @InProceedings{Haskell22p66, author = {Jamie Willis and Nicolas Wu and Tom Schrijvers}, title = {Oregano: Staging Regular Expressions with Moore Cayley Fusion}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {6680}, doi = {10.1145/3546189.3549916}, year = {2022}, } Publisher's Version 

Steuwer, Michel 
Haskell '22: "Investigating Magic Numbers: ..."
Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler
Celeste Hollenbeck , Michael F. P. O'Boyle , and Michel Steuwer (University of Edinburgh, UK) Inlining is a widely studied compiler optimization that is particularly important for functional languages such as Haskell and OCaml. The Glasgow Haskell Compiler (GHC) inliner is a heuristic of such complexity, however, that it has not significantly changed for nearly 20 years. It heavily relies on hardcoded numeric constants, or magic numbers, based on outofdate intuition. Dissatisfaction with inlining performance has led to the widespread use of inlining pragmas by programmers. In this paper, we present an indepth study of the effect of inlining on performance in functional languages. We specifically focus on the inlining behavior of GHC and present techniques to systematically explore the space of possible magic number values, or configurations, and evaluate their performance on a set of realworld benchmarks where inline pragmas are present. Pragmas may slow down individual programs, but on average improve performance by 10%. Searching for the best configuration on a perprogram basis increases this performance to an average of 27%. Searching for the best configuration for each program is, however, expensive and unrealistic, requiring repeated compilation and execution. This paper determines a new single configuration that gives a 22% improvement on average across the benchmarks. Finally, we use a simple machine learning model that predicts the best configuration on a perprogram basis, giving a 26% average improvement. @InProceedings{Haskell22p81, author = {Celeste Hollenbeck and Michael F. P. O'Boyle and Michel Steuwer}, title = {Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {8194}, doi = {10.1145/3546189.3549918}, year = {2022}, } Publisher's Version 

Vazou, Niki 
Haskell '22: "Coinduction Inductively: Mechanizing ..."
Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
Lykourgos Mastorou , Nikolaos Papaspyrou , and Niki Vazou (National Technical University of Athens, Greece; IMDEA Software Institute, Spain; Google, Germany) Liquid Haskell is an inductive verifier that cannot reason about codata. In this work we present two alternative approaches, namely indexed and constructive coinduction, to consistently encode coinductive proofs in Liquid Haskell. The intuition is that indices can be used to enforce the base case in the setting of classical logic and the guardedness check in the constructive proofs. We use our encodings to machine check 10 coinductive proofs, about unary and binary predicates on infinite streams and lists, showcasing how an inductive verifier can be used to check coinductive properties of Haskell code. @InProceedings{Haskell22p1, author = {Lykourgos Mastorou and Nikolaos Papaspyrou and Niki Vazou}, title = {Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {112}, doi = {10.1145/3546189.3549922}, year = {2022}, } Publisher's Version Haskell '22: "How to Safely Use Extensionality ..." How to Safely Use Extensionality in Liquid Haskell Niki Vazou and Michael Greenberg (IMDEA Software Institute, Spain; Stevens Institute of Technology, USA) Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation and port the proofs to an optimized pure implementation that behaves the same. But to reason about higherorder programs, we must reason about equalities between functions: we need a consistent encoding of functional extensionality. A natural but naive phrasing of the functional extensionality axiom (funExt) is inconsistent in refinement type systems with semantic subtyping and polymorphism: if we assume funExt, then we can prove false. We demonstrate the inconsistency and develop a new approach to equality in Liquid Haskell: we define a propositional equality in a library we call PEq. Using PEq avoids the inconsistency while proving useful equalities at higher types; we demonstrate its use in several case studies. We validate PEq by building a model and developing its metatheory. Additionally, we prove metaproperties of PEq inside Liquid Haskell itself using an unnamed folklore technique, which we dub 'classy induction'. @InProceedings{Haskell22p13, author = {Niki Vazou and Michael Greenberg}, title = {How to Safely Use Extensionality in Liquid Haskell}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {1326}, doi = {10.1145/3546189.3549919}, year = {2022}, } Publisher's Version Haskell '22: "Liquid Proof Macros ..." Liquid Proof Macros Henry Blanchette , Niki Vazou , and Leonidas Lampropoulos (University of Maryland at College Park, USA; IMDEA Software Institute, Spain) Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users' burden of proof. However, this power does not come without a price: convincing Liquid Haskell that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell's inner workings. In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tacticinspired DSL interface for more concise and userfriendly proofs, and we demonstrate the capabilities of this framework by automating a wide variety of proofs from an existing Liquid Haskell benchmark. @InProceedings{Haskell22p27, author = {Henry Blanchette and Niki Vazou and Leonidas Lampropoulos}, title = {Liquid Proof Macros}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {2738}, doi = {10.1145/3546189.3549921}, year = {2022}, } Publisher's Version Info 

Willis, Jamie 
Haskell '22: "Oregano: Staging Regular Expressions ..."
Oregano: Staging Regular Expressions with Moore Cayley Fusion
Jamie Willis , Nicolas Wu , and Tom Schrijvers (Imperial College London, UK; KU Leuven, Belgium) Regular expressions are a tool for recognising regular languages, historically implemented using derivatives or nondeterministic finite automata. They are convenient for many lightweight parsing workloads, but their traditional formulation only lends them to matching text, not returning fullystructured results. This contrasts with other forms of parsing, where the aim is to extract meaningful data, for example abstract syntax trees. Yet, most regular expression libraries do not support this useful output, and those that do are often slower, and backed by parser combinator libraries. This paper presents Oregano, a redesign of regular expressions to make use of Moore machines as the underlying machinery; this way the regular expression matcher can produce results. We further show how to produce heterogeneous results, providing a classic applicative interface. To make this representation performant, we leverage the relationship between Cayley representations, continuationpassing style, and staged metaprogramming to generate performant code for regular expression matching with fullystructured results. @InProceedings{Haskell22p66, author = {Jamie Willis and Nicolas Wu and Tom Schrijvers}, title = {Oregano: Staging Regular Expressions with Moore Cayley Fusion}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {6680}, doi = {10.1145/3546189.3549916}, year = {2022}, } Publisher's Version 

Wu, Nicolas 
Haskell '22: "Oregano: Staging Regular Expressions ..."
Oregano: Staging Regular Expressions with Moore Cayley Fusion
Jamie Willis , Nicolas Wu , and Tom Schrijvers (Imperial College London, UK; KU Leuven, Belgium) Regular expressions are a tool for recognising regular languages, historically implemented using derivatives or nondeterministic finite automata. They are convenient for many lightweight parsing workloads, but their traditional formulation only lends them to matching text, not returning fullystructured results. This contrasts with other forms of parsing, where the aim is to extract meaningful data, for example abstract syntax trees. Yet, most regular expression libraries do not support this useful output, and those that do are often slower, and backed by parser combinator libraries. This paper presents Oregano, a redesign of regular expressions to make use of Moore machines as the underlying machinery; this way the regular expression matcher can produce results. We further show how to produce heterogeneous results, providing a classic applicative interface. To make this representation performant, we leverage the relationship between Cayley representations, continuationpassing style, and staged metaprogramming to generate performant code for regular expression matching with fullystructured results. @InProceedings{Haskell22p66, author = {Jamie Willis and Nicolas Wu and Tom Schrijvers}, title = {Oregano: Staging Regular Expressions with Moore Cayley Fusion}, booktitle = {Proc.\ Haskell}, publisher = {ACM}, pages = {6680}, doi = {10.1145/3546189.3549916}, year = {2022}, } Publisher's Version 
29 authors
proc time: 4.76