It has never been easier to do type-level programming in Haskell to capture precise invariants of the values as we are working with. Thanks to extensions such as DataKinds and TypeFamilies, many value-level definitions translate directly to type-level definitions. However, once we have them at the type-level, you often find that GHC's type checker complains about two "obviously" similar expressions not being equal. It may not see that x + 0 and 0 + x are the same for any natural number x.
In this talk, you will see how and why these situations arise, in which the type checker does not spot seemingly obvious equalities between types. You will then learn about GHC's type checker plugins and about when and why it might be worthwhile to write one to address these issues. As an example use case, you will see how such a plugin can be written to implement type-level sets in such a way that using them becomes as frictionless as possible.
Gabe did his PhD in type theory at the University of Nottingham. He now likes putting types to work in the industry to make software more robust and to make writing it more fun.
About the Event: Back for a seventh installment, the Haskell eXchange is an annual conference created for and by the Skills Matter community. An opportunity for Haskellers to meet, learn and share skills, discover emerging technologies and help evolve the Haskell ecosystem. Everyone is welcome to join, whether you are an expert or a beginner, whether you are a commercial user, an academic or a hobbyist, we'd love it if you join us this year at the Haskell eXchange!