Changes between Version 1 and Version 2 of Roles2

May 22, 2014 6:01:32 PM (18 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)