Changes between Version 3 and Version 4 of Roles2


Ignore:
Timestamp:
May 22, 2014 7:00:25 PM (12 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Roles2

    v3 v4  
    1421422. The `ReaderT` example defined `ReaderT` as a newtype. The `Rep` instance shown is indeed writable by hand, right now. But, if `ReaderT` were defined as a ''data'' type, the `Rep` instance would be impossible to write, as there are no newtype-unwrapping instances. It seems a new form of axiom would be necessary to implement this trick for data types. This axiom would have to be produced at the data type definition, much like how newtype axioms are produced with newtype definitions. 
    143143 
    144 3. The `Coercible` solver is getting somewhat involved already (#9117, #9131) 
     1443. The `Coercible` solver is getting somewhat involved already (#9117, #9131). Can this be incorporated cleanly? We surely hope that the solver is sound with respect to the definition of representational coercions in Core. How complete is it? How will this affect completeness? In other words, will adding this extension necessarily mean that there are more types that are provably representationally equal but which GHC is unable to find this proof? 
     145 
     146=== Other issues === 
     147 
     1481. There is a weird asymmetry here. If we know `(Rep f, Coercible f g, Coercible a b)`, we can prove `Coercible (f a) (g b)`. We do this by proving `Coercible (f a) (f b)` and then `Coercible (f b) (g b)` and using transitivity. But, note that we do ''not'' know `Rep g`! Furthermore, `(Rep f, Coercible f g)` do ''not'' imply `Rep g` in the presence of role annotations: 
     149 
     150{{{ 
     151newtype MyMaybe a = Mk (Maybe a) 
     152type role MyMaybe nominal 
     153}}} 
     154 
     155Here, we have `Rep Maybe` and `Coercible Maybe MyMaybe` but not `Rep MyMaybe`. This is all very strange. Of course, we ''could'' define an instance `Rep MyMaybe`, despite the role annotation, by using the newtype-unwrapping instance. But, what does this mean if the author wants to export `MyMaybe` abstractly? 
     156 
     1572. Consider the `StateT` newtype: 
     158 
     159{{{ 
     160newtype StateT s m a = StateT (s -> m (a, s)) 
     161}}} 
     162 
     163Its roles are `nominal representational nominal`. But, if we have `Rep m`, then the roles could all be representational. For the `a` parameter, this is just like `ReaderT`. But, we are stuck with the `s` parameter, simply because the `s` parameter comes ''before'' `m` in the parameter list. There's no way to assert something about `m` when describing a property of `s`. 
     164 
     165== Other possible designs == 
     166 
     1671. 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. 
     168 
     1692. (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. 
     170 
     171Under this scenario, `StateT`'s role would be `[1 |-> (2.1 ~ R => R; N), 2 |-> R, 3 |-> (2.1 ~ R => R; N)]`. 
     172 
     173To 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. 
     174 
     175This 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.