... | ... | @@ -122,3 +122,40 @@ data Bar (a@R :: k) |
|
|
|
|
|
|
|
|
I (Richard E) propose the syntax for `Foo`, for no reason I can articulate. Note that the parentheses enclosing the kind annotation are required whether or not there is a role annotation.
|
|
|
|
|
|
## Roles and `Traversable`
|
|
|
|
|
|
|
|
|
Though a minor issue in the overall scheme, work on Roles had led to an interesting interaction with `Traversable`, excerpted here:
|
|
|
|
|
|
```wiki
|
|
|
class Traversable t where
|
|
|
traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
|
|
|
```
|
|
|
|
|
|
|
|
|
According to the rules for roles, the parameter `t` must be at role N, as it is used as a parameter to the type variable `f`. We must account for the possibility that `f` will be instantiated with a type whose last parameter is at role N, so we force `t` to be at role N as well.
|
|
|
|
|
|
|
|
|
This means that GeneralizedNewtypeDeriving (hereafter "GND") no longer works with Traversable. But, DeriveTraversable *does* still work. However, GHC previously preferred using GND over DeriveTraversable when both were available, which assumedly produced the same code. How is this all possible? If GND doesn't work anymore, is there something wrong with DeriveTraversable? The answer is that GND and DeriveTraversable make *different* instances, contrary to expectations. The reason is that DeriveTraversable has to use `fmap` to cast the result of `traverse` from the representation type back to the newtype. According to the Functor laws, `fmap`ping this cast should be a no-op (the law of interest is `fmap id == id`). But, if that law is not obeyed, `fmap`ping the cast may change the result of the `traverse`. Contrast this with a GND instance, which magically casts the result, without using `fmap`. If the Functor law is not obeyed, these two instances have different behavior.
|
|
|
|
|
|
|
|
|
Despite this, I believe that using GND with `Traversable` is indeed type-safe. Why? Because of the parametricity guaranteed in `Functor` and `Applicative`. The reason GND is prohibited with `Traversable` is that we are worried `f`'s last parameter will be at role N. While it is possible to write `Functor` and `Applicative` instances for such a type, the methods of those classes can't really use the any constructors that force the role to be N. For example, consider this:
|
|
|
|
|
|
```wiki
|
|
|
data G a where
|
|
|
GInt :: a -> G Int
|
|
|
Ga :: a -> G a
|
|
|
|
|
|
instance Functor G where
|
|
|
fmap f (GInt _) = error "urk" -- no way out here
|
|
|
fmap f (Ga a) = Ga (f a)
|
|
|
|
|
|
instance Applicative G where
|
|
|
pure a = Ga a
|
|
|
(Ga f) <*> (Ga a) = Ga (f a)
|
|
|
_ <*> _ = error "urk" -- no way out here, either
|
|
|
```
|
|
|
|
|
|
|
|
|
There's no way to usefully interact with the `GInt` constructor and get the code to type-check. Thus, I believe (but haven't yet proved), that using GND with `Traversable` is safe, because the `f` in `traverse` can't ever do bad things with its argument. If you, the reader, have more insight into this (or a counterexample!), please write! |