role signatures in libraries

[John Lato]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131127/c8ac62bb/attachment-0001.html>