Opened 5 years ago
Last modified 9 months ago
#8516 new feature request
Add (->) representation and the Invariant class to GHC.Generics
Reported by: | nfrisby | Owned by: | |
---|---|---|---|
Priority: | low | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.7 |
Keywords: | Generics, QuantifiedConstraints | Cc: | dreixel, goldfire, spl, Iceland_jack, songzh, kosmikus |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
We currently disallow any use of the parameter in the domain of (->).
newtype F a = F ((a -> Int) -> Int) deriving Generic1 <interactive>:4:38: Can't make a derived instance of `Generic1 (F g)': Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->) In the data declaration for `F'
DeriveFunctor succeeds for this F.
I'd like to add this representation type to GHC.Generics and DeriveGeneric.
newtype (f :->: g) a = FArrow1 (f a -> g a)
We could then represent the first example above. We could also derive the more interesting Generic1 (F g).
newtype F g a = F (g a -> Int) deriving Generic1 type instance Rep1 (F g) = Rec1 g :->: Rec0 Int instance Generic1 (F g) where to x = F $ unRec0 . unArrow1 x . Rec1 from (F x) = FArrow1 $ Rec0 . x . unRec1
Admittedly, there's not many generic definitions impeded by not having (:->:). Contra- and in-variant types are uncommon.
I'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim.
class Invariant t where invmap :: (a -> b) -> (b -> a) -> t a -> t b invmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b invmap_covariant f _ = fmap f instance (Invariant f,Invariant g) => Invariant (FArrow f g) where invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co
(Of course, Invariant should be a super class of Functor. :/ )
Now we can handle quite involved examples:
newtype F g h a = F (g (h a)) deriving Generic1 instance Invariant g => Generic1 (F g h) where to x = invmap unRec1 Rec1 $ unComp1 x from (F x) = Comp1 $ invmap Rec1 unRec1
All of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments.
Change History (18)
comment:1 Changed 5 years ago by
Cc: | dreixel added |
---|
comment:2 Changed 3 years ago by
comment:3 Changed 3 years ago by
Well, I had previously thought one could get away with not considering Invariant
, but after thinking about it some more, having Invariant
is crucial for this new feature to be compositional.
We'd add two new data types:
infixr 4 :->:, :->-: newtype (f :->: r) p = ContraArrow1 { unContraArrow1 :: f p -> r } newtype (f :->-: g) p = InvArrow1 { unInvArrow1 :: f p -> g p }
And, if we change Rec1 f
to f :.: Par1
, then we can also define the following for symmetry:
infixr 4 :>-: type (r :>-: f) = ((->) r) :.: f
(I've adopted a pretty arbitrary naming scheme where hyphens (-
) denote occurrences of the type parameter. Feel free to suggest other names.)
Then we can generate instances for data types no matter which side of an arrow a type parameter might occur. Here is an example:
newtype Endo a = Endo (a -> a) deriving Generic1 instance Invariant Endo where invmap f g (Endo x) = Endo (f . x . g) ==> instance Generic1 Endo where type Rep1 Endo = D1 ... (C1 ... (S1 ... (Par1 :->-: Par1))) to1 (M1 (M1 (M1 c))) = Endo ((.) (invCompose unPar1 Par1) unInvArrow1 c) from1 (Endo c) = M1 (M1 (M1 ((.) InvArrow1 (invCompose Par1 unPar1) c))) invCompose :: (c -> d) -> (a -> b) -> (b -> c) -> a -> d invCompose = \f g h x -> f (h (g x))
So far, so good. But if we define something like this:
newtype Endo2 a = Endo2 (Endo a) deriving Generic1
Then things become awkward. GHC would attempt to generate an instance like this:
instance Generic1 Endo2 where type Rep1 Endo2 = D1 ... (C1 ... (S1 ... (Endo :.: Par1))) to1 (M1 (M1 (M1 c))) = Endo2 ((.) (fmap unPar1) unComp1 c) from1 (Endo2 c) = M1 (M1 (M1 ((.) Comp1 (fmap Par1) c)))
But this will never work, because it assumes Endo
is a Functor
instance, which can't happen. This is quite a problem: we can make one datatype a Generic1
instance, but we can't make a simple newtype
wrapper around it a Generic1
instance!
However, if we changed the way GHC generated code for the :.:
case to assume that the outermost datatype is an Invariant
instance, not a Functor
instance, then it would work:
instance Generic1 Endo where type Rep1 Endo = D1 ... (C1 ... (S1 ... (Par1 :->-: Par1))) to1 (M1 (M1 (M1 c))) = Endo ((.) (invCompose unPar1 Par1) unInvArrow1 c) from1 (Endo c) = M1 (M1 (M1 ((.) InvArrow1 (invCompose Par1 unPar1) c)))
Of course, this would mean bringing in Invariant
to base
, and it makes an assumption that most datatypes you'd find in the wild are Invariant
instances already. As I mentioned above, trying to make Invariant
a superclass of Functor
is a hard sell.
Futhermore, I'm not sure if we'd really gain anything after all this breakage besides being able to derive Functor
and Invariant
instances generically. I'm not convinced the benefits outweigh the potential heartburn in this case.
comment:4 Changed 3 years ago by
Keywords: | Generics added |
---|
comment:5 Changed 3 years ago by
Cc: | goldfire added |
---|
I've been thinking about this recently, and I suspect there might be a way to accomplish this without needing anything like Functor
or Invariant
.
The only reason we currently use Functor
constraints in derived Generic1
instances is to give us the ability to "tunnel into" data structures that are polymorphically recursive at least two levels deep (e.g., newtype Compose f g a = Compose (f (g a))
). Consider a Generic1
instance for Foo
:
instance Functor f => Generic1 (Compose f g) where type Rep1 (Compose f g) = D1 ('MetaData "Compose" "Ghci3" "interactive" 'True) (C1 ('MetaCons "Compose" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (f :.: Rec1 g))) from1 (Compose x) = M1 (M1 (M1 (Comp1 (fmap Rec1 x)))) to1 (M1 (M1 (M1 x))) = Compose (fmap unRec1 (unComp1 x))
This works, but requires that ugly Functor
constraint. Is there an alternative? If we replace the fmap
calls with holes:
instance Generic1 (Compose f g) where type Rep1 (Compose f g) = D1 ('MetaData "Compose" "Ghci3" "interactive" 'True) (C1 ('MetaCons "Compose" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (f :.: Rec1 g))) from1 (Compose x) = M1 (M1 (M1 (Comp1 (_1 x)))) to1 (M1 (M1 (M1 x))) = Compose (_2 (unComp1 x))
Then it becomes clear what functions we need:
_1 :: f (g a) -> f (Rec1 g a) _2 :: f (Rec1 g a) -> f (g a)
All that _1
and _2
are doing is wrapping and unwrapping a newtype
underneath an f
! This would be a perfect job for Data.Coerce.coerce
. If we could write something like this:
instance (Coercible (f (g a)) (f (Rec1 g a)), Coercible (f (Rec1 g a)) (f (g a)) => Generic1 (Compose f g) where type Rep1 (Compose f g) = D1 ('MetaData "Compose" "Ghci3" "interactive" 'True) (C1 ('MetaCons "Compose" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (f :.: Rec1 g))) from1 (Compose x) = M1 (M1 (M1 (Comp1 (coerce x)))) to1 (M1 (M1 (M1 x))) = Compose (coerce (unComp1 x))
It would work! But we can't write this since a
isn't in scope in the instance's context. I can't even figure out how to hack it using something like Data.Constraint.Forall from the constraints
library.
Of course, there's the issue that we don't know a priori what role the type argument to f
has, so there would still be some types for which this Generic1
instance wouldn't typecheck. But I claim that any type for which f
is forced to be nominal (i.e., for which you couldn't coerce
underneath f
) couldn't have a Functor
instance anyway, so this approach should be no less expressive than the current one.
goldfire, would #9123 (higher-kinded roles) give us the ability to express this? If so, I think we could sidestep the issue of including Invariant
in base
entirely, since it would become unnecessary.
comment:6 follow-up: 7 Changed 3 years ago by
Ryan, this looks very promising! I think this snippet presents the idea clearly, if I understand correctly. Please confirm.
-- | We suspect higher-order kinds (#9123) would supplant this typeclass. class RoleIsRep f where mapCoerce :: Coercible a b => f a -> f b data T f a = T (f [a]) instance RoleIsRep 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 (mapCoerce x)))) to1 (M1 (M1 (M1 x))) = T (mapCoerce (unComp1 x))
Note that this is a performance improvement in some cases to boot!
And your observation is that if we can define a lawful Functor f
then we can define RoleRep f
, right?
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.
comment:7 Changed 3 years ago by
nfrisby, that sounds about right. What you call RoleIsRep
is what Edward Kmett calls Representational, which has the definition:
class Representational f where rep :: Coercible a b => Coercion (f a) (f b)
goldfire raised the idea of making Representational
a superclass of Functor
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:
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:
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 nfrisby:
Can we anticipate a time where a user would want these three things simultaneously: 1) a lawful
Functor f
, 2) anominal
role forf
's argument, and 3) an automatically derivedGeneric1
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:
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.
comment:8 Changed 3 years ago by
Cc: | spl added |
---|
comment:9 follow-up: 12 Changed 3 years ago by
Crumbs... #9123 (about Representational
) is a long thread! I'm totally not up to speed with all that.
However, part of the mix seems to be the feasibility (or otherwise) of allowing constraints like (forall a. Eq a => Eq [a]
instance contexts; see #2893, #2456, and #5927, etc. For example:
instance (Binary a, forall b. Binary b => Binary (f b)) => Binary (GRowe f a) where ...
I've always said "I don't know how to implement that", but this morning it feels different. Suppose that we only allowed those quantified constraints in the context of a top-level instance declaration.
- Solving "Wanted" constraints of this form is easy: it's just an implication constraint.
- Allowing them as "Given" constraints would be a little awkward, because it'd need a new field in the "inert set" of the constraint solver. But for instances it's all top-level-ish, so we could perhaps just extend the "local instance environment".
But even in the more general form it would be quite do-able I think. So, if allowing quantified constraints will help, perhaps it's time we bit that bullet.
Simon
Then it would only show up as a "Given" constraint when solving instance declarations, not in some arbitrary
comment:10 Changed 3 years ago by
Thanks, Simon! ImplicationConstraints
/QuantifiedConstraints
is something I've been wanting for a while, and it would definitely help me express more things in GHC generics than I've been wanting to express (see this comment in #5927 for more).
nfrisby, I thought of one more scenario in which conditions (1) and (2) could hold, but it's a bit of a silly one:
type role Wat nominal newtype Wat a = Wat a deriving (Functor, Generic1)
A scheming user could use RoleAnnotations
to explicitly mark a role as nominal
that would otherwise be inferred as representational
(or phantom
). But this feels extremely silly to me, since having a Functor
instance seems to defeat the whole point of having a nominal
role, since you can just use fmap
to change the internal representation yourself. Indeed, the only examples I can think of where users mark roles as nominal
are:
Set
(from the containers package)HashSet
(from the unordered-containers package)Key
(from the vault package)
And none of those can have Functor
instances anyway. So I don't think this "counterexample" is much of a concern at all.
comment:11 Changed 3 years ago by
And as it turns out, goldfire has a separate ticket (#8177) for the proposed idea of being able to give explicit role signatures to type families, which might make the potential regression in this comment not an actual regression. See my comment here.
comment:12 Changed 3 years ago by
Replying to simonpj:
But even in the more general form it would be quite do-able I think. So, if allowing quantified constraints will help, perhaps it's time we bit that bullet.
I think this is do-able. (I'm not currently volunteering to do it, though. Perhaps in the future, as doing this looks fun.) See our conversation starting at comment:14:ticket:2256.
comment:13 Changed 3 years ago by
Cc: | Iceland_jack added |
---|
comment:14 Changed 2 years ago by
Cc: | songzh added |
---|
Replying to nfrisby:
We currently disallow any use of the parameter in the domain of (->).
newtype F a = F ((a -> Int) -> Int) deriving Generic1 <interactive>:4:38: Can't make a derived instance of `Generic1 (F g)': Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->) In the data declaration for `F'DeriveFunctor succeeds for this F.
I'd like to add this representation type to GHC.Generics and DeriveGeneric.
newtype (f :->: g) a = FArrow1 (f a -> g a)We could then represent the first example above. We could also derive the more interesting Generic1 (F g).
newtype F g a = F (g a -> Int) deriving Generic1 type instance Rep1 (F g) = Rec1 g :->: Rec0 Int instance Generic1 (F g) where to x = F $ unRec0 . unArrow1 x . Rec1 from (F x) = FArrow1 $ Rec0 . x . unRec1Admittedly, there's not many generic definitions impeded by not having (:->:). Contra- and in-variant types are uncommon.
I'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim.
class Invariant t where invmap :: (a -> b) -> (b -> a) -> t a -> t b invmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b invmap_covariant f _ = fmap f instance (Invariant f,Invariant g) => Invariant (FArrow f g) where invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co(Of course, Invariant should be a super class of Functor. :/ )
Now we can handle quite involved examples:
newtype F g h a = F (g (h a)) deriving Generic1 instance Invariant g => Generic1 (F g h) where to x = invmap unRec1 Rec1 $ unComp1 x from (F x) = Comp1 $ invmap Rec1 unRec1All of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments.
comment:15 Changed 19 months ago by
Keywords: | QuantifiedContexts added |
---|
comment:16 Changed 13 months ago by
Keywords: | QuantifiedConstraints added; QuantifiedContexts removed |
---|
comment:18 Changed 9 months ago by
Cc: | kosmikus added |
---|
I really like the idea of adding
(:->:)
toGHC.Generics
. One of my biggest gripes withderiving Generic1
is that it doesn't work with many data types that have function arguments (e.g.,Endo
). I think adding(:->:)
would allow GHC generics to at least be as expressive asDeriveFunctor
/Foldable
/Traversable
.I'm a bit hesitant about adding
Invariant
tobase
, however, primarily because I find it unlikely that it would ever be made a superclass ofFunctor
, given the sheer amount of breakage that would cause. Moreover, I don't think we needInvariant
to be able to deriveGeneric1
for data types with(:->:)
. I believe at most a generatedGeneric1
instance would need someFunctor
constraints, but that's no different than the current story.(I haven't worked out the additional rules you'd need to add to the algorithms in Figures 1-4 of http://dreixel.net/research/pdf/gdmh.pdf, but the examples I've worked out by hand so far have only needed
Functor
constraints.)