| 81 | | = Kind-polymorphic `Typeable` = |
| 82 | | |
| 83 | | The paper describes an improved implementation of `Typeable` (section 2.5). This has not |
| 84 | | yet been implemented; the current `Typeable` class is: |
| 85 | | {{{ |
| 86 | | class Typeable (a :: *) where |
| 87 | | typeOf :: a -> TypeRep |
| 88 | | }}} |
| 89 | | |
| 90 | | The new proposal makes it into: |
| 91 | | {{{ |
| 92 | | data Proxy a = Proxy |
| 93 | | |
| 94 | | class Typeable a where |
| 95 | | typeRep :: Proxy a -> TypeRep |
| 96 | | }}} |
| 97 | | Note that `Proxy` is kind polymorphic, and so is the new `Typeable`: its type argument |
| 98 | | `a` can have any kind `k`. The paper goes on to describe how we can then give |
| 99 | | kind-specific instances: |
| 100 | | {{{ |
| 101 | | instance Typeable Int where typeRep _ = ... |
| 102 | | |
| 103 | | instance Typeable [] where typeRep _ = ... |
| 104 | | }}} |
| 105 | | |
| 106 | | The following changes need to done in the compiler: |
| 107 | | * Update `Data.Typeable` in `base` (mostly deleting classes and adding `Proxy`). |
| 108 | | |
| 109 | | * Rewrite the `deriving Typeable` mechanism in `TcGenDeriv`. |
| 110 | | |
| 111 | | From the user's perspective nothing has to change. We can make the new implementation |
| 112 | | backwards-compatible by: |
| 113 | | * Calling the method of `Typeable` `typeRep`, and not `typeOf` |
| 114 | | * Defining `typeOf`, `typeOf1`, ..., separately |
| 115 | | |
| 116 | | Concretely, the new `Data.Typeable` will look something like this: |
| 117 | | {{{ |
| 118 | | {-# LANGUAGE ScopedTypeVariables #-} |
| 119 | | {-# LANGUAGE PolyKinds #-} |
| 120 | | |
| 121 | | -- Type representation: unchanged |
| 122 | | data TypeRep = ... |
| 123 | | |
| 124 | | -- Kind-polymorphic proxy |
| 125 | | data Proxy t = Proxy |
| 126 | | |
| 127 | | -- Kind-polymorphic Typeable |
| 128 | | class Typeable a where |
| 129 | | typeRep :: Proxy a -> TypeRep |
| 130 | | |
| 131 | | -- Instances for base types |
| 132 | | instance Typeable Char where ... |
| 133 | | instance Typeable [] where ... |
| 134 | | instance Typeable Either where ... |
| 135 | | |
| 136 | | -- Old methods for backwards compatibility |
| 137 | | typeOf :: forall a. Typeable a => a -> TypeRep |
| 138 | | typeOf x = typeRep (getType x) where |
| 139 | | getType :: a -> Proxy a |
| 140 | | getType _ = Proxy |
| 141 | | |
| 142 | | typeOf1 :: forall t (a :: *). Typeable t => t a -> TypeRep |
| 143 | | typeOf1 x = typeRep (getType1 x) where |
| 144 | | getType1 :: t a -> Proxy t |
| 145 | | getType1 _ = Proxy |
| 146 | | }}} |
| 147 | | |
| 148 | | This is nearly enough; remember that currently we can do things like this: |
| 149 | | {{{ |
| 150 | | typeOf "p" |
| 151 | | typeOf1 "p" |
| 152 | | }}} |
| 153 | | And they mean different things: the first is the representation of `[Char]`, |
| 154 | | whereas the second is the representation of `[]`. In particular, |
| 155 | | `typeOf1 "p" == typeOf1 [()]`, for instance. To keep this behavior we have |
| 156 | | to guarantee that a datatype `T` with type parameters `a1` through `an` gets instances: |
| 157 | | {{{ |
| 158 | | data T a1 ... an |
| 159 | | |
| 160 | | instance Typeable T |
| 161 | | instance (Typeable a1) => Typeable (T a1) |
| 162 | | ... |
| 163 | | instance (Typeable a1, ..., Typeable an) => Typeable (T a1 ... an) |
| 164 | | }}} |
| 165 | | |
| 166 | | We can do this as before, by defining the arity `n-1` instance from the |
| 167 | | arity `n` instance: |
| 168 | | |
| 169 | | {{{ |
| 170 | | instance (Typeable t, Typeable (a :: *)) => Typeable (t a) |
| 171 | | instance (Typeable t, Typeable (a :: *), Typeable (b :: *)) => Typeable (t a b) |
| 172 | | }}} |
| 173 | | |
| 174 | | If we're willing to use `-XUndecidableInstances`, we can even do this with |
| 175 | | a single instance, relying on `-XPolyKinds`: |
| 176 | | {{{ |
| 177 | | instance (Typeable t, Typeable a) => Typeable (t a) |
| 178 | | }}} |
| 179 | | In this instance, `t` has kind `k -> *` and `a` has kind `k`. |
| 180 | | |