role signatures in libraries
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
On Wed, 27 Nov 2013, Richard Eisenberg wrote:
It seems that the syntax and semantics of role annotations has settled, and so it's time to add role annotations to various libraries.
This topic is completely new to me. Where can I read what it is about, what is its motivation?
Henning, Roles were cooked up to address the fact that currently, its possible to derive unsafeCoerce via the use of Generalized Newtype Deriving. Roles address that issue and close that type safety hole. Richard has a paper or so on it, and theres some pretty extensive documentation/examples on the ghc wiki/trac (though perhaps a more extensive exposition for normal haskellers is called for too?) On Wed, Nov 27, 2013 at 1:18 PM, Henning Thielemann < lemming@henning-thielemann.de> wrote:
On Wed, 27 Nov 2013, Richard Eisenberg wrote:
It seems that the syntax and semantics of role annotations has settled,
and so it's time to add role annotations to various libraries.
This topic is completely new to me. Where can I read what it is about, what is its motivation?
_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries
* Carter Schonwald <carter.schonwald@gmail.com> [2013-11-27 14:14:29-0500]
Richard has a paper or so on it, and theres some pretty extensive documentation/examples on the ghc wiki/trac (though perhaps a more extensive exposition for normal haskellers is called for too?)
I find the explanation in Richard's email excellent — very clear and accessible (except that, as Henning noted, it lacks the motivational part). Great job! Roman
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
Hi John, Good questions! On Nov 27, 2013, at 3:35 PM, John Lato wrote:
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?
If you want to be fully safe in the presence of different Storable dictionaries for Age and Int, yes, you should declare `a` to be nominal. However, it's much more likely that Age and Int have the same implementation for Storable, and it might be much more convenient for your users to be able to freely convert between `V Age` and `V Int`. I would say that this is a judgment call -- nominal is safer (always), but representational may be more practical. Note that this is not an issue of type safety, per se. It's much more an issue of type class coherence across newtypes.
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?
That's correct. Extending the roles mechanism in this direction might be a fruitful future direction, but it's not currently on my docket. I'm happy to advise if someone else wants to take this on! Richard
On Mon, Dec 2, 2013 at 3:00 PM, Richard Eisenberg <eir@cis.upenn.edu> wrote:
Hi John,
Good questions!
On Nov 27, 2013, at 3:35 PM, John Lato wrote:
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?
If you want to be fully safe in the presence of different Storable dictionaries for Age and Int, yes, you should declare `a` to be nominal. However, it's much more likely that Age and Int have the same implementation for Storable, and it might be much more convenient for your users to be able to freely convert between `V Age` and `V Int`. I would say that this is a judgment call -- nominal is safer (always), but representational may be more practical.
For the record, I use newtypes to pick out different Storable instances rather a lot, and would find it awfully inconvenient if library authors started assuming otherwise. Anthony
Hi Richard, Thanks for your response. On Mon, Dec 2, 2013 at 12:00 PM, Richard Eisenberg <eir@cis.upenn.edu>wrote:
Hi John,
Good questions!
On Nov 27, 2013, at 3:35 PM, John Lato wrote:
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?
If you want to be fully safe in the presence of different Storable dictionaries for Age and Int, yes, you should declare `a` to be nominal. However, it's much more likely that Age and Int have the same implementation for Storable, and it might be much more convenient for your users to be able to freely convert between `V Age` and `V Int`. I would say that this is a judgment call -- nominal is safer (always), but representational may be more practical.
Although I can't think of any case where I've changed a Storable instance across newtypes, Anthony makes use of this feature and others must also. I think the best thing to do is to make the best use of roles as we currently have them, for the most safety we can get. A no-cost conversion can always be achieved by unsafeCoerce after all.
Note that this is not an issue of type safety, per se. It's much more an issue of type class coherence across newtypes.
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?
That's correct. Extending the roles mechanism in this direction might be a fruitful future direction, but it's not currently on my docket. I'm happy to advise if someone else wants to take this on!
participants (6)
-
Anthony Cowley -
Carter Schonwald -
Henning Thielemann -
John Lato -
Richard Eisenberg -
Roman Cheplyaka