Is it possible to tie the role to whether the data constructor is visible or not?
On 07/10/2013 14:26, Richard Eisenberg wrote: > 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@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
