Please log in to watch this conference skillscast.
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
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.
YOU MAY ALSO LIKE:
Write Your Own GHC Type Checker Plugins
Gabe Dijkstra is Haskell programmer living in London. 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.