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.
type role Set nominal in the definition of the Set module to prevent the use of GND. (Why that
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 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