On Oct 16, 2013, at 4:23 PM, Simon Peyton-Jones wrote: > What it would mean is that, if we do decide to generalize roles further, > users would have one release that allows noticeably fewer uses of GND than > the one before or the one after it. On the other hand, if we're confident > that we're not going to tinker with roles more, then I see much stronger > reasons for releasing with 7.8. > > I don’t think we know for sure. But the way to find out is to release it. > If we don’t have a compiler that supports roles, no one will explore or use > them. We do this all the time, and yes, Haskell is a bit less > smoothly-upgradable as a result. But I think it’s worth it, otherwise we’d > be stuck in treacle. > > Remember this is fixing a current unsoundness that can lead to un-caught > segmentation faults in user code. That is a Jolly Good thing to fix, it not > just a snazzy feature that two people want. > > Richard, how are you fixed at the moment? Are you able to implement the new > GND check soon? Or not?
OK. It sounds like we're all pushing forward here. I should be able to implement within the next week, probably starting tomorrow, and possibly ending tomorrow, too. Not sure exactly how hard it will be. Richard > > Simon > > From: Richard Eisenberg [mailto:e...@cis.upenn.edu] > Sent: 16 October 2013 18:29 > To: Simon Peyton-Jones > Cc: Edward Kmett; ghc-devs > Subject: Re: More GND + role inference woes > > Please see my responses below. (Note: this was written before Edward's most > recent post, which will be addressed shortly.) > Executive summary: Edward's problem is more general than the one that Simon > solves, but what Edward wants is actually not type safe. > > On Oct 16, 2013, at 9:28 AM, Simon Peyton-Jones 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? > > This is a more specific instance of the problem. Yes, the case with `Trans` > does appear, but also cases like this: > > class Functor f => Core f where > core :: ((forall g x. Functor g => (x -> g x) -> f x -> g (f x)) -> a) -> f > a > > That's a nasty-looking type, but note the `g (f x)` that appears. Here, `f` > is used as a parameter to a type variable that *is not a class variable*. The > problem Simon describes is only the case where the applied type variable is a > class variable, and thus is known at `deriving` time. > > To handle things like Core, we would need to have more proper role > abstraction, where we can assert that `g` has a parameter with a > representational role in order to infer `f` as a representational parameter > for Core. In Edward's `linear` package, the Linear.Affine module has this > definition: > > newtype Point f a = P (f a) > deriving ( Eq, Ord, Show, Read, Monad, Functor, Applicative, Foldable > , Traversable, Apply, Bind, Additive, Metric, Core, R1, R2, R3, R4 > , Fractional , Num, Ix, Storable, Epsilon > ) > > Of these derivings, the following currently fail: Traversable, Bind, Core, > R1, R2, R3, and R4. It is straightforward to fix Traversable with > DeriveTraversable (and a standalone instance). Bind will fixed by the change > in the GND check. But, Core and the Rs won't be and would have to be written > by hand. > > > > > > 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? > > Yes. > > > > > 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? > > Yes. > > > 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. > > Well, it's the right-hand side of the arrow that's more troublesome, but that > works out in this case, too. > > > > In short, I think we are fine, once Richard has implemented the new GND test. > > Am I wrong? > > It depends on what "fine" is. > > The new GND check will allow more deriving, but not all that Edward wants. > BUT, the ones that (the new) GND doesn't allow aren't actually safe! In the > Point example, using GND on Core and the Rs might actually lead to a type > error, depending on the instantiation of local type variables within the > methods in those classes. For example, if the `g` variable in Core's `core` > method is instantiated with a type with a nominal parameter, there could be > trouble. > > So, I disagree with Edward's original claim at the top of this thread that > roles cause havoc here: they don't cause havoc, they catch latent type errors! > > On the other hand, I agree that with more machinery (that is, a constraint on > `g` about its parameter's role) we could potentially allow all the derived > instances that Edward wants. > > What I'm worried about is the user experience like the following: > - 7.8 comes out: A bunch of deriving clauses have to be expanded to > hand-written instances. Annoying, and with runtime cost. > - 7.10 comes out: A bunch of those expanded instances now can be rolled back > into derived ones, with some extra, not-backward-compatible annotations (that > is, the constraints on variables like `g`). Annoying, and a real maintenance > headache. > > What it would mean is that, if we do decide to generalize roles further, > users would have one release that allows noticeably fewer uses of GND than > the one before or the one after it. On the other hand, if we're confident > that we're not going to tinker with roles more, then I see much stronger > reasons for releasing with 7.8. > > Richard
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
