... | ... | @@ -192,6 +192,9 @@ instance Rep m => Rep (ReaderT r m) |
|
|
|
|
|
1. Should we do something analogous for phantom roles?
|
|
|
|
|
|
1. (Comment from Dominique Devriese)
|
|
|
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.
|
|
|
|
|
|
### Open implementation questions
|
|
|
|
|
|
1. 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.
|
... | ... | @@ -223,7 +226,9 @@ newtype StateT s m a = StateT (s -> m (a, s)) |
|
|
|
|
|
## Other possible designs
|
|
|
|
|
|
1. The design from the [ POPL'11 paper](http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf). 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.
|
|
|
1. The design from the [ POPL'11 paper](http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf). 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.
|
|
|
|
|
|
- (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 -> *`.
|
|
|
|
|
|
1. (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.
|
|
|
|
... | ... | |