Hi Richard,
Thanks very much for your work on this, I think the roles stuff looks quite useful.
I would like to go through another example to make sure I understand this properly.
Consider data V a = V Int (ForeignPtr a), a storable vector, where the Int is the number of elements. We would then want to add 'type role V nominal' as the stored data depends on the Storable instance for the 'a' parameter. Is this correct?
To me it looks like a next step would be a way to specify that two representationally-equal types share a dictionary, and thus could be considered nominally equal for that dictionary. This would mean if we use newtype MkAge = MkAge Int deriving Storable (via GeneralizedNewtypeDeriving), we could then coerce V Int to V MkAge. We don't currently have a way to do this, correct?
Thanks again for all your work on this!
Hi libraries,
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!
Richard
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://www.haskell.org/mailman/listinfo/libraries