default roles

[Richard Eisenberg]

We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.

Richard

On Oct 7, 2013, at 4:33 PM, Ganesh Sittampalam <ganesh at earth.li> wrote:

> 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>> 
>