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 <e...@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@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
