small improvement to roles mechanism

[Johan Tibell]

Let me start by saying that I'm happy we're trying to fix the GND problem.
Thanks for working on that.

That being said: is this ready for mainstream consumption? We're forcing
this on everyone without any language pragma or flags to opt-in/out. That
is bad if we're not sure we're doing the right thing in some cases or if
we're causing spurious failures. At ICFP I got the impression that very few
people will be affected, but Bryan's result suggests there are more people
than I thought.



On Thu, Oct 10, 2013 at 8:26 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> In Bryan's recent test of GHC 7.8 against all of Hackage, there were three
> spurious errors caused by lack of role abstraction. Here are the class
> definitions where a nominal parameter is inferred, probably against the
> wishes of the author:
>
> from logict-0.2.3/Control.Monad.Logic.Class:
> > class (MonadPlus m) => MonadLogic m where
> >     msplit     :: m a -> m (Maybe (a, m a))
>
> from monadLib-3.5.2/MonadLib:
> > class (Monad m) => ReaderM m i | m -> i where
> >   ask :: m i
>
> from base/Control.Arrow:
> > class Arrow a => ArrowApply a where
> >     app :: a (a b c, b) c
>
> In each of these, the last parameter of the class is given a nominal role
> because it appears as the parameter of a type variable. However, in each
> case, it appears as the parameter of a *class* type variable. This means
> that, if we somehow knew that the class author wanted the class to be
> usable with GND, we could simply check every instance declaration for that
> class to make sure that the relevant concrete instantiation has the right
> role. For example, when the user writes, for example
>
> > instance ArrowApply Foo where ?
>
> we check that Foo's first parameter has a representational role. If it
> doesn't, then the instance is rejected.
>
> An alternative, somewhat heavier idea would be to represent roles as class
> constraints. We could have
>
> > class NextParamNominal (c :: k)
> > class NextParamRepresentational (c :: k)
>
> GHC could "generate" instances for every datatype definition. For example:
>
> > type role Map nominal representational
> > data Map k v = ?
>
> would induce
>
> > instance NextParamNominal Map
> > instance NextParamRepresentational (Map k)
>
> Users would not be able to write these instances -- they would have to be
> generated by GHC. (Alternatively, there could be no instances, just a
> little magic in the constraint solver. Somewhat like Coercible.)
>
> Then, the classes above would just have to add a superclass, like this:
>
> > class (Arrow a, NextParamRepresentational a) => ArrowApply a where
> >   app :: a (a b c, b) c
>
> The role inference mechanism would be made aware of role constraints and
> use this one to derive that ArrowApply is OK for GND.
>
> This "heavier" approach has a similar upshot to the first idea of just
> checking at instance declarations, but it is more customizable and
> transparent to users (I think).
>
>
> I'm not sure I'm advocating for this change (or volunteering to implement
> before the release candidate), but I wanted to document the idea and get
> any feedback that is out there. This would fix the breakage we've seen
> without totally changing the kind system.
>
> Thanks,
> Richard
>
> PS: Due credit is to migmit for suggesting the type-class idea on
> glasgow-haskell-users.
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20131011/2056360d/attachment.html>