Haskell '25: "The Calculated Typer (Functional ..."
The Calculated Typer (Functional Pearl)
Zac Garby, Patrick Bahr, and Graham Hutton
(University of Nottingham, UK; IT University of Copenhagen, Denmark)
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how the calculations can be simplified using fold fusion. This approach enables the compositional derivation of correct-by-construction type checkers based on solving and composing fusion preconditions. We introduce our approach using a simple expression language, to which we then add support for exception handling and checked exceptions.
@InProceedings{Haskell25p17,
author = {Zac Garby and Patrick Bahr and Graham Hutton},
title = {The Calculated Typer (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {17-29},
doi = {10.1145/3759164.3759346},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p6-p doi:10.1145/3759164.3759346
Haskell '25: "Automatic C Bindings Generation ..."
Automatic C Bindings Generation for Haskell
Travis Cardwell, Sam Derbyshire, Edsko de Vries, and Dominik Schrempf
(Well-Typed, UK)
Interfacing Haskell with C libraries is a common necessity, but the manual creation of bindings is both error-prone and laborious. We present hs-bindgen, a new tool that provides fully automatic generation of Haskell FFI bindings directly from C header files.
We introduce a novel method for describing bindings through binding specifications, providing a compositional method for using bindings for one library in bindings for another. Furthermore, we define a domain-specific language in Haskell to represent C expressions found in C macros, along with a corresponding type inference algorithm, to allow us to generate bindings for functions defined as C macros.
@InProceedings{Haskell25p67,
author = {Travis Cardwell and Sam Derbyshire and Edsko de Vries and Dominik Schrempf},
title = {Automatic C Bindings Generation for Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {67-79},
doi = {10.1145/3759164.3759350},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p10-p doi:10.1145/3759164.3759350
Haskell '25: "Plinth: A Plugin-Powered Language ..."
Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, and Manuel Chakravarty
(Input Output, USA; Input Output, UK; Input Output, Netherlands)
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.
Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.
@InProceedings{Haskell25p30,
author = {Ziyang Liu and Kenneth MacKenzie and Roman Kireev and Michael Peyton Jones and Philip Wadler and Manuel Chakravarty},
title = {Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {30-37},
doi = {10.1145/3759164.3759347},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p7-p doi:10.1145/3759164.3759347
Haskell '25: "Automatic C Bindings Generation ..."
Automatic C Bindings Generation for Haskell
Travis Cardwell, Sam Derbyshire, Edsko de Vries, and Dominik Schrempf
(Well-Typed, UK)
Interfacing Haskell with C libraries is a common necessity, but the manual creation of bindings is both error-prone and laborious. We present hs-bindgen, a new tool that provides fully automatic generation of Haskell FFI bindings directly from C header files.
We introduce a novel method for describing bindings through binding specifications, providing a compositional method for using bindings for one library in bindings for another. Furthermore, we define a domain-specific language in Haskell to represent C expressions found in C macros, along with a corresponding type inference algorithm, to allow us to generate bindings for functions defined as C macros.
@InProceedings{Haskell25p67,
author = {Travis Cardwell and Sam Derbyshire and Edsko de Vries and Dominik Schrempf},
title = {Automatic C Bindings Generation for Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {67-79},
doi = {10.1145/3759164.3759350},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p10-p doi:10.1145/3759164.3759350
Haskell '25: "Rebound: Efficient, Expressive, ..."
Rebound: Efficient, Expressive, and Well-Scoped Binding
Noé De Santo and Stephanie Weirich
(University of Pennsylvania, USA)
We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments that map variables to expressions in some new scope. By statically tracking scopes, users of this library gain confidence that they have correctly maintained the subtle invariants that stem from using de Bruijn indices. Behind the scenes, Rebound uses environments to optimize the application of substitutions, while providing explicit access to these data structures when desired. We demonstrate that this library is expressive by using it to implement a wide range of language features with sophisticated uses of binding and several different operations that use this abstract syntax. Our examples include pi-forall, a tutorial implementation of a type checker for a dependently-typed programming language. Finally, we benchmark Rebound to understand its performance characteristics and find that it produces faster code than competing libraries.
@InProceedings{Haskell25p38,
author = {Noé De Santo and Stephanie Weirich},
title = {Rebound: Efficient, Expressive, and Well-Scoped Binding},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {38-52},
doi = {10.1145/3759164.3759348},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p8-p doi:10.1145/3759164.3759348
Haskell '25: "Automatic C Bindings Generation ..."
Automatic C Bindings Generation for Haskell
Travis Cardwell, Sam Derbyshire, Edsko de Vries, and Dominik Schrempf
(Well-Typed, UK)
Interfacing Haskell with C libraries is a common necessity, but the manual creation of bindings is both error-prone and laborious. We present hs-bindgen, a new tool that provides fully automatic generation of Haskell FFI bindings directly from C header files.
We introduce a novel method for describing bindings through binding specifications, providing a compositional method for using bindings for one library in bindings for another. Furthermore, we define a domain-specific language in Haskell to represent C expressions found in C macros, along with a corresponding type inference algorithm, to allow us to generate bindings for functions defined as C macros.
@InProceedings{Haskell25p67,
author = {Travis Cardwell and Sam Derbyshire and Edsko de Vries and Dominik Schrempf},
title = {Automatic C Bindings Generation for Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {67-79},
doi = {10.1145/3759164.3759350},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p10-p doi:10.1145/3759164.3759350
Haskell '25: "A Tale of Two Lambdas: A Haskeller’s ..."
A Tale of Two Lambdas: A Haskeller’s Journey into OCaml (Keynote)
Richard A. Eisenberg
(Jane Street, USA)
After spending a decade focusing mostly on Haskell, I have spent the last three years looking deeply at OCaml. This talk will capture some lessons learned about my work in the two languages and their communities -- how they are similar, how they differ, and how each might usefully grow to become more like the other. I will compare Haskell's purity against OCaml's support for mutation, type classes against modules as abstraction paradigms, laziness against strictness, along with some general thoughts about language philosophy. We'll also touch on the some of the challenges both languages face as open-source products, in need of both volunteers and funding. While some functional programming experience will definitely be helpful, I'll explain syntax as we go -- no Haskell or OCaml knowledge required, as I want this talk to be accessible equally to the two communities.
@InProceedings{Haskell25p2,
author = {Richard A. Eisenberg},
title = {A Tale of Two Lambdas: A Haskeller’s Journey into OCaml (Keynote)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {2-2},
doi = {10.1145/3759164.3771264},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-key2-p doi:10.1145/3759164.3771264
Haskell '25: "A Clash Course in Solving ..."
A Clash Course in Solving Sudoku (Functional Pearl)
Gergő Érdi
(Independent, Singapore)
Clash is a compiler from Haskell to hardware description. We explore a "Haskell-first" approach to hardware design by building an FPGA Sudoku solver based on a well-known software implementation, showing the step-by-step process of adapting it to hardware. The final code still exhibits the benefits of Haskell's powerful tools for abstraction.
@InProceedings{Haskell25p3,
author = {Gergő Érdi},
title = {A Clash Course in Solving Sudoku (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {3-16},
doi = {10.1145/3759164.3759345},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p1-p doi:10.1145/3759164.3759345
Haskell '25: "The Calculated Typer (Functional ..."
The Calculated Typer (Functional Pearl)
Zac Garby, Patrick Bahr, and Graham Hutton
(University of Nottingham, UK; IT University of Copenhagen, Denmark)
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how the calculations can be simplified using fold fusion. This approach enables the compositional derivation of correct-by-construction type checkers based on solving and composing fusion preconditions. We introduce our approach using a simple expression language, to which we then add support for exception handling and checked exceptions.
@InProceedings{Haskell25p17,
author = {Zac Garby and Patrick Bahr and Graham Hutton},
title = {The Calculated Typer (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {17-29},
doi = {10.1145/3759164.3759346},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p6-p doi:10.1145/3759164.3759346
Haskell '25: "The Calculated Typer (Functional ..."
The Calculated Typer (Functional Pearl)
Zac Garby, Patrick Bahr, and Graham Hutton
(University of Nottingham, UK; IT University of Copenhagen, Denmark)
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how the calculations can be simplified using fold fusion. This approach enables the compositional derivation of correct-by-construction type checkers based on solving and composing fusion preconditions. We introduce our approach using a simple expression language, to which we then add support for exception handling and checked exceptions.
@InProceedings{Haskell25p17,
author = {Zac Garby and Patrick Bahr and Graham Hutton},
title = {The Calculated Typer (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {17-29},
doi = {10.1145/3759164.3759346},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p6-p doi:10.1145/3759164.3759346
Haskell '25: "Plinth: A Plugin-Powered Language ..."
Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, and Manuel Chakravarty
(Input Output, USA; Input Output, UK; Input Output, Netherlands)
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.
Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.
@InProceedings{Haskell25p30,
author = {Ziyang Liu and Kenneth MacKenzie and Roman Kireev and Michael Peyton Jones and Philip Wadler and Manuel Chakravarty},
title = {Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {30-37},
doi = {10.1145/3759164.3759347},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p7-p doi:10.1145/3759164.3759347
Haskell '25: "Staging Automatic Differentiation ..."
Staging Automatic Differentiation with Fusion
Samuel Klumpers and Tom Schrijvers
(KU Leuven, Belgium)
Automatic differentiation (AD) is a family of algorithms with many applications in scientific computing and machine learning. They compute numerical derivatives by interpreting or transforming the source code of numeric expressions. The correctness and efficiency of such AD algorithms has been the subject of much research, in particular that of reverse-mode AD which is particularly efficient for computing large gradients, but the code it generates is highly non-obvious.
In this paper, we build on the earlier approach of van den Berg et al. [Science of Computer Programming, 231 (2024)], reverse-engineering their algorithm in terms of established program transformation techniques from abstract algebra and functional programming. We transform the existing interpreter-based approach into an efficient code generator by means of staging with Template Haskell, and leverage a fold fusion variant for staging and algebraic preservation maps to perform correct-by-construction binding time improvements.
The resulting generated code achieves speedups of a factor of 110.
@InProceedings{Haskell25p109,
author = {Samuel Klumpers and Tom Schrijvers},
title = {Staging Automatic Differentiation with Fusion},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {109-123},
doi = {10.1145/3759164.3759353},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p17-p doi:10.1145/3759164.3759353
Haskell '25: "Freer Arrows and Why You Need ..."
Freer Arrows and Why You Need Them in Haskell
Grant VanDomelen, Gan Shen, Lindsey Kuper, and Yao Li
(Portland State University, USA; University of California at Santa Cruz, USA)
Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demonstrate the usefulness of freer arrows in Haskell.
@InProceedings{Haskell25p94,
author = {Grant VanDomelen and Gan Shen and Lindsey Kuper and Yao Li},
title = {Freer Arrows and Why You Need Them in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {94-108},
doi = {10.1145/3759164.3759352},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p13-p doi:10.1145/3759164.3759352
Haskell '25: "Freer Arrows and Why You Need ..."
Freer Arrows and Why You Need Them in Haskell
Grant VanDomelen, Gan Shen, Lindsey Kuper, and Yao Li
(Portland State University, USA; University of California at Santa Cruz, USA)
Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demonstrate the usefulness of freer arrows in Haskell.
@InProceedings{Haskell25p94,
author = {Grant VanDomelen and Gan Shen and Lindsey Kuper and Yao Li},
title = {Freer Arrows and Why You Need Them in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {94-108},
doi = {10.1145/3759164.3759352},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p13-p doi:10.1145/3759164.3759352
Haskell '25: "Plinth: A Plugin-Powered Language ..."
Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, and Manuel Chakravarty
(Input Output, USA; Input Output, UK; Input Output, Netherlands)
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.
Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.
@InProceedings{Haskell25p30,
author = {Ziyang Liu and Kenneth MacKenzie and Roman Kireev and Michael Peyton Jones and Philip Wadler and Manuel Chakravarty},
title = {Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {30-37},
doi = {10.1145/3759164.3759347},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p7-p doi:10.1145/3759164.3759347
Haskell '25: "Lightweight Testing of Persistent ..."
Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad
Anton Lorenzen
(University of Edinburgh, UK)
Persistent data structures are ubiquitous in functional programming languages and their designers frequently have to reason about amortized time complexity. But proving amortized bounds is difficult in a persistent setting, and pen-and-paper proofs give little assurance of correctness, while a full mechanization in a proof assistant can be too involved for the casual user. In this work, we define a strict domain specific language (DSL) for testing the amortized time complexity of persistent data structures using QuickCheck. Our DSL can give strong evidence of correctness, while imposing low overhead on the user. We have used our DSL to check the amortized time complexity of all lazy data structures in Okasaki's book. As a sign of our approach's effectiveness, we re-discovered a previously unreported gap in the analysis of persistent Finger Trees.
@InProceedings{Haskell25p80,
author = {Anton Lorenzen},
title = {Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {80-93},
doi = {10.1145/3759164.3759351},
year = {2025},
}
Publisher's Version
Info
Article: splashws25haskellmain-p11-p doi:10.1145/3759164.3759351
Haskell '25: "Plinth: A Plugin-Powered Language ..."
Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, and Manuel Chakravarty
(Input Output, USA; Input Output, UK; Input Output, Netherlands)
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.
Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.
@InProceedings{Haskell25p30,
author = {Ziyang Liu and Kenneth MacKenzie and Roman Kireev and Michael Peyton Jones and Philip Wadler and Manuel Chakravarty},
title = {Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {30-37},
doi = {10.1145/3759164.3759347},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p7-p doi:10.1145/3759164.3759347
Haskell '25: "Plinth: A Plugin-Powered Language ..."
Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, and Manuel Chakravarty
(Input Output, USA; Input Output, UK; Input Output, Netherlands)
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.
Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.
@InProceedings{Haskell25p30,
author = {Ziyang Liu and Kenneth MacKenzie and Roman Kireev and Michael Peyton Jones and Philip Wadler and Manuel Chakravarty},
title = {Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {30-37},
doi = {10.1145/3759164.3759347},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p7-p doi:10.1145/3759164.3759347
Haskell '25: "Join Points in Practice (Keynote) ..."
Join Points in Practice (Keynote)
Simon Peyton Jones
(Epic Games, UK)
Eight years ago "Compiling without continuations" introduced the idea of so-called join points as a powerful optimisation tool in a functional language compiler. Since then join points have become more and more deeply entwined in GHC's optimisation passes; for example they are treated specially by the Simplifier and its Occurrence Analyser, and a dedicated pass called Exitification makes a join-point-specific transformation
With the perspective of this experience, I am convinced that any serious functional compiler should use join points (or something equivalent): it's a powerful and re-usable idea. Yet beyond the initial paper, none of what we have learned has appeared in print. In this talk I will share the lessons of the last eight years of using join points in practice in GHC.
@InProceedings{Haskell25p1,
author = {Simon Peyton Jones},
title = {Join Points in Practice (Keynote)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {1-1},
doi = {10.1145/3759164.3771263},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-key1-p doi:10.1145/3759164.3771263
Haskell '25: "Automatic C Bindings Generation ..."
Automatic C Bindings Generation for Haskell
Travis Cardwell, Sam Derbyshire, Edsko de Vries, and Dominik Schrempf
(Well-Typed, UK)
Interfacing Haskell with C libraries is a common necessity, but the manual creation of bindings is both error-prone and laborious. We present hs-bindgen, a new tool that provides fully automatic generation of Haskell FFI bindings directly from C header files.
We introduce a novel method for describing bindings through binding specifications, providing a compositional method for using bindings for one library in bindings for another. Furthermore, we define a domain-specific language in Haskell to represent C expressions found in C macros, along with a corresponding type inference algorithm, to allow us to generate bindings for functions defined as C macros.
@InProceedings{Haskell25p67,
author = {Travis Cardwell and Sam Derbyshire and Edsko de Vries and Dominik Schrempf},
title = {Automatic C Bindings Generation for Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {67-79},
doi = {10.1145/3759164.3759350},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p10-p doi:10.1145/3759164.3759350
Haskell '25: "Staging Automatic Differentiation ..."
Staging Automatic Differentiation with Fusion
Samuel Klumpers and Tom Schrijvers
(KU Leuven, Belgium)
Automatic differentiation (AD) is a family of algorithms with many applications in scientific computing and machine learning. They compute numerical derivatives by interpreting or transforming the source code of numeric expressions. The correctness and efficiency of such AD algorithms has been the subject of much research, in particular that of reverse-mode AD which is particularly efficient for computing large gradients, but the code it generates is highly non-obvious.
In this paper, we build on the earlier approach of van den Berg et al. [Science of Computer Programming, 231 (2024)], reverse-engineering their algorithm in terms of established program transformation techniques from abstract algebra and functional programming. We transform the existing interpreter-based approach into an efficient code generator by means of staging with Template Haskell, and leverage a fold fusion variant for staging and algebraic preservation maps to perform correct-by-construction binding time improvements.
The resulting generated code achieves speedups of a factor of 110.
@InProceedings{Haskell25p109,
author = {Samuel Klumpers and Tom Schrijvers},
title = {Staging Automatic Differentiation with Fusion},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {109-123},
doi = {10.1145/3759164.3759353},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p17-p doi:10.1145/3759164.3759353
Haskell '25: "Freer Arrows and Why You Need ..."
Freer Arrows and Why You Need Them in Haskell
Grant VanDomelen, Gan Shen, Lindsey Kuper, and Yao Li
(Portland State University, USA; University of California at Santa Cruz, USA)
Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demonstrate the usefulness of freer arrows in Haskell.
@InProceedings{Haskell25p94,
author = {Grant VanDomelen and Gan Shen and Lindsey Kuper and Yao Li},
title = {Freer Arrows and Why You Need Them in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {94-108},
doi = {10.1145/3759164.3759352},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p13-p doi:10.1145/3759164.3759352
Haskell '25: "Freer Arrows and Why You Need ..."
Freer Arrows and Why You Need Them in Haskell
Grant VanDomelen, Gan Shen, Lindsey Kuper, and Yao Li
(Portland State University, USA; University of California at Santa Cruz, USA)
Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to static analysis. We propose several variants of freer arrows. We conduct a case study on choreographic programming to demonstrate the usefulness of freer arrows in Haskell.
@InProceedings{Haskell25p94,
author = {Grant VanDomelen and Gan Shen and Lindsey Kuper and Yao Li},
title = {Freer Arrows and Why You Need Them in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {94-108},
doi = {10.1145/3759164.3759352},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p13-p doi:10.1145/3759164.3759352
Haskell '25: "Plinth: A Plugin-Powered Language ..."
Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, and Manuel Chakravarty
(Input Output, USA; Input Output, UK; Input Output, Netherlands)
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.
Our journey building Plinth has been unconventional in a number of ways. First, Plinth programs are written in a subset of Haskell, using standard Haskell syntax and types, which brings a number of advantages. Second, compilation is primarily handled by a GHC plugin, one of the most intricate we are aware of. Third, while some compiler optimizations mirror those in Haskell, others diverge significantly to meet on-chain execution constraints. Fourth, Plutus programs run on an instrumented CEK machine with a formal specification in Agda. This report reflects on our design choices, outlining effective practices, challenges, and key takeaways, with an emphasis on recent advances in the language, compiler, and runtime.
@InProceedings{Haskell25p30,
author = {Ziyang Liu and Kenneth MacKenzie and Roman Kireev and Michael Peyton Jones and Philip Wadler and Manuel Chakravarty},
title = {Plinth: A Plugin-Powered Language Built on Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {30-37},
doi = {10.1145/3759164.3759347},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p7-p doi:10.1145/3759164.3759347
Haskell '25: "Total Type Classes ..."
Total Type Classes
Robert Weingart and Nicolas Wu
(Imperial College London, UK)
In Haskell, type classes can act like functions from types to terms. However, unlike for functions, there is no way for the programmer to ask the compiler to verify that classes pattern-match exhaustively on their arguments, and their usage must always be marked by a constraint even when they are exhaustive.
This paper introduces the notion of total type classes and, more generally, total constraints, which allow the programmer to describe a set of instances whose existence can be verified by inspecting the instance declarations of the class, instead of on a case-by-case basis when a specific instance is demanded. To achieve this functionality, our implementation records the missing constraints during typechecking and then modifies the typechecked program, rewriting it as though the programmer had included the constraints.
@InProceedings{Haskell25p53,
author = {Robert Weingart and Nicolas Wu},
title = {Total Type Classes},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {53-66},
doi = {10.1145/3759164.3759349},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p9-p doi:10.1145/3759164.3759349
Haskell '25: "Rebound: Efficient, Expressive, ..."
Rebound: Efficient, Expressive, and Well-Scoped Binding
Noé De Santo and Stephanie Weirich
(University of Pennsylvania, USA)
We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments that map variables to expressions in some new scope. By statically tracking scopes, users of this library gain confidence that they have correctly maintained the subtle invariants that stem from using de Bruijn indices. Behind the scenes, Rebound uses environments to optimize the application of substitutions, while providing explicit access to these data structures when desired. We demonstrate that this library is expressive by using it to implement a wide range of language features with sophisticated uses of binding and several different operations that use this abstract syntax. Our examples include pi-forall, a tutorial implementation of a type checker for a dependently-typed programming language. Finally, we benchmark Rebound to understand its performance characteristics and find that it produces faster code than competing libraries.
@InProceedings{Haskell25p38,
author = {Noé De Santo and Stephanie Weirich},
title = {Rebound: Efficient, Expressive, and Well-Scoped Binding},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {38-52},
doi = {10.1145/3759164.3759348},
year = {2025},
}
Publisher's Version
Article: splashws25haskellmain-p8-p doi:10.1145/3759164.3759348
Haskell '25: "Total Type Classes ..."
Total Type Classes
Robert Weingart and Nicolas Wu
(Imperial College London, UK)
In Haskell, type classes can act like functions from types to terms. However, unlike for functions, there is no way for the programmer to ask the compiler to verify that classes pattern-match exhaustively on their arguments, and their usage must always be marked by a constraint even when they are exhaustive.
This paper introduces the notion of total type classes and, more generally, total constraints, which allow the programmer to describe a set of instances whose existence can be verified by inspecting the instance declarations of the class, instead of on a case-by-case basis when a specific instance is demanded. To achieve this functionality, our implementation records the missing constraints during typechecking and then modifies the typechecked program, rewriting it as though the programmer had included the constraints.
@InProceedings{Haskell25p53,
author = {Robert Weingart and Nicolas Wu},
title = {Total Type Classes},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {53-66},
doi = {10.1145/3759164.3759349},
year = {2025},
}
Publisher's Version
Published Artifact
Artifacts Available
Article: splashws25haskellmain-p9-p doi:10.1145/3759164.3759349