[Haskell'26] A Cost-Aware Probability Monad for Liquid Haskell

A Cost-Aware Probability Monad for Liquid Haskell (Video, Haskell 2026) Matthias Hetzenberger, Georg Moser, Florian Zuleger (TU Wien, Austria; University of Innsbruck, Austria; TU Wien, Austria / TU München, Germany) Abstract: 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: https://doi.org/10.1145/3830439.3831276 Supplementary archive: https://doi.org/10.5281/zenodo.21397698 (Badges: Artifacts Available) ORCID: https://orcid.org/0000-0002-2052-8772, https://orcid.org/0000-0001-9240-6128, https://orcid.org/0000-0003-1468-8398 Video Tags: Liquid Haskell, probabilistic algorithms and data structures, doi:10.1145/3830439.3831276, doi:10.5281/zenodo.21397698, orcid:0000-0002-2052-8772, orcid:0000-0001-9240-6128, orcid:0000-0003-1468-8398, Artifacts Available Presentation at the Haskell 2026 symposium, August 28-29, 2026, https://icfp26.sigplan.org/home/haskellsymp-2026 Sponsored by ACM SIGPLAN.