The way I've been describing GND all along has been an abbreviation. GHC does
not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC mints a
fresh dictionary for Ord Age where all the methods are implemented as coerced
versions of the methods for Ord Int. (I'm not sure why it's implemented this
way, which is why I've elided this detail in just about every conversation on
the topic.) With this in mind, I have a proposal:
1) All parameters of all classes have nominal role.
2) Classes also store one extra bit per parameter, saying whether all uses of
that parameter are representational. Essentially, this bit says whether that
parameter is suitable for GND. (Currently, we could just store for the last
parameter, but we can imagine extensions to the GND mechanism for other
parameters.)
Yes, this seems right. And NOW I finally realise why GHC implements GND like
this. Consider
class Show a => C a where { op :: a -> a }
instance C Int where ...
newtype Age = Age Int deriving( Show, C )
Here we want to make a (C Age) dictionary that use the (C Int) version of 'op'.
But the superclass for (Show Age) must not use the (Show Int) version of
'show'! It must use Age's own version of Show.
So we I think Richard's proposal is spot on. Go for it. Can you work on
that, Richard?
Simon
From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org]
On Behalf Of Richard Eisenberg
Sent: 09 October 2013 20:21
To: Edward Kmett
Cc: Simon Peyton-Jones; glasgow-haskell-users@haskell.org Mailing List
Subject: Re: default roles
Now I think we're on the same page, and I *am* a little worried about the sky
falling because of this. (That's not a euphemism -- I'm only a little worried.)
Well, maybe I should be more worried.
The whole idea of roles is to protect against type-unsoundness. They are doing
a great job of that here -- no problem that we've discussed in this thread is a
threat against type safety.
The issue immediately at hand is about coherence (or perhaps you call it
confluence) of instances. Roles do not address the issue of coherence at all,
and thus they fail to protect against coherence attacks. It would take More
Thought to reformulate roles (or devise something else) to handle coherence.
It's worth pointing out that this isn't a new problem, exactly. Bug #8338 shows
a way to produce incoherence using only the GADTs extension. (It does need 4
modules, though.) I conjecture that incoherence is also possible through
GeneralizedNewtypeDeriving, both as it existed in GHC 7.6.3 and in 7.8, so it's
not an issue with Coercible, exactly. It's just that Coercible allows you to
get incoherence with so much less fuss than before!
Wait! I have an idea!
The way I've been describing GND all along has been an abbreviation. GHC does
not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC mints a
fresh dictionary for Ord Age where all the methods are implemented as coerced
versions of the methods for Ord Int. (I'm not sure why it's implemented this
way, which is why I've elided this detail in just about every conversation on
the topic.) With this in mind, I have a proposal:
1) All parameters of all classes have nominal role.
2) Classes also store one extra bit per parameter, saying whether all uses of
that parameter are representational. Essentially, this bit says whether that
parameter is suitable for GND. (Currently, we could just store for the last
parameter, but we can imagine extensions to the GND mechanism for other
parameters.)
Because GND is implemented using coercions on each piece instead of wholesale,
the nominal roles on classes won't get in the way of proper use of GND. An
experiment (see below for details) also confirms that even superclasses work
well with this idea -- the superclasses aren't coerced.
Under this proposal, dictionaries can never be coerced, but GND would still
seem to work.
Thoughts?
Richard
Experiment:
newtype Age = MkAge Int
instance Eq Age where
_ == _ = False
deriving instance Ord Age
useOrdInstance :: Ord a => a -> Bool
useOrdInstance x = (x == x)
What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD). This
means that the existing GND mechanism (I didn't change anything around this
part of the code) uses superclass instances for the *newtype*, not for the
*base type*. So, even with superclasses, class dictionaries don't need to be
coerced.
On Oct 9, 2013, at 2:52 PM, Edward Kmett
mailto:ekm...@gmail.com>> wrote:
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 generat
