| 93 | |
| 94 | The 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 | |
| 96 | Using this, we can define GND over `join` thus (continuing the [#join example] above): |
| 97 | |
| 98 | {{{ |
| 99 | instance (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 | |
| 106 | This compiles without difficulty. |
| 107 | |
| 108 | Of course, we need to bake this reasoning into the compiler and the existing `Coercible` solver, essentially with a `Coercible` "instance" like |
| 109 | |
| 110 | {{{ |
| 111 | instance (Rep f, Coercible a b) => Coercible (f a) (f b) |
| 112 | }}} |
| 113 | |
| 114 | We 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 | |
| 118 | 1. How far should instance generation go? For example, for the type |
| 119 | |
| 120 | {{{ |
| 121 | newtype ReaderT r m a = ReaderT (r -> m a) |
| 122 | }}} |
| 123 | |
| 124 | the instance |
| 125 | |
| 126 | {{{ |
| 127 | instance Rep m => Rep (ReaderT r m) |
| 128 | }}} |
| 129 | |
| 130 | can 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 | |
| 132 | 2. Should users be able to write instances for `Rep` by hand? They cannot do so for `Coercible`. |
| 133 | |
| 134 | 3. 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 | |
| 136 | 4. Should we do something analogous for phantom roles? |
| 137 | |
| 138 | === Open implementation questions === |
| 139 | |
| 140 | 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. |
| 141 | |
| 142 | 2. 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 | |
| 144 | 3. The `Coercible` solver is getting somewhat involved already (#9117, #9131) |