default roles

[David Menendez]

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