Changes between Version 2 and Version 3 of Roles2


Ignore:
Timestamp:
May 22, 2014 6:33:35 PM (16 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Roles2

    v2 v3  
    11= Update to Roles =
    22
    3 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.
     3It has become (somewhat) clear that the Roles mechanism as implemented in GHC 7.8 is insufficient. (See [#examples examples] below.) This page is dedicated to creating a new design for roles that might fix the problems.
    44
    5 == Problem examples ==
     5== [=#examples Problem examples] ==
    66
    77We have three known examples of where current roles are failing us.
    88
    9 === Adding `join` to `Monad` ===
     9=== [=#join Adding `join` to `Monad`] ===
    1010
    1111As part of the [http://www.haskell.org/haskellwiki/Functor-Applicative-Monad_Proposal Applicative-Monad Proposal], we wish to add `join` to `Monad`, thus:
     
    9191  co :: Coercible a b => Coercion (f a) (f b)
    9292}}}
     93
     94The idea is that a type is in the `Rep` class if its ''next'' parameter is representational. Thus, we would have instances `Rep Maybe`, `Rep []`, `Rep Either`, `Rep (Either a)`, etc. We would ''not'' have `Rep G`, where `G` is a GADT.
     95
     96Using this, we can define GND over `join` thus (continuing the [#join example] above):
     97
     98{{{
     99instance (Rep m, Monad m) => Monad (T m) where
     100  ...
     101  join   = case co :: Coercion (m (m a)) (m (T m a)) of
     102             Coercion -> coerce (join :: m (m a) -> m a)
     103           :: forall a. T m (T m a) -> T m a
     104}}}
     105
     106This compiles without difficulty.
     107
     108Of course, we need to bake this reasoning into the compiler and the existing `Coercible` solver, essentially with a `Coercible` "instance" like
     109
     110{{{
     111instance (Rep f, Coercible a b) => Coercible (f a) (f b)
     112}}}
     113
     114We also would want automatic generation of instances of `Rep`, not unlike the generation of instances for `Coercible`.
     115
     116=== Open user-facing design questions ===
     117
     1181. How far should instance generation go? For example, for the type
     119
     120{{{
     121newtype ReaderT r m a = ReaderT (r -> m a)
     122}}}
     123
     124the instance
     125
     126{{{
     127instance Rep m => Rep (ReaderT r m)
     128}}}
     129
     130can be written. Should this be inferred? I (Richard) can imagine a beefed up role inference algorithm which could figure this out. But, perhaps there exist harder cases that would not be inferrable.
     131
     1322. Should users be able to write instances for `Rep` by hand? They cannot do so for `Coercible`.
     133
     1343. What should the method in `Rep` be? `Coercion a b -> Coercion (f a) (f b)`, `Coercible a b => Coercion (f a) (f b)`, and `Coercible a b => Coercible (f a) (f b)` (definable internally) are all contenders.
     135
     1364. Should we do something analogous for phantom roles?
     137
     138=== Open implementation questions ===
     139
     1401. Currently, all coercions (including representational ones) are unboxed (and thus take up exactly 0 bits) in a running program. (We ignore `-fdefer-type-errors` here.) But, Core has no way of expressing ''functions'' in the coercion language, and the `co` method above essentially desugars to a coercion function. Either we have to add functions to the language of coercions, or we have to keep the coercions generated by `Rep` instances boxed at runtime, taking of the space of a pointer and potentially an unevaluated thunk.
     141
     1422. 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.
     143
     1443. The `Coercible` solver is getting somewhat involved already (#9117, #9131)