[GHC] #9123: Need for higher kinded roles

[GHC]

#9123: Need for higher kinded roles
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |            Owner:  goldfire
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:  7.12.1
             Component:  Compiler    |          Version:  7.8.2
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Project (more
       Type of failure:              |  than a week)
  None/Unknown                       |       Blocked By:
             Test Case:              |  Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * cc: sweirich@… (added)
 * difficulty:  Unknown => Project (more than a week)
 * milestone:  7.10.1 => 7.12.1


Comment:

 I hate to disappoint, but my thesis advisor, cc'd, has forbidden me from
 taking this on in the near future.

 To be fair, I didn't push back too strongly, because this is a non-trivial
 change:

 1. It requires a new theory for Core to be worked out (and, ideally,
 proved type-safe). We need to update Core because rule (*) from comment:15
 has to be baked in.

 2. It requires a way to infer `Rep` instances. Are these created on-the-
 fly like `Coercible` ones? Are they generated automatically, but not on-
 the fly? Do they require the user to request them?

 3. It requires a new solver for `Coercible` instances, preferably with
 some suggestion of completeness.

 Though I'm not convinced the community would want yet another paper on
 roles, fixing the deficiencies of the previous paper, I actually think
 that there's enough to be worked out here that such a paper would be
 possible to write.

 And, I'm a little bothered that, even after all of this work, we would
 still not have a comprehensive solution. I would expect that within the
 next few years, someone (quite possibly named Edward Kmett) would find a
 very-legitimate use case that this solution would not address. And then
 the whole rigamarole would have to be repeated.

 The real answer, I think, is role polymorphism, which would have the
 expressiveness of the POPL'11 paper but the flexibility of the current
 system. This would mean decorating each kind-level arrow with a role and
 allowing abstraction over those roles. But, these annotations could be
 drawn from an ordinary promoted datatype! Thus, we would have something
 like `(->) :: Role -> * -> * -> *`. (There is some similarity between this
 idea and NoSubKinds.) Inferring these annotations might be problematic,
 though.

 It is tantalizing to note that roles are somehow dual to injectivity. That
 is, if `F`'s argument has a representational role, then `x ≈ y` implies `F
 x ≈ F y` (writing `≈` for {{{`Coercible`}}}). Rather similarly, if `F` is
 injective, then `F x ~ F y` implies `x ~ y`. We might even want to
 abstract over injectivity, noting that `map f` is injective precisely when
 `f` is injective. Injectivity abstraction is certainly far off (we don't
 yet have a useful `map` in types!), but my intuition is that the right
 solution to the problems described here would also allow injectivity
 abstraction... and that if it doesn't we might not have the right solution
 here.

 Getting much more concrete, I think a better way forward in the short term
 is to allow something like `deriving {-# UNSAFE #-} instance Monad m =>
 Monad (N m)`, allowing GND to use `unsafeCoerce` instead of `coerce`. This
 could, instead, be done using Template Haskell without too much bother. We
 could even go ahead and add `join` to `Monad`. Most GNDs with the enhanced
 `Monad` would still work, and if they don't, we can make sure that the
 error message gives useful advice.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9123#comment:27>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler