HaskellImplementorsWorkshop/2013/Eisenberg

GeneralizedNewtypeDeriving is now type-safe: How "Roles" save the day

Richard A. Eisenberg

The flaw with GeneralizedNewtypeDeriving and how it can cause Haskell programs to crash first made itself known on the GHC Trac with bug #1496 in July 2007. Type safety is compromised because GeneralizedNewtypeDeriving essentially can allow a programmer to equate two distinct types, using either type families or GADTs. The solution to the problem -- known as roles -- was the subject of a POPL 2011 paper, "Generative type abstraction and type-level computation." Roles allow for two distinct notions of equality: representational equality that states that two types have the same representation (but may still be considered different by type families), and nominal equality that states that two types are wholly the same. As roles denote a choice of equality relation, a role is given for every coercion (equality proof) and axiom manipulated by GHC. Roles must also get attached to the type parameters of datatypes, classes and type synonyms, indicating how they use these parameters.

In this talk, I will give an overview of roles, focusing on how roles might affect contributors to GHC and its libraries.