default roles

Simon Peyton-Jones simonpj
Thu Oct 10 16:11:15 UTC 2013


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-bounces at haskell.org] On Behalf Of David Menendez
Sent: 10 October 2013 16:25
To: Richard Eisenberg
Cc: glasgow-haskell-users at haskell.org Mailing List; Simon Peyton-Jones
Subject: Re: default roles

On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at 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 <dave at zednenem.com<mailto:dave at zednenem.com>>
<http://www.eyrie.org/~zednenem/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20131010/97742690/attachment-0001.html>



More information about the Glasgow-haskell-users mailing list