Changes between Version 11 and Version 12 of Roles2
 Timestamp:
 Jul 26, 2018 11:58:24 AM (15 months ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

Roles2
v11 v12 164 164 4. Should we do something analogous for phantom roles? 165 165 166 5. (Comment from Dominique Devriese) 167 Should `Functor f` have `Rep f` as a parent constraint? After all, if `Coercible a b` then we can already convert from `f a` to `f b` using `fmap coerce` and the parametricity of `fmap` implies that it can't function in a typespecific way, so I suspect that, together with the functor identity law, this somehow implies that `fmap coerce` must necessarily function the same as a lowlevel coerce. 168 166 169 === Open implementation questions === 167 170 … … 193 196 == Other possible designs == 194 197 195 1. The design from the [http://www.seas.upenn.edu/~sweirich/papers/popl163afweirich.pdf POPL'11 paper]. This design incorporates roles into kinds. It solves the exact problems here, but at great cost: because roles are attached to kinds, we have to choose a types roles in the wrong place. For example, consider the `Monad` class. Should the parameter `m` have type `*/R > *`, requiring all monads to take representational arguments, or should it have type `*/N >*`, disallowing GND if `join` is in the `Monad` class? We're stuck with a different set of problems. And, there is the pervasiveness of this change, which is why we didn't implement it in the first place. 198 1. The design from the [http://www.seas.upenn.edu/~sweirich/papers/popl163afweirich.pdf POPL'11 paper]. This design incorporates roles into kinds. It solves the exact problems here, but at great cost: because roles are attached to kinds, we have to choose a types roles in the wrong place. For example, consider the `Monad` class. Should the parameter `m` have kind `*/R > *`, requiring all monads to take representational arguments, or should it have type `*/N >*`, disallowing GND if `join` is in the `Monad` class? We're stuck with a different set of problems. And, there is the pervasiveness of this change, which is why we didn't implement it in the first place. 199 * (comment from Dominique Devriese) Note that `Monad` implies `Functor`, so by the argument about `Functor f` implying `Rep f` above, I would argue that `m` should have kind `*/R > *`. 196 200 197 201 2. (This is just Richard thinking out loud. It may be gibberish.) What if we generalize roles to be parameterized? To make the definitions wellformed, roles would be attached directly to type constructors (not the parameters), but be a mapping from 1indexed natural numbers to roles. As an example, `ReaderT`'s role would be `[1 > R, 2 > R, 3 > ((2.1 ~ R) => R; N)]`. The first two entries just say that parameters `r` and `m` have representational roles. The last entry (`3 > ((2.1 ~ R) => R; N)`) says that, if `m`'s first parameter (that is, parameter `2.1`, where the `.` is some sort of indexing operator  not a decimal point!) is representational, then so is `a`; otherwise, `a` is nominal. This defaulting behavior does ''not'' cause coherence problems, as long as the roles are listed in order from phantom to nominal  if GHC can't prove a more permissive role, a more restrictive one is assumed.