Haskell '26: "CloudMicroHaskell: Direct-Style ..."
CloudMicroHaskell: Direct-Style Distributed Haskell via Runtime Graph Serialisation
Robert Krook and Lennart Augustsson
(Chalmers University of Technology and University of Gothenburg, Sweden; Unaffiliated, Sweden)
Cloud Haskell brings Erlang-style distributed programming to Haskell, but its treatment of mobile code exposes a difficult boundary in the source-level API. Remote processes must be expressed as static closures, messages must satisfy serialisation constraints, and participating nodes are assumed to share the relevant code.
This paper explores a different design point. We present CloudMicroHaskell, a Cloud Haskell-style library built on MicroHaskell, whose runtime represents both code and data as a combinator graph. When a process or message crosses a node boundary, CloudMicroHaskell serialises the reachable graph directly. As a result, remote spawning can be written in direct style: process bodies may capture variables from their surrounding scope, and messages may contain ordinary values, including functions, without programmer-written closure conversion.
We describe the implementation of the MicroCloudHaskell node runtime, including remote spawn, message delivery, monitors, exit propagation, and library implementations of generic servers and supervisors. We evaluate the system with process/message benchmarks, a distributed work-pool benchmark, a file-synchronisation case study, and a heterogeneous deployment on microcontrollers. The results show that runtime graph serialisation makes the Cloud Haskell programming model substantially more direct, while also making the tradeoff explicit: some guarantees enforced by Cloud Haskell's source-level types become dynamic checks, and programmers must be aware of laziness and runtime-owned resources when moving graphs between nodes.
Article Search
Article: icfpws26haskellmain-p8-p doi:10.1145/3830439.3831272
Haskell '26: "Tikka: An Interpreter and ..."
Tikka: An Interpreter and Debugger for a Pedagogical Subset of Haskell
Alex Hobbs and Alex Dixon
(University of Warwick, UK)
Functional programming is a core part of many undergraduate-level courses in Computer Science. Pedagogical interest in Haskell continues to grow as functional idioms become commonplace in popular multi-paradigm languages. The Glasgow Haskell Compiler (GHC) is by far Haskell’s most used compiler, but can hinder students’ initial learning because of its detailed and verbose error messages which are designed to support experienced users and cover a broad language surface. In this paper we introduce Tikka, an interpreter for a carefully-selected subset of Haskell with concise, beginner-friendly error messages, evaluation tracing, and a bespoke IDE. This paper discusses the design of an interpreter targeted towards novice users, and presents an evaluation of its use in practice through user testing and a side-by-side comparison of GHC and Tikka.
Article Search
Article: icfpws26haskellmain-p48-p doi:10.1145/3830439.3831274
Haskell '26: "Coercive Subtyping for Implicit ..."
Coercive Subtyping for Implicit Functorial Programming
Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, and Aaron Stump
(Boston College, USA; Johns Hopkins University, USA)
Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these operations using a coercive subtyping discipline and study the metatheory of the resulting algebra of coercions. For functors, we promote the fmap combinator of type (A → B) → F A → F B to a coercion A → B ≤ F A → F B. We incorporate it into a monomorphic system of coercions for base types, arrow types, and functor types. We prove that the resulting system of coercions is coherent, meaning that all possible choices of coercions from A to B end up equivalent. The proof of the theorem is based on coherence by evaluation, an approach to coherence proofs based on the well-known technique of normalization by evaluation. All definitions and theorems in the paper are checked in Agda, which played a valuable role in the design of the system.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p23-p doi:10.1145/3830439.3831273
Haskell '26: "Turning Parser Errors into ..."
Turning Parser Errors into Suggestions for REPL-Driven DSLs (Functional Pearl)
Matthías Páll Gissurarson, Elisabet Lobo-Vesga, and Alejandro Russo
(DPella, Gothenburg, Sweden; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Many of the domain-specific languages we use every day are not written to files but typed at an interactive prompt, e.g., database shells, cloud CLIs, and in-house analytics consoles. For these REPL-driven command languages, autocomplete is, we argue, not a polish feature but a core usability requirement --and yet they are precisely the languages whose authors often have the fewest resources to invest in tooling. Designing a new programming language tailored to specific domain challenges can be both powerful and rewarding. However, a major hurdle for adoption among users is, in our experience, the lack of tooling support, particularly features like autocomplete that enhance usability and reduce the learning curve. In this paper, we present a fresh perspective that turns parser errors -- traditionally seen as roadblocks -- into opportunities for generating valid, context-aware autocomplete suggestions. By leveraging the parser's built-in feedback mechanisms, our method offers a lightweight, adaptable, and simple solution, enabling domain-specific languages to provide basic development assistance with minimal overhead. The technique fits the REPL-driven DSL genre by design: inputs are modest-size single statements, the cursor sits at the end of the line, and parser-error recovery is unnecessary. We apply the technique to DPella DSL, a production REPL-driven DSL whose grammar comprises 43 top-level command constructors, 130 reserved keywords, and 22 labelled syntactic categories that drive identifier completion.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p69-p doi:10.1145/3830439.3831275
Haskell '26: "A Cost-Aware Probability Monad ..."
A Cost-Aware Probability Monad for Liquid Haskell
Matthias Hetzenberger, Georg Moser, and Florian Zuleger
(TU Wien, Austria; University of Innsbruck, Austria; TU München, Germany)
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributions, expectations, and recursive stochastic behaviour. Existing formal approaches frequently require substantial manual proof effort, since expected costs are often encoded separately from probabilistic computations and must therefore be propagated explicitly throughout proofs.
In this paper, we present a cost-aware probability monad for Liquid Haskell that supports reasoning about probabilistic programs together with their expected costs. Our approach combines executable probabilistic programs with refinement-type-based verification and SMT-supported automation. The monad intrinsically tracks probability mass, expected values, and expected costs through refinement types, enabling many quantitative properties of probabilistic computations to be inferred compositionally from program structure.
We evaluate our approach on several classical probabilistic algorithms and data structures, including meldable heaps, randomised quicksort and quickselect, randomised splay trees, random permutations, and the hiring problem. The case studies demonstrate different points along the spectrum between automated and interactive verification.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p90-p doi:10.1145/3830439.3831276
Haskell '26: "Tikka: An Interpreter and ..."
Tikka: An Interpreter and Debugger for a Pedagogical Subset of Haskell
Alex Hobbs and Alex Dixon
(University of Warwick, UK)
Functional programming is a core part of many undergraduate-level courses in Computer Science. Pedagogical interest in Haskell continues to grow as functional idioms become commonplace in popular multi-paradigm languages. The Glasgow Haskell Compiler (GHC) is by far Haskell’s most used compiler, but can hinder students’ initial learning because of its detailed and verbose error messages which are designed to support experienced users and cover a broad language surface. In this paper we introduce Tikka, an interpreter for a carefully-selected subset of Haskell with concise, beginner-friendly error messages, evaluation tracing, and a bespoke IDE. This paper discusses the design of an interpreter targeted towards novice users, and presents an evaluation of its use in practice through user testing and a side-by-side comparison of GHC and Tikka.
Article Search
Article: icfpws26haskellmain-p48-p doi:10.1145/3830439.3831274
Haskell '26: "Evaluating Shrinking (Experience ..."
Evaluating Shrinking (Experience Report)
Alperen Keles, George Miao, and Leonidas Lampropoulos
(University of Maryland, College Park, USA)
Property-based testing frameworks rely on shrinking to turn noisy random failures into counterexamples that developers can debug. Although bug-finding performance is routinely measured, shrinking itself is rarely evaluated quantitatively. We present an experience report on evaluating shrinking across three Haskell frameworks: QuickCheck, Hedgehog, and Falsify. The comparison spans four ETNA workloads and several generator families, including type-based, API-based, and correct-by-construction generators. We measure both effectiveness, using tree edit distance to a ground-truth minimum found by exhaustive search, and cost, using shrink time and time per unit of shrinking progress. Across these workloads, QuickCheck's structural shrinking is usually faster and remains competitive on final counterexample quality; integrated shrinking does not by itself guarantee a performance or effectiveness advantage. We discuss what these results imply for future evaluations and designs of shrinking algorithms.
Article Search
Article: icfpws26haskellmain-p4-p doi:10.1145/3830439.3831271
Haskell '26: "CloudMicroHaskell: Direct-Style ..."
CloudMicroHaskell: Direct-Style Distributed Haskell via Runtime Graph Serialisation
Robert Krook and Lennart Augustsson
(Chalmers University of Technology and University of Gothenburg, Sweden; Unaffiliated, Sweden)
Cloud Haskell brings Erlang-style distributed programming to Haskell, but its treatment of mobile code exposes a difficult boundary in the source-level API. Remote processes must be expressed as static closures, messages must satisfy serialisation constraints, and participating nodes are assumed to share the relevant code.
This paper explores a different design point. We present CloudMicroHaskell, a Cloud Haskell-style library built on MicroHaskell, whose runtime represents both code and data as a combinator graph. When a process or message crosses a node boundary, CloudMicroHaskell serialises the reachable graph directly. As a result, remote spawning can be written in direct style: process bodies may capture variables from their surrounding scope, and messages may contain ordinary values, including functions, without programmer-written closure conversion.
We describe the implementation of the MicroCloudHaskell node runtime, including remote spawn, message delivery, monitors, exit propagation, and library implementations of generic servers and supervisors. We evaluate the system with process/message benchmarks, a distributed work-pool benchmark, a file-synchronisation case study, and a heterogeneous deployment on microcontrollers. The results show that runtime graph serialisation makes the Cloud Haskell programming model substantially more direct, while also making the tradeoff explicit: some guarantees enforced by Cloud Haskell's source-level types become dynamic checks, and programmers must be aware of laziness and runtime-owned resources when moving graphs between nodes.
Article Search
Article: icfpws26haskellmain-p8-p doi:10.1145/3830439.3831272
Haskell '26: "Coercive Subtyping for Implicit ..."
Coercive Subtyping for Implicit Functorial Programming
Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, and Aaron Stump
(Boston College, USA; Johns Hopkins University, USA)
Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these operations using a coercive subtyping discipline and study the metatheory of the resulting algebra of coercions. For functors, we promote the fmap combinator of type (A → B) → F A → F B to a coercion A → B ≤ F A → F B. We incorporate it into a monomorphic system of coercions for base types, arrow types, and functor types. We prove that the resulting system of coercions is coherent, meaning that all possible choices of coercions from A to B end up equivalent. The proof of the theorem is based on coherence by evaluation, an approach to coherence proofs based on the well-known technique of normalization by evaluation. All definitions and theorems in the paper are checked in Agda, which played a valuable role in the design of the system.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p23-p doi:10.1145/3830439.3831273
Haskell '26: "Evaluating Shrinking (Experience ..."
Evaluating Shrinking (Experience Report)
Alperen Keles, George Miao, and Leonidas Lampropoulos
(University of Maryland, College Park, USA)
Property-based testing frameworks rely on shrinking to turn noisy random failures into counterexamples that developers can debug. Although bug-finding performance is routinely measured, shrinking itself is rarely evaluated quantitatively. We present an experience report on evaluating shrinking across three Haskell frameworks: QuickCheck, Hedgehog, and Falsify. The comparison spans four ETNA workloads and several generator families, including type-based, API-based, and correct-by-construction generators. We measure both effectiveness, using tree edit distance to a ground-truth minimum found by exhaustive search, and cost, using shrink time and time per unit of shrinking progress. Across these workloads, QuickCheck's structural shrinking is usually faster and remains competitive on final counterexample quality; integrated shrinking does not by itself guarantee a performance or effectiveness advantage. We discuss what these results imply for future evaluations and designs of shrinking algorithms.
Article Search
Article: icfpws26haskellmain-p4-p doi:10.1145/3830439.3831271
Haskell '26: "Turning Parser Errors into ..."
Turning Parser Errors into Suggestions for REPL-Driven DSLs (Functional Pearl)
Matthías Páll Gissurarson, Elisabet Lobo-Vesga, and Alejandro Russo
(DPella, Gothenburg, Sweden; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Many of the domain-specific languages we use every day are not written to files but typed at an interactive prompt, e.g., database shells, cloud CLIs, and in-house analytics consoles. For these REPL-driven command languages, autocomplete is, we argue, not a polish feature but a core usability requirement --and yet they are precisely the languages whose authors often have the fewest resources to invest in tooling. Designing a new programming language tailored to specific domain challenges can be both powerful and rewarding. However, a major hurdle for adoption among users is, in our experience, the lack of tooling support, particularly features like autocomplete that enhance usability and reduce the learning curve. In this paper, we present a fresh perspective that turns parser errors -- traditionally seen as roadblocks -- into opportunities for generating valid, context-aware autocomplete suggestions. By leveraging the parser's built-in feedback mechanisms, our method offers a lightweight, adaptable, and simple solution, enabling domain-specific languages to provide basic development assistance with minimal overhead. The technique fits the REPL-driven DSL genre by design: inputs are modest-size single statements, the cursor sits at the end of the line, and parser-error recovery is unnecessary. We apply the technique to DPella DSL, a production REPL-driven DSL whose grammar comprises 43 top-level command constructors, 130 reserved keywords, and 22 labelled syntactic categories that drive identifier completion.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p69-p doi:10.1145/3830439.3831275
Haskell '26: "Evaluating Shrinking (Experience ..."
Evaluating Shrinking (Experience Report)
Alperen Keles, George Miao, and Leonidas Lampropoulos
(University of Maryland, College Park, USA)
Property-based testing frameworks rely on shrinking to turn noisy random failures into counterexamples that developers can debug. Although bug-finding performance is routinely measured, shrinking itself is rarely evaluated quantitatively. We present an experience report on evaluating shrinking across three Haskell frameworks: QuickCheck, Hedgehog, and Falsify. The comparison spans four ETNA workloads and several generator families, including type-based, API-based, and correct-by-construction generators. We measure both effectiveness, using tree edit distance to a ground-truth minimum found by exhaustive search, and cost, using shrink time and time per unit of shrinking progress. Across these workloads, QuickCheck's structural shrinking is usually faster and remains competitive on final counterexample quality; integrated shrinking does not by itself guarantee a performance or effectiveness advantage. We discuss what these results imply for future evaluations and designs of shrinking algorithms.
Article Search
Article: icfpws26haskellmain-p4-p doi:10.1145/3830439.3831271
Haskell '26: "A Cost-Aware Probability Monad ..."
A Cost-Aware Probability Monad for Liquid Haskell
Matthias Hetzenberger, Georg Moser, and Florian Zuleger
(TU Wien, Austria; University of Innsbruck, Austria; TU München, Germany)
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributions, expectations, and recursive stochastic behaviour. Existing formal approaches frequently require substantial manual proof effort, since expected costs are often encoded separately from probabilistic computations and must therefore be propagated explicitly throughout proofs.
In this paper, we present a cost-aware probability monad for Liquid Haskell that supports reasoning about probabilistic programs together with their expected costs. Our approach combines executable probabilistic programs with refinement-type-based verification and SMT-supported automation. The monad intrinsically tracks probability mass, expected values, and expected costs through refinement types, enabling many quantitative properties of probabilistic computations to be inferred compositionally from program structure.
We evaluate our approach on several classical probabilistic algorithms and data structures, including meldable heaps, randomised quicksort and quickselect, randomised splay trees, random permutations, and the hiring problem. The case studies demonstrate different points along the spectrum between automated and interactive verification.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p90-p doi:10.1145/3830439.3831276
Haskell '26: "Coercive Subtyping for Implicit ..."
Coercive Subtyping for Implicit Functorial Programming
Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, and Aaron Stump
(Boston College, USA; Johns Hopkins University, USA)
Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these operations using a coercive subtyping discipline and study the metatheory of the resulting algebra of coercions. For functors, we promote the fmap combinator of type (A → B) → F A → F B to a coercion A → B ≤ F A → F B. We incorporate it into a monomorphic system of coercions for base types, arrow types, and functor types. We prove that the resulting system of coercions is coherent, meaning that all possible choices of coercions from A to B end up equivalent. The proof of the theorem is based on coherence by evaluation, an approach to coherence proofs based on the well-known technique of normalization by evaluation. All definitions and theorems in the paper are checked in Agda, which played a valuable role in the design of the system.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p23-p doi:10.1145/3830439.3831273
Haskell '26: "Turning Parser Errors into ..."
Turning Parser Errors into Suggestions for REPL-Driven DSLs (Functional Pearl)
Matthías Páll Gissurarson, Elisabet Lobo-Vesga, and Alejandro Russo
(DPella, Gothenburg, Sweden; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Many of the domain-specific languages we use every day are not written to files but typed at an interactive prompt, e.g., database shells, cloud CLIs, and in-house analytics consoles. For these REPL-driven command languages, autocomplete is, we argue, not a polish feature but a core usability requirement --and yet they are precisely the languages whose authors often have the fewest resources to invest in tooling. Designing a new programming language tailored to specific domain challenges can be both powerful and rewarding. However, a major hurdle for adoption among users is, in our experience, the lack of tooling support, particularly features like autocomplete that enhance usability and reduce the learning curve. In this paper, we present a fresh perspective that turns parser errors -- traditionally seen as roadblocks -- into opportunities for generating valid, context-aware autocomplete suggestions. By leveraging the parser's built-in feedback mechanisms, our method offers a lightweight, adaptable, and simple solution, enabling domain-specific languages to provide basic development assistance with minimal overhead. The technique fits the REPL-driven DSL genre by design: inputs are modest-size single statements, the cursor sits at the end of the line, and parser-error recovery is unnecessary. We apply the technique to DPella DSL, a production REPL-driven DSL whose grammar comprises 43 top-level command constructors, 130 reserved keywords, and 22 labelled syntactic categories that drive identifier completion.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p69-p doi:10.1145/3830439.3831275
Haskell '26: "Coercive Subtyping for Implicit ..."
Coercive Subtyping for Implicit Functorial Programming
Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, and Aaron Stump
(Boston College, USA; Johns Hopkins University, USA)
Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these operations using a coercive subtyping discipline and study the metatheory of the resulting algebra of coercions. For functors, we promote the fmap combinator of type (A → B) → F A → F B to a coercion A → B ≤ F A → F B. We incorporate it into a monomorphic system of coercions for base types, arrow types, and functor types. We prove that the resulting system of coercions is coherent, meaning that all possible choices of coercions from A to B end up equivalent. The proof of the theorem is based on coherence by evaluation, an approach to coherence proofs based on the well-known technique of normalization by evaluation. All definitions and theorems in the paper are checked in Agda, which played a valuable role in the design of the system.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p23-p doi:10.1145/3830439.3831273
Haskell '26: "Coercive Subtyping for Implicit ..."
Coercive Subtyping for Implicit Functorial Programming
Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, and Aaron Stump
(Boston College, USA; Johns Hopkins University, USA)
Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these operations using a coercive subtyping discipline and study the metatheory of the resulting algebra of coercions. For functors, we promote the fmap combinator of type (A → B) → F A → F B to a coercion A → B ≤ F A → F B. We incorporate it into a monomorphic system of coercions for base types, arrow types, and functor types. We prove that the resulting system of coercions is coherent, meaning that all possible choices of coercions from A to B end up equivalent. The proof of the theorem is based on coherence by evaluation, an approach to coherence proofs based on the well-known technique of normalization by evaluation. All definitions and theorems in the paper are checked in Agda, which played a valuable role in the design of the system.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p23-p doi:10.1145/3830439.3831273
Haskell '26: "A Cost-Aware Probability Monad ..."
A Cost-Aware Probability Monad for Liquid Haskell
Matthias Hetzenberger, Georg Moser, and Florian Zuleger
(TU Wien, Austria; University of Innsbruck, Austria; TU München, Germany)
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributions, expectations, and recursive stochastic behaviour. Existing formal approaches frequently require substantial manual proof effort, since expected costs are often encoded separately from probabilistic computations and must therefore be propagated explicitly throughout proofs.
In this paper, we present a cost-aware probability monad for Liquid Haskell that supports reasoning about probabilistic programs together with their expected costs. Our approach combines executable probabilistic programs with refinement-type-based verification and SMT-supported automation. The monad intrinsically tracks probability mass, expected values, and expected costs through refinement types, enabling many quantitative properties of probabilistic computations to be inferred compositionally from program structure.
We evaluate our approach on several classical probabilistic algorithms and data structures, including meldable heaps, randomised quicksort and quickselect, randomised splay trees, random permutations, and the hiring problem. The case studies demonstrate different points along the spectrum between automated and interactive verification.
Article Search
Artifacts Available
Article: icfpws26haskellmain-p90-p doi:10.1145/3830439.3831276