Re: [GHC] #9123: Need for higher kinded roles

19 May 2014

      #9123: Need for higher kinded roles
-------------------------------------+------------------------------------
        Reporter:  simonpj           |            Owner:
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by simonpj):

 Let's articulate Edward's proposal explicitly, so we all know what we are
 talking about.   Here is one possible version, expressed in the language
 of the Safe Coercions paper. Yell if I get this wrong.

  * We add the following decomposition rule to the solution rules for
 `Coercible`:
 {{{
 instance (Repesentational f, Coercible a b) => Coercible (f a) (f b)
 }}}
  Edward actually suggested something more like
 {{{
 instance (Representational f, Coercible f g, Coercible a b)
       => Coercible (f a) (g b)
 }}}
  but I dislike the assymetry in `f`, `g`, and I think this weaker thing
 will do.

  * The `Representational` class would have built-in solution rules (as
 `Coercible` does), all of the form:
 {{{
 instance Representational (T a b c)
 }}}
  whenever the ''next'' argument of `T` is representational.

 I am hazy about

  * Whether it should be possible to have user-written instances for
 `Representational`

  * How `Representational` is defined.  It could be
 {{{
 class Representational f where
   rep :: Coercion a b -> Coercion (f a) (f b)
 }}}
  or
 {{{
 class Representational f where
   rep :: Coercible a b => Coercion (f a) (f b)
 }}}
  or (if `Representational` is built in)
 {{{
 class Representational f where
   rep :: Coercible a b => Coercible (f a) (f b)
 }}}
   The latter is easiest for the type checker.

 I see no need to make `Representational` a superclass of `Functor`.
 Rather, GND on
 {{{
 data T m a = MkT (m a) deriving( Monad )
 }}}
 would yield an instance
 {{{
 instance (Representational m, Monad m) => Monad (T m) where
  ...
 }}}
 which is absolutely fine.  No need for every monad to be representational.

 Simon

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