Recent versions of the Haskell compiler GHC have a number of advanced features that allow many idioms from dependently typed programming to be encoded. We describe our experiences using this "dependently typed Haskell'' to construct a performance-critical library that is a key component in a number of verification tools. We have discovered that it can be done, and it brings significant value, but also at a high cost. In this experience report, we describe the ways in which programming at the edge of what is expressible in Haskell’s type system has brought value, the difficulties that it has imposed, and some of the ways we coped with the difficulties.
Tue 20 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:20 - 16:30
|Dependently Typed Haskell in Industry (Experience Report)
|A Role for Dependent Types in Haskell
|Higher-order Type-level Programming in Haskell