I have some use for Generic for an existential type which is constraint to be Generic.
{-# LANGUAGE DeriveGeneric #-}{-# LANGUAGE ExistentialQuantification #-}{-# LANGUAGE StandaloneDeriving #-}importGHC.GenericsdataU=foralla.(Generica)=>Uaderiving(Generic)-- TRY 1-- Can't make a derived instance of ‘Generic U’:-- Constructor ‘U’ has existentials or constraints in its type-- Possible fix: use a standalone deriving declaration insteadderivinginstanceGenericU-- TRY 2-- Can't make a derived instance of ‘Generic U’:-- U must be a vanilla data constructor-- In the stand-alone deriving instance for ‘Generic U’dataD1SerdataC1_0SerinstanceGenericUwhere-- TRY 3typeRepU=DD1Ser(C1C1_0Ser(S1NoSelector(Repa)))-- Not in scope: type variable ‘a’-- How to bring the existential type `a' into scope?
Edited
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Child items
0
Show closed items
No child items are currently assigned. Use child items to break down this issue into smaller parts.
I might be wrong, but I don't think there's any hope for supporting existentials with the current approach of GHC.Generics (especially when their kind is * and they show up as arguments to constructors).
I think that we'd need new language extensions (QuantifiedConstraints and ImplicationConstraints) to do this properly. See my comment on #5927 (closed).
Indeed, now that we have QuantifiedConstraints, we may very well have all the machinery we need to define Generic for GADTs. The remaining question is how far we want to go with it.
When I say "define Generic for GADTs", there are two shortcomings of today's GHC.Generics that would need to be addressed:
GHC.Generics does not provide a way to reason about existential contexts in GADT constructors (e.g., data T1 a where MkT1 :: Show a => a -> T1 a)
GHC.Generics does not provide a way to reason about existentially quantified type variables in GADT constructors (e.g., data T2 where MkT2 :: e -> T2)
These are related shortcomings, but I believe that (1) would be easier to solve than (2). This relates to GHC.Generics because the amount of extra machinery we would to add to that module depends on whether we want to solve both (1) and (2), or if we only want to solve (1). With that in mind, I'll sketch two potential designs that could add GADT support to GHC.Generics:
A conservative extension to GHC.Generics
Today's GHC.Generics has many different representation types for handling different properties of data constructors. For example, it has (:+:) to represent sums, (:*:) to represent products, and K1 to represent fields. This design would add one more representation type, (:=>:), that is specifically geared towards representing existential contexts:
Its corresponding Rep type in a Generic instance would look approximately like so:
instance Generic (T1 a) where type Rep (T1 a) = (Show a) :=>: (K1 a)
The interesting part comes when we define instances of (:=>:) for use in datatype-generic programs. As a simple example, suppose we wanted to define a generic version of the Show class. We might have define an auxiliary type class to show representation types:
The novel bit comes when we have to define a GShow instance for (:=>:). We want to make sure that the existential context in the data constructor doesn't "leak" out when we pattern match on it—after all, that is the whole point of existential contexts. To reify this property into the language of GHC.Generics representation types, we make use of QuantifiedConstraints:
The c => Show f says that Show f holds, but only under the assumption that c already holds. This is the key step that prevents c from leaking out. Armed with this instance (and suitable GShow instances for other representation types, such as K1), we can define a Show instance for T1:
instanceShow(T1a)whereshow=defaultShow
This all is described in more detail in this blog post of mine. Note that what I call (:=>:) above is referred to as ECC in the blog post, but other than that, the idea is lifted directly from the post.
A key advantage of this approach is that it is entirely backwards-compatible with today's GHC.Generics. The only change is the introduction of a new representation type, but beyond that, all existing code that uses GHC.Generics should continue to compile. Users could then opt in to existential-context support by defining instances for (:=>:).
The downside of this approach is that it solves shortcoming (1) above, but it does not solve shortcoming (2). In other words, it is an incomplete solution to the overall problem, and in particular, this would not address the program in the original issue description.
A redesign of GHC.Generics (a.k.a, the kind-generics approach)
I've spent a while thinking of a way to fix both shortcomings (1) and (2) in a way that's backwards-compatible with today's GHC.Generics. The closest I came was this Haskell Implementors Workshop talk, but the system described in that talk is rather clunky and confusing to use. By sheer coincidence, I discovered later (at the same venue where I gave my talk, no less) that @trupill and @VictorCMiraldo had also discovered a way to fix both shortcomings (1) and (2), described in their paper Generic Programming of All Kinds.
The upside is that their approach is much cleaner than any ideas I had at the time, and their approach can represent more data types. The best way to learn about how their approach works is to look at the kind-generics, which implements the ideas from their paper in the style of GHC.Generics. They've also included a tutorial in the kind-generics repo, which is likely an easier place to start than the paper itself.
The downside, however, is that kind-generics is a pretty fundamental redesign of how GHC.Generics works. The overall idea is the same: you have a type class, GenericK, with an associated type family, RepK. Instances of GenericK will provide implement RepK such that it is isomorphic to the original data type, and also define functions that convert the data type to RepK (and vice versa). Users define datatype-generic code by defining instances for representation types, just as in GHC.Generics. Moreover, some of the representation types in kind-generics are taken directly from GHC.Generics without changes.
The similarities stop there, however. A key difference in GHC.Generics is that representation types all have kind LoT d -> Type. LoT (short for "list of types") is a type-level context that tracks how many type variables are in scope. The use of LoT is critical for kind-generics to be able to solve shortcoming (2) above, as existential type variables are tracked in this type-level context. As a result of this extra complexity, defining datatype-generic code using kind-generics can sometimes require more sophistication than what is usually seen with today's GHC.Generics.
In fewer words, there's no simple way to turn GHC.Generics into kind-generics without breaking changes. The changes might be worth the breakage, as we would gain the ability to define datatype-generic code for GADTs (both of the (1) and (2) variety), but it would be breakage nonetheless.
Which approach is better?
I'm not sure. There's no denying that the "conservative extension to GHC.Generics" approach is only a partial solution, but on the other hand, it's vastly simpler. Perhaps there is sufficient value in only addressing shortcoming (1), but not (2), that it makes to pursue this approach. As a testament to this approach's simplicity, I've already implemented in an experimental GHC branch here, and it only takes about 280 extra lines of code in total.
On the other hand, I'm sure that many people won't be satisfied unless they can define Generic instances of both the (1) and (2) varieties. kind-generics is able to do that, but there's still a question of the cleanest way to migrate from today's GHC.Generics to kind-generics. One idea that I've discussed with @trupill and @VictorCMiraldo is to implement these ideas in a new GHC.Generics.Kind module while keeping the existing GHC.Generics module around for "legacy" datatype-generic code. This would allow people to experiment with the new ideas, and if GHC.Generics.Kind became much more popular than GHC.Generics, we could even consider deprecating the latter in favor of the former. Moreover, it's worth noting that this idea doesn't exclude the possibility of adding (:=>:) to GHC.Generics, and it would be theoretically possible to implement both approaches. (Note that I do not yet have a complete implementation of kind-generics within GHC.)
As a final note, I'd like to emphasize that none of the ideas above are set in stone, and any further action on this front would warrant a GHC proposal(s).
I'm still not sure what you're trying to propose. First of all, just to clarify:
One could introduce the following type:
data Exists1 f a where Exists1 :: forall x. f x
That isn't a legal GADT definition. Did you mean something like this?
dataExists1fawhereExists1::forallfx.fx->Exists1fx
If so, is your intention to use Exists1 to represent data types with existentially quantified type variables? For example, what would the representation type for something like this look like with Exists1?
Ah, now I see what you mean. That's an interesting idea for representing only a subset of GADTs with existentially quantified type variables. Presumably there would be some restrictions about the positions where existentially quantified type variables are legal? For example, I'm struggling to imagine how to represent these data types:
Yes, you would have the same restrictions as Generic1: the type argument could only appear under zero or more applications of functors, but not as in a -> a.
For the second case the solution would be to have a special form of the (:=>) you mentioned above which applies the constraint to its argument:
Yes, you would have the same restrictions as Generic1: the type argument could only appear under zero or more applications of functors, but not as in a -> a.
I see.
Is there a story for how multiple existentially quantified type variables would work? For instance, would either of these data types be representable?
dataSwhereMkS::a->a->SdataTwhereMkT::a->b->T
For the second case the solution would be to have a special form of the (:=>) you mentioned above which applies the constraint to its argument:
But what should go in the place of the ??? above? We can't use c x because we don't have a type variable x in scope. Nor does QuantifiedConstraints work, since if you try to do something like this:
Bug.hs:34:10: error: * Could not deduce: c x0 from the context: forall x. c x => Foldable f bound by an instance declaration: forall (c :: * -> Constraint) (f :: * -> *). (forall x. c x => Foldable f) => Foldable (Implies1 c f) at Bug.hs:34:10-65 or from: c x bound by a quantified context at Bug.hs:34:10-65 * In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for `Foldable (Implies1 c f)' |34 | instance (forall x. c x => Foldable f) => Foldable (Implies1 c f) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
For these reasons, I gave up on this idea in this blog post of mine. But perhaps you can find a way to make this work?