Aug 2026· Proceedings of the 19th ACM SIGPLAN International Haskell Symposium· pp. 2-2· 0 citations
TL;DR
The "rebound" library is used to demonstrate and reflect on the current capabilities of dependently-typed programming in Haskell, and supports working with well-scoped de Bruijn indices in abstract syntax trees.
Abstract
Dependent type theory is having a moment as the foundation for interactive provers, such as Lean, Rocq, and Agda. But what does dependent type theory offer to programmers, who just want to get work done? While Haskell is not a full spectrum dependently-typed language, its type system draws inspiration from its features, and provides a playground for experimentation. In this talk, I will use the "rebound" library to demonstrate and reflect on the current capabilities of dependently-typed programming in Haskell. This library supports working with well-scoped de Bruijn indices in abstract syntax trees. Because ASTs statically track their scope depths, type checking program transformations ensures that scopes are properly maintained, a source of subtle bugs in language implementation.
Set-theoretic type connectives with their native support for union, intersection, and negation have the potential to capture the idioms of dynamically typed languages like Erlang. We investigate whether this theoretical expressiveness translates into practice: does the resulting type solver remain tractable on real-wor...
Albert Schimpf, Annette Bieniusa· Proc. ACM Program. Lang.· 1 citation
Tikka is introduced, an interpreter for a carefully-selected subset of Haskell with concise, beginner-friendly error messages, evaluation tracing, and a bespoke IDE.
Alex Hobbs, Alex Dixon· Proceedings of the 19th ACM...· 0 citations
With growing complexity, distributed software systems become increasingly challenging to maintain and reason about. When implementing a distributed protocol, developers must ensure manually that the different components fit together. Choreographic programming addresses this challenge by specifying global protocols in a...
Simon Daniel, Timon Böhler, D. Richter et al.· 0 citations
Over the past two decades, numerous systems have brought some of the benefits of dependent typing to a wide variety of new programming languages, often by restricting which terms can appear inside types. Such techniques are known as refinement types, occurrence typing, liquid types, and path dependent types, among othe...
Yu-Quan Fu, C. Angiuli, Sam Tobin-Hochstadt· 0 citations
We introduce a novel functional-style concurrent programming language called Categorical Message Passing Language (CaMPL) which is designed using the mathematics of linear actegories. This mathematical underpinning gives CaMPL programs useful properties such as deadlock freedom, and additionally, livelock freedom for p...
Robin Cockett, D. Hashimoto, Alexanna Little Berg et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
