Re: default roles

9 Oct 2013

      I'd be happy to be wrong. =)

We do seem to have stumbled into a design paradox though.

To make it so you can use roles in GeneralizedNewtypeDeriving hinges on the
parameter's role being representational, but making it representational
means users can also use coerce to turn dictionaries into other
dictionaries outside of GND.

This is quite insidious, as another dictionary for Eq or Ord may exist for
that type, where it becomes unsound as the generated dictionary may be used
to destroy confluence.

This means that even if something like Set has a nominal argument it isn't
safe, because you can attack the invariants of the structure via Ord.

newtype Bad = Bad Int deriving Eq
instance Ord Bad where
   compare (Bad a) (Bad b) = compare b a

If Ord has a representational role then I can use coerce to convert a
dictonary Ord Bad to Ord Int, then work locally in a context where that is
the dictionary for Ord Int that I get when I go to do an insert or lookup.

I don't mean to sound like the sky is falling, but I do worry that the 'use
of a constraint in a data type' may not be necessary or sufficient. That is
a lot of surface area to defend against attack.

I am not sure that I actually need a data type to coerce a dictionary. It
seems likely that I could do it with just a well crafted function argument
and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the
moment to give it a try.

-Edward

On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg  wrote:
...
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  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 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 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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users