Re: [GHC] #8516: Add (->) representation and the Invariant class to GHC.Generics

14 Aug 2016

      #8516: Add (->) representation and the Invariant class to GHC.Generics
-------------------------------------+-------------------------------------
        Reporter:  nfrisby           |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler (Type    |              Version:  7.7
  checker)                           |
      Resolution:                    |             Keywords:  Generics
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 nfrisby, that sounds about right. What you call `RoleIsRep` is what Edward
 Kmett calls [https://ghc.haskell.org/trac/ghc/ticket/9123#comment:5
 Representational], which has the definition:

 {{{#!hs
 class Representational f where
   rep :: Coercible a b => Coercion (f a) (f b)
 }}}

 goldfire raised the idea of making `Representational` a superclass of
 `Functor` [https://ghc.haskell.org/trac/ghc/ticket/9123#comment:3 here].
 Indeed, every `Functor` instance should also admit a `Representational`
 instance. I can't prove this directly, since you aren't allowed to
 implement `Coercible` instances directly, but you can at least write both
 halves of the isomorphism a `Coercion` induces:

 {{{#!hs
 functorRep1 :: (Coercible a b, Functor f) => f a -> f b
 functorRep1 = fmap coerce

 functorRep2 :: (Coercible a b, Functor f) => f b -> f a
 functorRep2 = fmap coerce
 }}}

 And since the `Functor` laws dictate that `fmap id = id`, and `coerce` is
 morally the same thing as `id`, we can reason that `fmap coerce = coerce`
 for all law-abiding `Functor`s.

 With that above machinery, our new `Generic1` instance looks like:

 {{{#!hs
 data T f a = T (f [a])

 instance Representational f => Generic1 (T f) where
   type Rep1 (T f) =
     D1 ('MetaData "T" "module" "package" 'True)
       (C1 ('MetaCons "T" 'PrefixI 'False)
         (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness
 'DecidedLazy)
           (f :.: Rec1 [])))
   from1 (T x) = M1 (M1 (M1 (Comp1 (coerceWith rep x))))
   to1 (M1 (M1 (M1 x))) = T (coerceWith rep (unComp1 x))
 }}}

 Replying to [comment:6 nfrisby]:
...
Can we anticipate a time where a user would want these three things
 simultaneously: 1) a lawful `Functor f`, 2) a `nominal` role for `f`'s
 argument, and 3) an automatically derived `Generic1` instance? That's the
 only case where this would be "worse" for the user, I think.
My hope is that (1) and (2) won't happen simultaneously, but now that I
 think about it more closely, there is a case where this does happen: type
 families. Consider this code:

 {{{#!hs
 type family Id a where
   Id a = a

 newtype I a = I (Id a)

 instance Functor I where
   fmap f (I a) = I (f a)

 newtype T a = T (I [a]) deriving Generic1
 }}}

 However, if we switched over to `Representational`, this would no longer
 typecheck, since GHC always infers `nominal` roles for every argument of a
 type family. The fact that `Id`'s argument is `nominal` is a bit annoying,
 since it //feels// like it should be `representational`, but at present we
 have no way of enforcing that.

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