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 | | |