I think we're basically in agreement. I'm more than happy to write those 5-6 instances that legitimately aren't safe to derive.
-Edward > On Oct 16, 2013, at 1:30 PM, Richard Eisenberg <e...@cis.upenn.edu> wrote: > > 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
