Changes between Version 1 and Version 2 of Roles2

May 22, 2014 6:01:32 PM (12 months ago)



  • Roles2

    v1 v2  
    2222newtype T m a = T (m a) 
    2323  deriving (Functor, Applicative, Monad) 
     25readRef :: MonadIO m => IORef a -> T m a 
     26readRef = T . liftIO . readIORef 
     29The designer of `T` will export it abstractly, allowing only the reading of `IORef`s in the `T` monad but not other operations. 
     31Sadly, the use of GND fails here, with `join` in the `Monad` class. Here is the relevant generated code: 
     34instance Monad m => Monad (T m) where 
     35  ... 
     36  join = coerce (join :: m (m a) -> m a) :: forall a. T m (T m a) -> T m a 
     39Thus, GHC must derive `Coercible (m (m a) -> m a) (T m (T m a) -> T m a)`. This requirement reduces (in part) to `Coercible (m (m a)) (T m (T m a))`. We try to solve this by applying a newtype-unwrapping instance, `Coercible x (m a) => Coercible x (T m a)`. Then, we must solve `Coercible (m (m a)) (m (T m a))`. And here, we are stuck. We do know `Coercible (m a) (T m a)`, but we don't know the role of `m`'s parameter, and must assume (for safety) that it could be nominal. Thus, we can't solve for `Coercible (m (m a)) (m (T m a))`. 
     41This problem would occur if `join` were in `Monad` and a programmer used GND on any monad transformer. This is a common enough idiom to make us want to fix the situation. 
     43=== The `MVector` class === 
     45A redesign of the `vector` package is underway, introducing the `Vector` class, among other changes. Here is the offending method: 
     48class (...) => Vector v a where 
     49  basicUnsafeIndexM :: Monad m => v a -> Int -> m a 
     50  ... 
     53Here, `a` is the type of the thing stored in the vector, and it is natural to want to coerce a vector of `Int`s to a vector of `Age`s. But, GND would not work here, for very similar reasons to the case above -- we won't be able to coerce `m Int` to `m Age`, because we don't know enough about `m`. 
     55=== The `acme-schoenfinkel` package === 
     57This next example is the one known case of type-safe code that existed before GHC 7.8 that does not work with GHC 7.8's roles. The package `acme-schoenfinkel-0.1.1` package (by Ertugrul Söylemez) defines 
     60    WrappedSchoenfinkel { 
     61      unwrapSchoenfinkel :: cat a b 
     62    } 
     63    deriving (Alternative, Applicative, Arrow, ArrowApply, 
     64              ArrowChoice, ArrowLoop, ArrowPlus, ArrowZero, 
     65              Category, Functor) 
     68GND fails on `ArrowApply`: 
     71class Arrow a => ArrowApply (a :: * -> * -> *) where 
     72  app :: forall b c. a (a b c, b) c 
     75The problem here echoes the `join` problem quite closely. 
     77== The best known solution == 
     79Edward Kmett initially described an approach in an [ email], roughly as follows (names subject to bikeshedding, as always): 
     81Currently, `Data.Type.Coercion` makes this definition: 
     84data Coercion a b where 
     85  Coercion :: Coercible a b => Coercion a b 
     88Building on that, define a class `Rep` like this: 
     90class Rep (f :: k1 -> k2) where 
     91  co :: Coercible a b => Coercion (f a) (f b)