Does GND make sense in cases where the superclasses aren't also derived? If I
had a type T whose Ord instance made use of the Eq instance for some reason,
and then I made a newtype T' with a new Eq instance and a GND Ord instance, the
calls to (==) in the Ord instance will refer to the T implementation, right?
Yes, absolutely.
class Show a => C a where
op :: a -> a
You might want to use GND for the (C Age) instance, but NOT use GND for the
Show instance.
Simon
From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org]
On Behalf Of David Menendez
Sent: 10 October 2013 16:25
To: Richard Eisenberg
Cc: glasgow-haskell-users@haskell.org Mailing List; Simon Peyton-Jones
Subject: Re: default roles
On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg
<e...@cis.upenn.edu<mailto:e...@cis.upenn.edu>> wrote:
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.
Does GND make sense in cases where the superclasses aren't also derived? If I
had a type T whose Ord instance made use of the Eq instance for some reason,
and then I made a newtype T' with a new Eq instance and a GND Ord instance, the
calls to (==) in the Ord instance will refer to the T implementation, right?
That seems like what'd we'd expect GND to do, but is it ever something you
would want to do?
--
Dave Menendez <d...@zednenem.com<mailto:d...@zednenem.com>>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
