dep typed haskell

Dependently Typed Haskell in Industry

https://dl.acm.org/doi/10.1145/3341704

This an extensive experience report from Galois about their use of advanced Haskell's type system features, like data kinds, higher-kinded types of all sort, type families, type-level natural arithmetics, lists, maps...

These features were used while developing a tool called Crucible for simulating imperative languages and runtime systems. By transforming programs into some Crucible expressions, simulations can be run and properties asserted thus providing high-assurance guarantees on low-level programs.

The net outcome of the experience can be summarised as:

• There's a high upfront cost to pay to use those features in an industrial-strengrth system, in terms of code size, additional tooling, training of developers, cognitive load, support code creation, GHC evolutions tracking...
• There are inherent limitations in Haskell TS that makes it necessary to fallback to value-level checks which unavoidably leads to errors and bugs
• This effort pays off in the long run through the assurance it provides both in the use of the tool and its maintenance cost: Strong type discipline makes refactoring safer as breaking changes are caught earlier in the development lifecycle
• Haskell is still better than pure DT languages because of the extensive ecosystem

Based on our experience [..] we believe that hte benefits of low-stress refactoring and confidence in the system's correctness have been worth the considerable costs of employing dependent Haskell in Crucible