E3jfnxklhmy4lrlnv3b2
SkillsCast

Write Your Own GHC Type Checker Plugins

11th October 2018 in London at CodeNode

There are 38 other SkillsCasts available from Haskell eXchange 2018

Please log in to watch this conference skillscast.

Https s3.amazonaws.com prod.tracker2 resource 41088130 skillsmatter conference skillscast o9nohu

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.

YOU MAY ALSO LIKE:

Thanks to our sponsors

Write Your Own GHC Type Checker Plugins

Gabe Dijkstra

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.

SkillsCast

Please log in to watch this conference skillscast.

Https s3.amazonaws.com prod.tracker2 resource 41088130 skillsmatter conference skillscast o9nohu

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.

YOU MAY ALSO LIKE:

Thanks to our sponsors

About the Speaker

Write Your Own GHC Type Checker Plugins

Gabe Dijkstra

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.

Photos