Changes between Version 9 and Version 10 of Roles2


Ignore:
Timestamp:
Jun 2, 2014 4:35:20 PM (14 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Roles2

    v9 v10  
    1711712. (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.
    172172
    173 Under this scenario, `StateT`'s role would be `[1 |-> (2.1 ~ R => R; N), 2 |-> R, 3 |-> (2.1 ~ R => R; N)]`.
     173  Under this scenario, `StateT`'s role would be `[1 |-> (2.1 ~ R => R; N), 2 |-> R, 3 |-> (2.1 ~ R => R; N)]`.
    174174
    175 To implement this, we would probably need role ''evidence'' sloshing around, not unlike coercions. This evidence would be consumed by appropriately beefed up coercion forms (particularly, the !TyConAppCo case). It would be produced by role ''axioms'' at every data- and newtype definition.
     175  To implement this, we would probably need role ''evidence'' sloshing around, not unlike coercions. This evidence would be consumed by appropriately beefed up coercion forms (particularly, the !TyConAppCo case). It would be produced by role ''axioms'' at every data- and newtype definition.
    176176
    177 This design seems something like a middle road between the flexibility and modularity (that is, roles and kinds are distinct) that we have now and the completeness offered by the POPL'11 solution.
     177  This design seems something like a middle road between the flexibility and modularity (that is, roles and kinds are distinct) that we have now and the completeness offered by the POPL'11 solution.