Version 2 (modified by 3 years ago) (diff) | ,
---|

# Update to Roles

It has become (somewhat) clear that the Roles mechanism as implemented in GHC 7.8 is insufficient. (See examples below.) This page is dedicated to creating a new design for roles that might fix the problems.

## Problem examples

We have three known examples of where current roles are failing us.

### Adding `join`

to `Monad`

As part of the Applicative-Monad Proposal, we wish to add `join`

to `Monad`

, thus:

class Applicative m => Monad m where ... join :: forall a. m (m a) -> m a

This is all well and good, and would work with GeneralizedNewtypeDeriving (GND) most of the time. But, consider this:

newtype T m a = T (m a) deriving (Functor, Applicative, Monad) readRef :: MonadIO m => IORef a -> T m a readRef = T . liftIO . readIORef

The designer of `T`

will export it abstractly, allowing only the reading of `IORef`

s in the `T`

monad but not other operations.

Sadly, the use of GND fails here, with `join`

in the `Monad`

class. Here is the relevant generated code:

instance Monad m => Monad (T m) where ... join = coerce (join :: m (m a) -> m a) :: forall a. T m (T m a) -> T m a

Thus, 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))`

.

This 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.

### The `MVector`

class

A redesign of the `vector`

package is underway, introducing the `Vector`

class, among other changes. Here is the offending method:

class (...) => Vector v a where basicUnsafeIndexM :: Monad m => v a -> Int -> m a ...

Here, `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`

.

### The `acme-schoenfinkel`

package

This 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

WrappedSchoenfinkel { unwrapSchoenfinkel :: cat a b } deriving (Alternative, Applicative, Arrow, ArrowApply, ArrowChoice, ArrowLoop, ArrowPlus, ArrowZero, Category, Functor)

GND fails on `ArrowApply`

:

class Arrow a => ArrowApply (a :: * -> * -> *) where app :: forall b c. a (a b c, b) c

The problem here echoes the `join`

problem quite closely.

## The best known solution

Edward Kmett initially described an approach in an email, roughly as follows (names subject to bikeshedding, as always):

Currently, `Data.Type.Coercion`

makes this definition:

data Coercion a b where Coercion :: Coercible a b => Coercion a b

Building on that, define a class `Rep`

like this:

class Rep (f :: k1 -> k2) where co :: Coercible a b => Coercion (f a) (f b)