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