default roles

[Richard Eisenberg]

You raise an excellent point, and yes, your understanding of how roles work in this case is correct.

The problem with your proposal is that it's rather involved to implement and maintain -- essentially, every type and type variable would need to be annotated with both a role and a kind. (These annotations would generally be invisible to users, but quite apparent to implementors.) The current solution is admittedly incomplete in this area, but it requires tracking roles only for parameters to datatypes and classes. We're waiting to see how important this particular issue is in practice before committing to implementing it (a medium-sized project) and maintaining it into perpetuity.

Richard

On Oct 7, 2013, at 3:55 PM, migmit wrote:

> Something bugs me here.
> 
> If some type variable a is used as a parameter to another type variable t, then it's considered nominal. I suppose, that's because it is possible that it would be nominal for some specific t. But we might just know that in our application it's always representational, for every possible t that we would ever use. In this case, we might want to a) explicitly state that t's type parameter should always be representational, and b) at the same time make a representational. Seems like a probable scenario to me.
> 
> ?????????? ? iPad
> 
> 07 ???. 2013 ?., ? 17:26, Richard Eisenberg <eir at cis.upenn.edu> ???????(?):
> 
>> As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.
>> 
>> [1] : http://ghc.haskell.org/trac/ghc/wiki/Roles
>> [2] : http://www.cis.upenn.edu/~eir/papers/2013/roles/roles-slides.pdf
>> 
>> I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:
>> 
>> * If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)
>> 
>> * If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.
>> 
>> Which do we think is better?
>> 
>> Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:
>> 
>> > module Set (Set) where   -- note: no constructors exported!
>> >
>> > data Set a = MkSet [a]
>> > insert :: Ord a => a -> Set a -> Set a
>> > ...
>> 
>> > {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
>> > module Client where
>> >
>> > import Set
>> >
>> > newtype Age = MkAge Int deriving Eq
>> >
>> > instance Ord Age where
>> >   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>> >
>> > class HasSet a where
>> >   getSet :: Set a
>> >
>> > instance HasSet Int where
>> >   getSet = insert 2 (insert 5 empty)
>> >
>> > deriving instance HasSet Age
>> >
>> > good :: Set Int
>> > good = getSet
>> >
>> > bad :: Set Age
>> > bad = getSet
>> 
>> According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.
>> 
>> So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
>> > type role Set nominal
>> in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)
>> 
>> Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
>> > type role Foo representational
>> to allow it.
>> 
>> There are clearly reasons for and against either decision, but which is better? Let the users decide!
>> 
>> Discussion time: 2 weeks.
>> 
>> Thanks!
>> Richard
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20131007/a33a6a0f/attachment-0001.html>