160 | | |
161 | | |
162 | | == Type functions == |
163 | | |
164 | | Follow as per type classes |
165 | | |
166 | | |
167 | | == Syntax of Kinds == |
168 | | |
169 | | {{{ |
170 | | kind ::= * | # | ? | (kind) | kind -> kind | |
171 | | ty :=: ty | forall var . kind | var |
172 | | }}} |
173 | | |
174 | | == Syntax of Types == |
175 | | |
176 | | Type syntax needs to be extended with a new binder. |
177 | | |
178 | | |
179 | | == Implementation route == |
180 | | |
181 | | Places that would be hit (TODO): |
182 | | |
183 | | * Parser |
184 | | * New Language Flag {-# PolymorphicKinds #-} ? |
185 | | * Syntax of kinds |
186 | | * Possibly syntax of function types |
187 | | |
188 | | * Type checker |
189 | | |
190 | | * Core / Core Lint |
191 | | |
192 | | * Module interfaces |
193 | | * To expose kind-quantified variables (does this drop out of any other change) |
194 | | |
195 | | * Test cases |
196 | | |
197 | | |
198 | | == To classify == |
199 | | |
200 | | Other 'issues' (probably non-issues). Kinds in rank-n types? |
201 | | foobar :: forall k1 (b :: k1) (c :: k1 -> *) . (forall k2 (e :: k2 -> *) (f :: k) . e f -> Int ) -> b c -> Int |
202 | | |
203 | | Impredicativity |
204 | | |
205 | | {{{ |
206 | | #!text/x-haskell |
207 | | data Proxy :: forall k . k -> * |
208 | | |
209 | | foo :: forall (m :: forall k . k -> *) . m Int -> m Maybe -> Int -- This is ok |
210 | | |
211 | | bar = foo Proxy Proxy |
212 | | }}} |
213 | | |
214 | | {{{ |
215 | | #!text/x-haskell |
216 | | data Foo :: forall k . k -> * |
217 | | |
218 | | foo :: forall (m :: (forall k . k -> *) -> *) . m Proxy -> Int -- This line is ok |
219 | | -- has a higher |
220 | | -- ranked kind, but |
221 | | -- that's not an |
222 | | -- issue as we |
223 | | -- have to be |
224 | | -- explicit |
225 | | |
226 | | bar = foo Foo -- This is impredicative (and rejected) as it requires instantiating |
227 | | -- Foo's k to (forall k . k -> *) |
228 | | }}} |