small improvement to roles mechanism
Fri Oct 11 23:14:48 UTC 2013
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.
> PS: Due credit is to migmit for suggesting the type-class idea on
> ghc-devs mailing list
> ghc-devs at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs