small improvement to roles mechanism

[Edward Kmett]

Playing around with this for a few minutes led me to the following very
half-baked thoughts and observations. I'm going to lob up a bunch of things
that are potentially too big of a change to contemplate, and which aren't
fully thought out. I warn you in advance. =)

My first thought is that NextParamNominal doesn't add really any value, its
just the positive assertion that some argument is really representational
that is interesting. What if it was that the compiler generated instances
for the NextParamRepresentation (called NPR in the sequel so I can keep
sane) that it could figure out, but we left it open so users could supply
explicit witnesses. This seems somewhat more compatible with the open world
assumption.

E.g.

import Control.Category
import GHC.Prim

class NPR (c :: * -> *) where
  npr :: Coercible a b => Proxy# c -> Proxy# a -> Proxy# b -> (Coercible (c
a) (c b) => r) -> r

Note: Coercible does not seem to be currently polykinded. I expected to use
something like:

class NPR (c :: i -> j) where

so this is currently just a toy, but it is enough to write non-trivial, but
stuff in user land.

It does point out that if you wanted to proceed down this path you'd
probably need to poly-kind Coercible or use more heavy machinery somewhere
else.

Currently, my major problem with the role machinery, is that it is
basically unusable in the presence of any kind of monad transformer or
decently parametric type. For instance There is no way to observe that
something like

newtype Compose f g a = Compose (f (g a))

really should be representational when both f and g have their next
argument representational, but the following *does* type check:

instance (NPR f, NPR g) => NPR (Compose f g) where
  npr _ a b k
     = npr (proxy# :: Proxy# g) a b
     $ npr (proxy# :: Proxy# f) (g a) (g b) k
     where
       g :: Proxy# a -> Proxy# (g a)
       g _ = proxy#

and could be written by an expert user. It seems to me that by preventing
the user from instantiating NPR you'd be cutting off a significantly
productive avenue that might be sufficient to get you much of the power of
full roles as kinds.

With something like that, then the current rule that lets you lift
Coercible a b  to get Coercible (f a) (f b) could become something like:

(NPR f, Coercible a b) => Coercible (f a) (f b)

rather than rummage explicitly through the role information.

Similarly the machinery for GND could use NPR to cast the dictionary slots.

The current role annotations would then serve as requests for instances for
the representational arguments.

Two trivial and largely irrelevant asides at this point:

1.) If we stole the @ type application syntax for proxy application then
that would be something like:

  npr _ @a @b k = npr @g @a @b $ npr @f @(g a) @(g b) k

probably with a bunch of disambiguating parens. ;) It'd probably be about
the same with explicit type application as well though.

2.) In writing that it turned out that GHC rejected (_ :: Proxy# a) as a
pattern with ScopedTypeVariables, as that expects the type on the right of
the :: to have lifted kind. That is why I'm using the `asTypeOf`, style of
combinator to apply `g` to the proxy. I'm not familiar with that part of
the compiler, so I don't know how trivial that would be to fix. It probably
arises if you go to talk about an explicit (_ :: State# s) pattern as well.

Back on topic:

This isn't a perfect solution though. It strikes me that there are many of
these instances that we can't write cleanly or possibly at all in user land:

data Free f a = Pure a | Free (f (Free f a))

instance NPR f => NPR (Free f) where
  npr _ a b k = ???

so perhaps I've missed the mark on what the constraint should be or perhaps
saying

type role Compose nominal nominal representational

could be enough to infer that you need the

instance (NPR f, NPR g) => NPR (Compose f g)

using the role annotation to drive the request for such an instance

(Aside: should those first args be representational?)

Similarly,

type role Free nominal representational

could be enough to figure out that we pass 'f' (Free f a), so for 'a' to be
representational f has to take a representational argument, and give you

instance NPR f => NPR (Free f)

It turns this sort of thing from an inference to a checking problem which
seems more tractable.

This strikes me as a big can of worms, but it is an interesting potential
point in the design space.

It also probably makes me sound like a raving lunatic, but I figured
someone should give you feedback on the idea. ;)

-Edward



On Thu, Oct 10, 2013 at 11: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/99840d84/attachment.html>