#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