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! On Nov 27, 2013 10:05 AM, "Richard Eisenberg" <eir@cis.upenn.edu> wrote:
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