Changes between Version 2 and Version 3 of Roles

Aug 1, 2013 11:49:15 AM (4 years ago)



  • Roles

    v2 v3  
    105105I (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.
     107== Roles and `Traversable` ==
     109Though a minor issue in the overall scheme, work on Roles had led to an interesting interaction with `Traversable`, excerpted here:
     112class Traversable t where
     113  traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
     116According 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.
     118This 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.
     120Despite 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:
     123data G a where
     124  GInt :: a -> G Int
     125  Ga   :: a -> G a
     127instance Functor G where
     128  fmap f (GInt _) = error "urk"  -- no way out here
     129  fmap f (Ga a)   = Ga (f a)
     131instance Applicative G where
     132  pure a = Ga a
     133  (Ga f) <*> (Ga a) = Ga (f a)
     134  _ <*> _ = error "urk" -- no way out here, either
     137There'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!