[Haskell'26] What Have We Learned about Dependently Typed Programming from Haskell? (Keynote)

What Have We Learned about Dependently Typed Programming from Haskell? (Keynote) (Video, Haskell 2026) Stephanie Weirich (University of Pennsylvania, USA) 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. Article: https://doi.org/10.1145/3830439.3839121 ORCID: https://orcid.org/0000-0002-6756-9168 Video Tags: doi:10.1145/3830439.3839121, orcid:0000-0002-6756-9168 Presentation at the Haskell 2026 symposium, August 28-29, 2026, https://icfp26.sigplan.org/home/haskellsymp-2026 Sponsored by ACM SIGPLAN.