role signatures in libraries
eir at cis.upenn.edu
Wed Nov 27 18:05:33 UTC 2013
It seems that the syntax and semantics of role annotations has settled, and so it's time to add role annotations to various libraries. Here are the key ideas:
tl;dr: Add nominal role annotations for abstract datatypes whose data has an invariant based on a class instance. Set and Map are top candidates.
- We have three notions of equality: nominal, representational, and phantom.
- Type equality as we know it is called *nominal*.
- A newtype is considered *representationally* equal to its representation type.
* Thus, if we have `newtype Age = MkAge Int`, `Age` and `Int` are representationally equal.
- Any two types are "phantomly" equal.
* See below for an illustrative example of why this notion is useful.
- Every type parameter of every datatype and class is assigned a role. A parameter's role says what notion of equality must hold to show that two instantiations of the datatype are representationally equal.
* Say we have `Bar a` where a's role is nominal. That means that `Bar Age` is *not* representationally equal to `Bar Int`.
* Say we have `Foo a` where a's role is representational. That means that `Foo Age` is representationally equal to `Foo Int`.
* Say we have `Quux a` where a's role is phantom. That means that `Quux Int` is representationally equal to `Quux Bool`.
- Datatype roles are inferred to be the most permissive possible.
* `data Bar a = MkBar (F a)` where `F` is a type family: a's role will be inferred to be nominal.
* `data Foo a = MkFoo a`: a's role will be inferred to be representational.
* `data Quux a = MkQuux String`: a's role will be inferred to be phantom.
- Class roles are inferred to be nominal.
* This choice follows from the idea that the dictionaries for `Ord Int` and `Ord Age` should not be assumed to be the same.
- A role annotation can be used to change a parameter's role. The syntax is a top-level declaration `type role <typename> <list of roles>`. You need the extension RoleAnnotations to use these. Role names are spelled out (nominal, representational, phantom) and are in lower-case.
* If we wanted, say, Quux's parameter's role to be representational, we could say `type role Quux representational`.
- Role annotations must be in the same module as a type is defined in.
- Roles can be left out by inserting `_`. This causes the role to be inferred.
- Role annotations cannot be used to undercut type safety. They are checked to make sure they meet this requirement.
- The new function `coerce` (in GHC.Exts) allows for 0-cost conversion between representationally equal types.
* This means that converting [Quux Bool] to [Quux Int] is now free. This is why phantom equality is interesting.
- You should consider adding a role annotation on any type that has an invariant based on class instances.
* For example, the information stored in a Set is ordered according to the data's Ord instance. So, there should probably be an annotation `type role Set nominal`.
* As a further example, the data stored in a Map cares about the Ord instance of its first parameter but not its second. So, we would probably want `type role Map nominal representational`.
Note that the new roles stuff does *not* allow programmers to do more bad things than they could previously. A sufficiently clever use of GeneralizedNewtypeDeriving could invalidate any instance-based invariants you wished to impose. However, we now have the power to stop these leaks of abstraction. We also have, in `coerce`, an easier way to take advantage of any remaining holes, making it even more important to close the gaps.
The user manual is updated with respect to all the roles stuff -- you may want to see there for more info.
Please let me know if you have any questions about this!
More information about the Libraries