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.