I don't quite agree with your analysis, Edward.

Eq can be auto-derived, so it makes for a confusing example. Let's replace Eq 
in your example with this class:

> class C a where
>  c_meth :: a -> a -> Bool

Then, your example leads to the same embarrassing state of affairs: coercing a 
dictionary for (C Int) to one for (C Bar).

But, I would argue that we still want C's parameter to have a representational 
role. Why? Consider this:

> data Blargh = ...
> instance C Blargh where ...
>
> newtype Baz = MkBaz Blargh deriving C

We want that last line to work, using GeneralizedNewtypeDeriving. This hinges 
on C's parameter's role being representational.

I think that what you've witnessed is a case of bug #8338 
(http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my view, 
and it seems to touch on roles, but I'm not completely sure of their 
relationship.

So, I think that classes should keep their representational roles (regardless 
of the decision on datatypes -- Haskell doesn't really support "abstract" 
classes), but perhaps we have to find a way to stop these incoherent instances 
from forming. Maybe the use of a constraint makes a datatype's role be nominal?

Richard

On Oct 9, 2013, at 1:55 PM, Edward Kmett <ekm...@gmail.com> wrote:

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

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply via email to