If this forced me to write those instances by hand, I could accept that as a
tax for correctness. It means you can't GND any of the HasFoo dictionaries that
lens builds, but meh.
My original objection was for the existing solution with type classes
themselves having their arguments be representational. Now that we've changed
the problem, the fact that things like this are being caught does a lot to
reassure me of the vastly improved correctness of the new scheme.
Off the top of your head do things like the following work under the new scheme?
newtype T m a = T { runT :: StateT MyState m a } deriving (Monad, MonadState
MyState, MonadTrans)
I don't have a good enough mental model of the desugaring of the fundep in
MonadState.
-Edward
> On Oct 16, 2013, at 1:28 PM, Richard Eisenberg <[email protected]> wrote:
>
> 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
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
