It seems like we may be on the same page now. Do you agree with my previous email that the change to the GND check will not solve *all* your problems? That is, there will be some derived instances you will have to hand-write, but (I think) for good reason.
Richard On Oct 16, 2013, at 12:46 PM, Edward Kmett wrote: > > > On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones <simo...@microsoft.com> wrote: > >> I think I know what to do about the GND + roles question. >> >> First, the problem. Here’s an example: >> class Trans t a where >> foo :: t a -> t a >> >> newtype N x = MkN x deriving( Trans Maybe ) >> >> As things stand, Trans gets roles (representational, nominal). The second >> parameter ‘a’ gets a nominal role because we don’t know what ‘t’ will get >> instantiated too. >> >> As a result the attempted GND is rejected because of the new role stuff. >> But with 7.6.3 we’ll get an instance >> instance Trans Maybe a => Trans Maybe (N a) >> from the GND mechanism. >> >> Do I have this right? >> >> >> Second, there is a Good Reason for the problem. Suppose I said >> newtype N x = MkN x deriving( Trans D ) >> where D was a data family. Then the foo method for (D x) might seg-fault if >> applied to a (D (N x)) value. So the current GND is treading on very thin >> ice, and it is ice that the author (Edward) does not control. His clients >> control it. >> >> Do I have this right? >> >> >> Third, there is an easy solution. As Richard observed in a separate thread >> about Coercible, GND does not attempt to build a coercion to witness >> Trans Maybe x ~R Trans Maybe (N x) >> >> Rather, it builds a dictionary for (Trans Maybe (N x)) thus >> dTransMaybeN :: Trans Maybe x -> Trans Maybe (N x) >> dTransMaybeN d = MkTrans (sel_foo d |> co) >> >> where the (sel_foo d) selects the foo method from d. That is, we actually >> cast the methods, not the dictionary as a whole. So what we need is a >> coercion between >> Maybe x ~R Maybe (N x) >> Can we get that? Yes of course! Maybe has a representational role. >> >> Bottom line: we should accept or reject a GND attempt not on the basis of >> the role of the class, but rather on whether the method types are coercible. >> Indeed, this is just what we agreed some days ago >> http://www.haskell.org/pipermail/glasgow-haskell-users/2013-October/024386.html >> >> So I think this solves Edward’s problem below. >> >> >> Moreover, I think this solves the other failures in >> http://www.haskell.org/pipermail/ghc-devs/2013-October/002961.html. Here is >> one example, in that email. smallcheck has this: >> newtype Series m a = Series (ReaderT Depth (LogicT m) a) >> deriving >> ( …, MonadLogic) >> >> where logict defines MonadLogic thus: >> >> class (MonadPlus m) => MonadLogic m where >> msplit :: m a -> m (Maybe (a, m a)) >> >> So the “bottom line” check above will attempt to find a cocercion betwem >> msplit’s type with m=Series m, and with m=ReaderT Depth (LogitT m). Right? >> So on the left of msplit’s arrow, we’ll ask can we prove >> >> Series m a ~R ReaderT Depth (LogicT m) a >> >> Can we show that? Yes, of course… that is the very newtype coercion for >> Series. >> >> In short, I think we are fine, once Richard has implemented the new GND test. >> >> Am I wrong? > > I have no counter examples for GND based on coercing dictionaries rather than > parameters at this time and I do agree that this does strike me as sufficient > to plug the obvious holes in the current approach. > > I'll keep looking and see if I can't find a way to subvert the system, but > this sounds promising for roles. > > In light of this, the NPR approach that Richard suggested strikes me as more > relevant to fixing up Coercible than GND and as you mentioned we can very > well spend another release cycle to get Coercible right. > > Assuming the dictionary casts work the way we expect, I'm think I'm sold. The > main thing I don't want to do is wake up after 7.8 is cut and personally have > to write 4000 lines of previously derived instances that are provably safe, > because of an overly restrictive role scheme. I'm cautiously optimistic that > this will be sufficient to keep me out of that scenario. ;) > > -Edward > >> Simon >> >> >> From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Edward >> Kmett >> Sent: 13 October 2013 23:02 >> To: ghc-devs; Richard Eisenberg >> Subject: Re: More GND + role inference woes >> >> I didn't think I was using GND much at all, but apparently I was wrong. >> >> >> >> After Ben's initial foray into building linear, I went and looked at the >> other applications of GeneralizedNewtypeDeriving in my code and found that >> in parsers, all of the derived instances for the supplied parser >> transformers fail. >> >> >> >> This also affects any attempt to use GND to do deriving for any monad >> transformer stack that isn't fully instantiated to concrete terms. This is >> actually a very common idiom to avoid writing boilerplate on top of >> transformers: >> >> >> >> newtype T m a = T { runT : StateT MyState (ReaderT MyEnv) m a } >> >> deriving (Functor, Monad, Applicative, MonadState MyState, MonadReader >> MyEnv, ...) >> >> >> >> As I rummage through more of my code, I actually can't find any instances of >> GND that do still work that aren't of the form: >> >> >> >> newtype Foo a = Foo { runFoo :: a } deriving ... >> >> >> >> Literally every other example I have of GND in the code I maintain has >> something in it that causes it to run afoul of the new roles machinery. >> >> >> >> I'd say the problem is more widespread than we thought. >> >> >> >> -Edward >> >> >> >> On Sun, Oct 13, 2013 at 5:26 PM, Edward Kmett <ekm...@gmail.com> wrote: >> >> Ben Gamari was trying to update my linear package to work with GHC HEAD. >> >> >> >> Along the way he noted an example of the new GND+role inference machinery >> failing rather spectacularly. >> >> >> >> http://hackage.haskell.org/package/linear-1.3/docs/src/Linear-Affine.html#Point >> >> >> >> Note the number of classes that the current proposal would force us to hand >> implement. >> >> >> >> =( >> >> >> >> -Edward >> >> >>
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
