default roles

Wed Oct 9 17:55:30 UTC 2013

I just noticed there is a pretty big issue with the current default role
where typeclasses are concerned!

When implementing Data.Type.Coercion I had to use the fact that I could
apply coerce to the arguments of

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

This makes sense as Coercion itself has two representational arguments.

This struck me as quite clever, so I went to test it further.

data Foo a where
   Foo :: Eq a => Foo a

newtype Bar = Bar Int
instance Eq Bar where
  _ == _ = False

I fully expected the following to fail:

coerce (Foo :: Foo Int) :: Foo Bar

but instead it succeeded.

This means I was able to convert a dictionary Eq Int into a dictionary for Eq
Bar!

This indicates that Eq (actually all) of the typeclasses are currently
marked as having representational, when actually it strikes me that
(almost?) none of them should be.

Coercible is the only case I can think of in base of a class with two
representational arguments, but this is only valid because we prevent users
from defining Coercible instances manually.

If I try again with a new typeclass that has an explicit nominal role

type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd
expect.

This indicates two big issues to me:

1.) At the very least the default role for type *classes* should be nominal
for each argument. The very point of an instance is to make a nominal
distinction after all. =)

2.) It also indicates that making any typeclass with a representational (/
phantom?) argument shouldn't be possible in valid SafeHaskell, as you can
use it to subvert the current restrictions on OverlappingInstances.

-Edward

On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki <iavor.diatchki at gmail.com>wrote:

> Hello,
>
> My preference would be for the following design:
>
> 1. The default datatypes for roles are Nominal, but programmers can add
> annotations to relax this.
> 2. Generlized newtype deriving works as follows:  we can coerce a
> dictionary for `C R` into `C T`, as long as we can coerce the types of all
> methods instantiated with `R`, into the corresponding types instantiated
> with `T`.  In other words, we are pretending that we are implementing all
> methods by using `coerce`.
>
> As far as I can see this safe, and matches what I'd expect as a
> programmer.  It also solves the problem with the `Set` example: because
> `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge`
> and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added
> benefit of this approach is that when newtype deriving fails, we can give a
> nicer error saying exactly which method causes the problem.
>
> -Iavor
>
>
>
>
>
>
> On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir at cis.upenn.edu>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
>>
>>
>
> _______________________________________________
> 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/20131009/30d07763/attachment.html>