More GND + role inference woes

[Simon Peyton-Jones]

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?

Simon

From: Richard Eisenberg [mailto:eir at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131016/346305b1/attachment-0001.html>