204 | | The implementation of newtypes has changed to include explicit type coercions in the place of the previously used ad-hoc mechanism. When a newtype |
205 | | |
206 | | {{{newtype T a = MkT (T a -> T a)}}} |
207 | | |
208 | | is declared, a new !TyCon called CoT is created, and is stored in the |
209 | | type constructor. The new TyCon has the ame arity as the newtype type |
210 | | constructor, in this case one. The TyCon does not have a kind on its |
211 | | own, only when fully applied to its arguments. In this case we have |
212 | | |
213 | | {{{CoT Int :: T Int :=: (T Int -> T Int)}}} |
214 | | |
215 | | This coercion is used to wrap and unwrap newtypes whenever the constructor or case is used in the Haskell source code. |
216 | | |
217 | | Such coercions are always used when the newtype is recursive and are optional for non-recursive newtypes. This can be easily changed by altering the function mkNewTyConRhs in iface/BuildTyCl.lhs. |
| 204 | The implementation of newtypes has changed to include explicit type coercions in the place of the previously used ad-hoc mechanism. |
| 205 | For a newtype declared by |
| 206 | {{{ |
| 207 | newtype T a = MkT (a -> a) |
| 208 | }}} |
| 209 | the `NewTyCon` for `T` will contain n`t_co = CoT` where `CoT t : T t :=: t -> |
| 210 | t`. This `TyCon` is a `CoercionTyCon`, so it does not have a kind on its |
| 211 | own; it basically has its own typing rule for the fully-applied |
| 212 | version. If the newtype `T` has k type variables hen `CoT` has arity at |
| 213 | most k. In the case that the right hand side is a type application |
| 214 | ending with the same type variables as the left hand side, we |
| 215 | "eta-contract" the coercion. So if we had |
| 216 | {{{ |
| 217 | newtype S a = MkT [a] |
| 218 | }}} |
| 219 | then we would generate the arity 0 coercion `CoS : S :=: []`. The |
| 220 | primary reason we do this is to make newtype deriving cleaner. If the coercion |
| 221 | cannot be reduced in this fashion, then it has the same arity as the tycon. |
| 222 | |
| 223 | In the paper we'd write |
| 224 | {{{ |
| 225 | axiom CoT : (forall t. T t) :=: (forall t. [t]) |
| 226 | }}} |
| 227 | and then when we used `CoT` at a particular type, `s`, we'd say |
| 228 | {{{ |
| 229 | CoT @ s |
| 230 | }}} |
| 231 | which encodes as `(TyConApp instCoercionTyCon [TyConApp CoT [], s])` |
| 232 | |
| 233 | But in GHC we instead make `CoT` into a new piece of type syntax |
| 234 | (like `instCoercionTyCon`, `symCoercionTyCon` etc), which must always |
| 235 | be saturated, but which encodes as |
| 236 | {{{ |
| 237 | TyConApp CoT [s] |
| 238 | }}} |
| 239 | In the vocabulary of the paper it's as if we had axiom declarations |
| 240 | like |
| 241 | {{{ |
| 242 | axiom CoT t : T t :=: [t] |
| 243 | }}} |
| 244 | The newtype coercion is used to wrap and unwrap newtypes whenever the constructor or case is used in the Haskell source code. |
| 245 | |
| 246 | Such coercions are always used when the newtype is recursive and are optional for non-recursive newtypes. Whether or not they are used can be easily changed by altering the function mkNewTyConRhs in iface/BuildTyCl.lhs. |