#8165 closed feature request (fixed)
Use GeneralizedNewtypeDeriving to automatically create associated type families
Reported by: | MikeIzbicki | Owned by: | RyanGlScott |
---|---|---|---|
Priority: | normal | Milestone: | 8.2.1 |
Component: | Compiler (Type checker) | Version: | 7.6.3 |
Keywords: | TypeFamilies, deriving | Cc: | RyanGlScott |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | deriving/should_compile/T8165, deriving/should_fail/T8165_fail1, deriving/should_fail/T8165_fail2 |
Blocked By: | Blocking: | ||
Related Tickets: | #2721 | Differential Rev(s): | Phab:D2636 |
Wiki Page: |
Description
Here's a simple example:
class C a where type T a instance C Int where type T Int = Bool newtype NT = NT Int deriving C
Change History (25)
comment:1 Changed 6 years ago by
comment:2 follow-up: 3 Changed 6 years ago by
Ambiguous cases like this could remain a type error. That would probably prevent the most confusion.
comment:3 Changed 6 years ago by
In all the cases where I've wanted to use this, the type is polymorphic. Here's a real example of when I've wanted to use this:
class HasRing a where type Ring a instance HasRing [a] where type Ring [a] = a instance Hasring (Vector a) where type Ring (Vector a) = a newtype L2Norm a = L2Norm a deriving HasRing newtype L1Norm a = L1Norm a deriving HasRing
The deriving clauses would be equivalent to:
instance HasRing a => HasRing (L2Norm a) where type Ring (L2Norm a) = Ring a instance HasRing a => HasRing (L1Norm a) where type Ring (L1Norm a) = Ring a
This might become problematic if there are multiple type parameters though.
comment:4 Changed 6 years ago by
This auto-generation seems to be rather different from the way GeneralizedNewtypeDeriving
works in other contexts. In particular, the instances that you're generating are not directly related to any existing instances. Are you proposing that type families used on derived instances should just "look through" the newtype and be applied to the base type? Or only in cases with type variables? And, where does the HasRing a =>
constraint come from?
Without those constraints, I can see more of a coherent and general picture here... but it doesn't seem like GeneralizedNewtypeDeriving
to me. Perhaps you're really proposing a new extension for generation of type family instances for newtypes?
comment:5 Changed 5 years ago by
Component: | Compiler → Compiler (Type checker) |
---|
comment:6 Changed 5 years ago by
Milestone: | → 7.12.1 |
---|---|
Owner: | set to goldfire |
Encouraged by Iavor Diatchki and Adam Gundry, I've realized that my comment:4 is utterly wrong -- MikeIzbicki's proposal is reasonable.
Concretely, I propose:
GeneralizedNewtypeDeriving
for classes with associated types define new associated type instances that "look through" to the underlying type instance.
This satisfies Mike's original example. To my comment:1, it says Int
. And, this proposal works for comment:3.
Note that associated data
instances will still be prohibited -- these are not covered by this ticket.
I can implement in due course.
comment:7 Changed 5 years ago by
So, to be more specific, the recipe is this:
class C a where type T a op :: a -> a newtype T a = MkT <rep-type> deriving( C )
Here the deriving
clause would generate
instance C <rep-type> => C (T a) where type T (T a) = T <rep-type> op = coerce (op :: <rep-type> -> <rep-type>)
As usual, a wiki page to explain the details when we have to eta-reduce the newtype, etc, would be helpful.
Simon
comment:9 Changed 4 years ago by
Would this approach be able to work for associated injective type families? If you had something like this:
class C a where type T a = r | r -> a instance C Int where type T Int = Char newtype WrappedInt = WrapInt Int deriving C
Then, if I understand the above proposal, the following code would be generated:
instance C WrappedInt where type T WrappedInt = T Int
which would violate injectivity.
comment:10 Changed 4 years ago by
Milestone: | 8.0.1 → 8.2.1 |
---|
Yes, as well it should. Derived instances are still type-checked, so this would be caught with no special-casing. I could imagine that the error message would be hard to understand, but that's the worst that would happen.
But this isn't going to happen by the 8.0 feature freeze, I'm afraid.
comment:11 Changed 4 years ago by
Keywords: | TypeFamilies added |
---|
comment:12 Changed 3 years ago by
Cc: | RyanGlScott added |
---|
comment:13 Changed 3 years ago by
Related Tickets: | → #2721 |
---|
comment:14 Changed 3 years ago by
Hm... what code would generated in this example?
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} import Data.Kind class C (a :: k) where type T k :: Type instance C Int where type T Type = Int -------------------- newtype MyInt = MyInt Int deriving C
comment:15 Changed 3 years ago by
The definition of C
should be illegal since it doesn't mention the variable a
. Apparently that hasn't been fixed yet though, I thought it was?
comment:16 Changed 3 years ago by
Why should C
be illegal? The type parameters of T
are a permutation of a proper subset of the class parameters (a
and k
), so it should be legal.
But moreover, I think the answer to my question in comment:14 is: you can't newtype-derive C
for MyInt
, as there's an associated type that doesn't mention the last type parameter of C
. This is crucial, because if this doesn't hold, then we won't have a T
instance to fall back on, making the whole derivation crumble. We'd just need to check for this condition beforehand.
comment:17 Changed 3 years ago by
Oh that is a strange condition, but okay. (Maybe what I was thinking about was a new sanity condition on associated type instances, not their declarations.)
comment:18 Changed 3 years ago by
The recipe gave in comment:4 doesn't work for the example in comment:14. I could elaborate the recipe a bit thus:
class C x y z where type T y z x op :: x -> [y] -> z newtype N a = MkN <rep-type> deriving( C ) -- Here the deriving clause would generate instance C x y <rep-type> => C x y (N a) where type T y (N a) x = T y <rep-type> x op = coerce (op :: x -> [y] -> <rep-type>)
The recipe for generating the type instance
is to replace the occurrence of z
(which must occur) with <rep-type>
on the LHS and RHS. I don't think it need be the last parameter of T
, as the example shows.
I'm far from sure if this is really worth the effort of explaining and implementing it.
comment:19 Changed 3 years ago by
Owner: | changed from goldfire to RyanGlScott |
---|
Right, I didn't say the last type parameter of T
had to be the newtype. Rather, the last type parameter of the class C
(z
in the example in comment:18) just has to occur somewhere in the type parameters of T
.
I'm far from sure if this is really worth the effort of explaining and implementing it.
I disagree! Really, this is a quite straightforward idea (with a couple of small gotchas, like the one you observed), and I've implemented most of it already—I just need to polish up the documentation, update the GHC wiki, and post a Phabricator Diff.
comment:20 follow-up: 21 Changed 3 years ago by
Just to be clear on the design here: we plan on rejecting the code in comment:14, right? That is, for GND to work with associated types, the last parameter of the class must be mentioned in the associated type LHS. Then I'm on board.
comment:21 Changed 3 years ago by
Replying to goldfire:
Just to be clear on the design here: we plan on rejecting the code in comment:14, right? That is, for GND to work with associated types, the last parameter of the class must be mentioned in the associated type LHS. Then I'm on board.
Yes, precisely. I'll make sure to mention this fact in the users' guide.
comment:22 Changed 3 years ago by
Differential Rev(s): | → Phab:D2636 |
---|---|
Status: | new → patch |
comment:24 Changed 3 years ago by
Resolution: | → fixed |
---|---|
Status: | patch → closed |
Test Case: | → deriving/should_compile/T8165, deriving/should_fail/T8165_fail1, deriving/should_fail/T8165_fail2 |
comment:25 Changed 20 months ago by
Keywords: | deriving added |
---|
What should happen in this scenario:
What does
U E
reduce to,E
orInt
?