Changes between Version 1 and Version 2 of KindSystem
 Timestamp:
 Oct 16, 2008 10:59:15 AM (6 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

KindSystem
v1 v2 5 5 == Rationale == 6 6 7 Haskell has a very powerful and expressive static type system. The problem is 8 when you come to do any programming at the type level, that is typed by an 9 unsatisfactorily inexpressive kind system. We propose to make it just a little 10 bit stronger. 11 12 Note: the aim here initially is to implement a small useful extension to Haskell, and not 13 to retrofit the entirety of e.g. [http://web.cecs.pdx.edu/~sheard/Omega/index.html Omega] into GHC (yet ;)) 7 Haskell has a very powerful and expressive static type system. The problem is when you come to do any programming at the type level, that is typed by an unsatisfactorily inexpressive kind system. We propose to make it just a little bit stronger. 8 9 Note: the aim here initially is to implement a small useful extension to Haskell, and not to retrofit the entirety of e.g. [http://web.cecs.pdx.edu/~sheard/Omega/index.html Omega] into GHC yet ;)) 14 10 15 11 == Motivation == 16 12 17 Consider the simple example of lists parameterised by their lengths. There are 18 many variations on this theme in the Haskell lore, this authors favourite 19 follows thusly: 13 Consider the simple example of lists parameterised by their lengths. There are many variations on this theme in the Haskell lore, this authors favourite follows thusly: 20 14 21 15 {{{ … … 31 25 There are many eugh moments in this code: 32 26 33 * We first declare two new types ({{{Zero}}} and {{{Succ}}}), and, thanks to the EmpyDataDecls extension, say 34 that they are uninhabited by values (except bottom/error). 35 * {{{Zero}}} has kind {{{*}}}, and {{{Succ}}} has kind {{{* > *}}}, so it is perfectly 36 valid to create a haskell function with a signature: 27 * We first declare two new types ({{{Zero}}} and {{{Succ}}}), and, thanks to the EmpyDataDecls extension, say that they are uninhabited by values (except bottom/error). 28 * {{{Zero}}} has kind {{{*}}}, and {{{Succ}}} has kind {{{* > *}}}, so it is perfectly valid to create a haskell function with a signature: 37 29 38 30 {{{ … … 41 33 }}} 42 34 43 Really the programmers intent is that {{{Zero}}} and {{{Succ}}} are in a disjoint 44 namespace from *kinded types, and thus this function signature should be 45 disallowed. 46 47 * {{{Succ}}} has kind {{{* > *}}}, whereas really the programmer wants to 48 enforce that the argument to {{{Succ}}} will only ever consist of {{{Zero}}}s or 49 {{{Succ}}}s. i.e. the {{{* > *}}} kind given to {{{Succ}}} is far to relaxed. 35 Really the programmers intent is that {{{Zero}}} and {{{Succ}}} are in a disjoint namespace from *kinded types, and thus this function signature should be disallowed. 36 37 * {{{Succ}}} has kind {{{* > *}}}, whereas really the programmer wants to enforce that the argument to {{{Succ}}} will only ever consist of {{{Zero}}}s or {{{Succ}}}s. i.e. the {{{* > *}}} kind given to {{{Succ}}} is far to relaxed. 50 38 51 39 * We then decalare a new data type to hold lists parameterised by their lengths. 52 * {{{List}}} has kind {{{* > * > *}}}, which really doesn't tell us anything 53 other than its arity. An alternative definition could have been: 54 {{{data List item len where ... }}}, although this adds only pedagogical 55 information, and nothing new that the compiler can statically check. 56 57 * The {{{Cons}}} constructor actually has a mistake in it. The second 58 argument ({{{List n a}}}) has the names to the type parameters flipped. The 59 compiler cannot detect this, and the error will become apparant at use sites 60 which are at a distance from this declaration site. 61 62 * Nothing stops a user creating the silly type {{{List Int Int}}} even 63 though the intention is that the second argument is structured out of 64 {{{Succ}}}s and {{{Zero}}}s. 65 66 We propose to add new base kinds other than {{{*}}} using a simple notation. The 67 above example ''could'' become: 40 * {{{List}}} has kind {{{* > * > *}}}, which really doesn't tell us anything other than its arity. An alternative definition could have been: {{{data List item len where ... }}}, although this adds only pedagogical information, and nothing new that the compiler can statically check. 41 42 * The {{{Cons}}} constructor actually has a mistake in it. The second argument ({{{List n a}}}) has the names to the type parameters flipped. The compiler cannot detect this, and the error will become apparant at use sites which are at a distance from this declaration site. 43 44 * Nothing stops a user creating the silly type {{{List Int Int}}} even though the intention is that the second argument is structured out of {{{Succ}}}s and {{{Zero}}}s. 45 46 We propose to add new base kinds other than {{{*}}} using a simple notation. The above example ''could'' become: 68 47 69 48 {{{ … … 79 58 80 59 81 * We first declare a new ''kind'' {{{Nat}}}, that is defined by two types, {{{Zero}}} 82 and {{{Succ}}}. Although {{{Zero}}} and {{{Succ}}} are types, they do not classify any 83 haskell values (including undefined/bottom). So the {{{foo :: Zero > Succ Zero 84 > Bool}}} type signature from earlier would be rejected by the compiler. 85 86 * We then declare the type {{{List}}}, but we now say the second argument to 87 {{{List}}} has to be a type of kind {{{Nat}}}. With this extra information, the 88 compiler can statically detect our erroneous {{{Cons}}} declaration and would also 89 reject silly types like {{{List Int Int}}}. 60 * We first declare a new ''kind'' {{{Nat}}}, that is defined by two types, {{{Zero}}} and {{{Succ}}}. Although {{{Zero}}} and {{{Succ}}} are types, they do not classify any haskell values (including undefined/bottom). So the {{{ foo :: Zero > Succ Zero > Bool }}} type signature from earlier would be rejected by the compiler. 61 62 * We then declare the type {{{List}}}, but we now say the second argument to {{{List}}} has to be a type of kind {{{Nat}}}. With this extra information, the compiler can statically detect our erroneous {{{Cons}}} declaration and would also reject silly types like {{{List Int Int}}}. 90 63 91 64 == Declaration Syntax == … … 93 66 === ADT syntax === 94 67 95 The idea would be to mirror existing Haskell data declarations. There is a 96 clear analogy as we are now creating new kinds consiting of type constructors as 97 opposed to new types consisting of data constructors. 98 99 To destinguish kind declarations from data declarations we can either add a new 100 form of ''kind'' declaration: 68 The idea would be to mirror existing Haskell data declarations. There is a clear analogy as we are now creating new kinds consiting of type constructors as opposed to new types consisting of data constructors. 69 70 To destinguish kind declarations from data declarations we can either add a new form of ''kind'' declaration: 101 71 102 72 {{{ … … 107 77 However this steals {{{kind}}} as syntax with the usual problems of breaking existing programs. 108 78 109 Alternatively (preferably), we can add a modifier to data declarations to 110 indicate that we mean a kind declaration: 79 Alternatively (preferably), we can add a modifier to data declarations to indicate that we mean a kind declaration: 111 80 112 81 {{{ … … 117 86 == Interaction with GADTs == 118 87 119 GADTs can already be annotated with a mixture of names with optional explicit 120 kind signatures and just kind signatures. These kind signatures would 121 now be able to refer to the newly declared, non* kinds. However the ultimate 122 kind of a GADT must still be {{{*}}}. i.e. 88 GADTs can already be annotated with a mixture of names with optional explicit kind signatures and just kind signatures. These kind signatures would now be able to refer to the newly declared, non* kinds. However the ultimate kind of a GADT must still be {{{*}}}. i.e. 123 89 124 90 {{{ … … 132 98 }}} 133 99 134 In the above example, there is the question of what kind we should assign to 135 {{{a}}} in {{{Ok}}}. Currently it would be inferred to be {{{*}}}. That inference engine 136 would need to be improved to include inference of other kinds. 137 138 GADT constructors must only accept arguments of kind {{{*}}} (as per the 139 restrictions on (>) described below), but may also collect 140 constraints for the kind inference system. 100 In the above example, there is the question of what kind we should assign to {{{a}}} in {{{Ok}}}. Currently it would be inferred to be {{{*}}}. That inference engine would need to be improved to include inference of other kinds. 101 102 GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (>) described below), but may also collect constraints for the kind inference system. 141 103 142 104 == Interaction with normal functions == 143 105 144 Functions cannot have arguments of a non * kind. So the following would be 145 disallowed: 106 Functions cannot have arguments of a non * kind. So the following would be disallowed: 146 107 147 108 {{{ … … 163 124 }}} 164 125 165 In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind 166 {{{*}}}. 126 In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}. 167 127 168 128 === Ambiguous cases === 169 129 170 TODO: are there real ambiguous cases? _Assuming_ data types have their kind 171 signatures inferred before functions are type checked and must be monomorphic in 172 their kinds, I don't see how there could be unless a variable is totally 173 unconstrained (i.e. not mentioned) 130 TODO: are there real ambiguous cases? _Assuming_ data types have their kind signatures inferred before functions are type checked and must be monomorphic in their kinds, I don't see how there could be unless a variable is totally unconstrained (i.e. not mentioned) 174 131 175 132 {{{ … … 177 134 }}} 178 135 179 However this is accepted (6.8.3), although ghci drops the 'a'. Even if it was 180 used in a scoped setting (TODO example of where that makes sense without a type 181 class grounding it), the moment it is used it'll get a kind constraint. Do PolymorphicKinds break this assumption? 136 However this is accepted (6.8.3), although ghci drops the 'a'. Even if it was used in a scoped setting (TODO example of where that makes sense without a type class grounding it), the moment it is used it'll get a kind constraint. Do PolymorphicKinds break this assumption? 182 137 183 138 184 139 === Interaction with Type Classes === 185 140 186 Type classes are currently indexed by variables with a fixed kind. Type classes could now be indexed by 187 variables with nonvalue kinds. E.g. 141 Type classes are currently indexed by variables with a fixed kind. Type classes could now be indexed by variables with nonvalue kinds. E.g. 188 142 189 143 {{{ … … 200 154 }}} 201 155 202 By default declaration arguments are inferred to be of kind {{{*}}} if there is 203 nothing in the class declaration (member functions or explicit kind signature) 204 to change this. This seems sensible for backwardcompatibility. 156 By default declaration arguments are inferred to be of kind {{{*}}} if there is nothing in the class declaration (member functions or explicit kind signature) to change this. This seems sensible for backwardcompatibility. 205 157 206 158 == Interaction with Type Synonym Families == … … 215 167 == Polymorphic kinds == 216 168 217 Also see PolymorphicKinds 218 219 Data kinds could also be parameterised by kinds in the same way that data types 220 can be parameterised by types. This will require ''polymorphic kinds'', see below: 169 Also see PolymorphicKinds which this would build upon... 170 171 Data kinds could also be parameterised by kinds in the same way that data types can be parameterised by types. This will require ''polymorphic kinds'', see below: 221 172 222 173 {{{ … … 232 183 == A detour of Sorts == 233 184 234 GHC currently allowtype hackery is the ability to specify simple kind 235 signatures. By allowing declaration of other kinds, and parameterisation of 236 kinds, we will require kinds to have sorts. Initially we want to push 237 everything up one layer, so our language of sorts is generated by the sort that 238 classifies kinds {{{*}}}, or functions {{{sort > sort}}}. 185 GHC currently allowtype hackery is the ability to specify simple kind signatures. By allowing declaration of other kinds, and parameterisation of kinds, we will require kinds to have sorts. Initially we want to push everything up one layer, so our language of sorts is generated by the sort that classifies kinds {{{*}}}, or functions {{{sort > sort}}}. 239 186 240 187 This means we could allow explicit sortsignatures on kind arguments, e.g.: … … 259 206 == GADK Syntax == 260 207 261 It might also be nice to support GADK (Generalized Algebraic Data Kind) syntax 262 for declaring kinds, ala: 208 It might also be nice to support GADK (Generalized Algebraic Data Kind) syntax for declaring kinds, ala: 263 209 264 210 {{{ … … 276 222 }}} 277 223 278 At the moment I haven't thought about existential kinds or kindrefinement that 279 GADK syntax makes natural. Probably beyond the scope of this work, but should be 280 open for someone to add in the future. TODO think about motivating examples. 281 282 Note: I don't think it's worth having existential kinds without kindrefinement 283 as we don't have kindclasses, and so no user could ever make use of them. Kind 284 refinement does allow existential kinds to make sense however (or at least be 285 usable). The question then is when does kindrefinement come into play  286 pattern matches. TODO generate some examples to motivate this. 224 At the moment I haven't thought about existential kinds or kindrefinement that GADK syntax makes natural. Probably beyond the scope of this work, but should be open for someone to add in the future. TODO think about motivating examples. 225 226 Note: I don't think it's worth having existential kinds without kindrefinement as we don't have kindclasses, and so no user could ever make use of them. Kind refinement does allow existential kinds to make sense however (or at least be usable). The question then is when does kindrefinement come into play  pattern matches. TODO generate some examples to motivate this. 287 227 288 228 … … 291 231 With bits stolen from IntermediateTypes 292 232 293 There are already 2 sorts, {{{TY}}} and {{{CO}}}, for kinds that classify types, and for 294 coercions that classify evidence. 233 There are already 2 sorts, {{{TY}}} and {{{CO}}}, for kinds that classify types, and for coercions that classify evidence. 295 234 296 235 Previously I've called sort {{{TY}}} {{{*}}}. … … 309 248 '''Option 1 : Just use {{{*}}} ''' 310 249 311 Since all these meanings are in different namespaces, they arn't ambiguous and 312 can be left asis. 250 Since all these meanings are in different namespaces, they arn't ambiguous and can be left asis. 313 251 314 252 ''Pros:'' … … 322 260 '''Option 2 : Pick new symbols''' 323 261 324 Explicit, new names. E.g. {{{*}}} for terms, {{{@}}} for kinds, {{{&}}} for sorts (insert 325 your own choices). 262 Explicit, new names. E.g. {{{*}}} for terms, {{{@}}} for kinds, {{{&}}} for sorts (insert your own choices). 326 263 327 264 ''Pros:'' … … 335 272 Omega style level names. So: {{{*}}} is a term, {{{*1}}} is a kind, {{{*2}}} is a sort etc. 336 273 337 Possibly with some form of aliases to make the common levels more memorable, 338 e.g. {{{*k}}} for kinds, {{{*s}}} for sorts. 274 Possibly with some form of aliases to make the common levels more memorable, e.g. {{{*k}}} for kinds, {{{*s}}} for sorts. 339 275 340 276 ''Pros:'' … … 345 281 * Possibly tricky to parse/lex 346 282 347 Of course, if we are going to worry about {{{*}}} at different levels, the same 348 could apply to other machinary that is applied at different levels (I'm looking 349 at you (>)). 283 Of course, if we are going to worry about {{{*}}} at different levels, the same could apply to other machinary that is applied at different levels (I'm looking at you (>)). 350 284 351 285 … … 354 288 With reference to: TypeNaming 355 289 356 Strictly, the new kinds that have been introduced using {{{data kind}}} syntax 357 inhabit a new namespace. Mostly it is unambiguous when you refer to a type and 358 when you refer to a kind. However there are some corner cases, particularly in 359 module import/export lists. 290 Strictly, the new kinds that have been introduced using {{{data kind}}} syntax inhabit a new namespace. Mostly it is unambiguous when you refer to a type and when you refer to a kind. However there are some corner cases, particularly in module import/export lists. 360 291 361 292 === Option 1 : Collapse Type and Kind namespace === … … 366 297 367 298 '''Cons:''' 368 * Inconsistent. It would allow the user to create {{{True}}} and {{{False}}} as 369 types, but not to be able to put them under kind {{{Bool}}}. (You'd need to name 370 your kind a {{{Bool'}}} or {{{Bool_k}}}) 299 * Inconsistent. It would allow the user to create {{{True}}} and {{{False}}} as types, but not to be able to put them under kind {{{Bool}}}. (You'd need to name your kind a {{{Bool'}}} or {{{Bool_k}}}) 371 300 372 301 === Option 2 : Fix ambiguities === … … 404 333 TODO: I'm not so sure about the motivation of this anymore... 405 334 406 However any datalevel instantiations of the {{{k}}} in {{{List k}}} must be 407 monomorphic. E.g. Lists parameterised by the types of their elements: 335 However any datalevel instantiations of the {{{k}}} in {{{List k}}} must be monomorphic. E.g. Lists parameterised by the types of their elements: 408 336 409 337 {{{