Changes between Version 2 and Version 3 of Roles


Ignore:
Timestamp:
Aug 1, 2013 11:49:15 AM (19 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Roles

    v2 v3  
    104104 
    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. 
     106 
     107== Roles and `Traversable` == 
     108 
     109Though a minor issue in the overall scheme, work on Roles had led to an interesting interaction with `Traversable`, excerpted here: 
     110 
     111{{{ 
     112class Traversable t where 
     113  traverse :: Applicative f => (a -> f b) -> t a -> f (t b) 
     114}}} 
     115 
     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. 
     117 
     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. 
     119 
     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: 
     121 
     122{{{ 
     123data G a where 
     124  GInt :: a -> G Int 
     125  Ga   :: a -> G a 
     126 
     127instance Functor G where 
     128  fmap f (GInt _) = error "urk"  -- no way out here 
     129  fmap f (Ga a)   = Ga (f a) 
     130 
     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 
     135}}} 
     136 
     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!