Changes between Version 11 and Version 12 of Roles2


Ignore:
Timestamp:
Jul 26, 2018 11:58:24 AM (13 months ago)
Author:
dominiquedevriese
Comment:

Two comments about the role of the argument type of a monad m

Legend:

Unmodified
Added
Removed
Modified
  • Roles2

    v11 v12  
    1641644. Should we do something analogous for phantom roles?
    165165
     1665. (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 type-specific way, so I suspect that, together with the functor identity law, this somehow implies that `fmap coerce` must necessarily function the same as a low-level coerce.
     168
    166169=== Open implementation questions ===
    167170
     
    193196== Other possible designs ==
    194197
    195 1. The design from the [http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.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.
     1981. The design from the [http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.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 -> *`.
    196200
    1972012. (This is just Richard thinking out loud. It may be gibberish.) What if we generalize roles to be parameterized? To make the definitions well-formed, roles would be attached directly to type constructors (not the parameters), but be a mapping from 1-indexed 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.