Changes between Version 1 and Version 2 of KindSystem


Ignore:
Timestamp:
Oct 16, 2008 10:59:15 AM (6 years ago)
Author:
guest
Comment:

De latexing

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v1 v2  
    55== Rationale == 
    66 
    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 ;)) 
     7Haskell 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 
     9Note: 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 ;)) 
    1410 
    1511== Motivation == 
    1612 
    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: 
     13Consider 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: 
    2014 
    2115{{{ 
     
    3125There are many eugh moments in this code: 
    3226 
    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: 
    3729 
    3830      {{{ 
     
    4133      }}} 
    4234 
    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. 
    5038 
    5139* 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 
     46We propose to add new base kinds other than {{{*}}} using a simple notation.  The above example ''could'' become: 
    6847 
    6948{{{ 
     
    7958 
    8059 
    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}}}. 
    9063 
    9164== Declaration Syntax == 
     
    9366=== ADT syntax === 
    9467 
    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: 
     68The 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 
     70To destinguish kind declarations from data declarations we can either add a new form of ''kind'' declaration: 
    10171 
    10272{{{ 
     
    10777However this steals {{{kind}}} as syntax with the usual problems of breaking existing programs. 
    10878 
    109 Alternatively (preferably), we can add a modifier to data declarations to 
    110 indicate that we mean a kind declaration: 
     79Alternatively (preferably), we can add a modifier to data declarations to indicate that we mean a kind declaration: 
    11180 
    11281{{{ 
     
    11786== Interaction with GADTs == 
    11887 
    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. 
     88GADTs 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. 
    12389 
    12490{{{ 
     
    13298}}} 
    13399 
    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. 
     100In 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 
     102GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (->) described below), but may also collect constraints for the kind inference system. 
    141103 
    142104== Interaction with normal functions == 
    143105 
    144 Functions cannot have arguments of a non * kind.  So the following would be 
    145 disallowed: 
     106Functions cannot have arguments of a non * kind.  So the following would be disallowed: 
    146107 
    147108{{{ 
     
    163124}}} 
    164125 
    165 In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind 
    166 {{{*}}}. 
     126In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}. 
    167127 
    168128=== Ambiguous cases === 
    169129 
    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) 
     130TODO: 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) 
    174131 
    175132{{{ 
     
    177134}}} 
    178135 
    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? 
     136However 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? 
    182137 
    183138 
    184139=== Interaction with Type Classes === 
    185140 
    186 Type classes are currently indexed by variables with a fixed kind.  Type classes could now be indexed by 
    187 variables with non-value kinds.  E.g. 
     141Type classes are currently indexed by variables with a fixed kind.  Type classes could now be indexed by variables with non-value kinds.  E.g. 
    188142 
    189143{{{ 
     
    200154}}} 
    201155 
    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 backward-compatibility. 
     156By 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 backward-compatibility. 
    205157 
    206158== Interaction with Type Synonym Families == 
     
    215167== Polymorphic kinds == 
    216168 
    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: 
     169Also see PolymorphicKinds which this would build upon... 
     170 
     171Data 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: 
    221172 
    222173{{{ 
     
    232183== A detour of Sorts == 
    233184 
    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}}}. 
     185GHC 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}}}. 
    239186 
    240187This means we could allow explicit sort-signatures on kind arguments, e.g.: 
     
    259206== GADK Syntax == 
    260207 
    261 It might also be nice to support GADK (Generalized Algebraic Data Kind) syntax 
    262 for declaring kinds, ala: 
     208It might also be nice to support GADK (Generalized Algebraic Data Kind) syntax for declaring kinds, ala: 
    263209 
    264210{{{ 
     
    276222}}} 
    277223 
    278 At the moment I haven't thought about existential kinds or kind-refinement 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 kind-refinement 
    283 as we don't have kind-classes, 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 kind-refinement come into play - 
    286 pattern matches.  TODO generate some examples to motivate this. 
     224At the moment I haven't thought about existential kinds or kind-refinement 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 
     226Note: I don't think it's worth having existential kinds without kind-refinement as we don't have kind-classes, 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 kind-refinement come into play - pattern matches.  TODO generate some examples to motivate this. 
    287227 
    288228 
     
    291231With bits stolen from IntermediateTypes 
    292232 
    293 There are already 2 sorts, {{{TY}}} and {{{CO}}}, for kinds that classify types, and for 
    294 coercions that classify evidence.   
     233There are already 2 sorts, {{{TY}}} and {{{CO}}}, for kinds that classify types, and for coercions that classify evidence.   
    295234 
    296235Previously I've called sort {{{TY}}} {{{*}}}. 
     
    309248'''Option 1 : Just use {{{*}}} ''' 
    310249 
    311 Since all these meanings are in different namespaces, they arn't ambiguous and 
    312 can be left as-is. 
     250Since all these meanings are in different namespaces, they arn't ambiguous and can be left as-is. 
    313251 
    314252''Pros:'' 
     
    322260'''Option 2 : Pick new symbols''' 
    323261 
    324 Explicit, new names.  E.g. {{{*}}} for terms, {{{@}}} for kinds, {{{&}}} for sorts (insert 
    325 your own choices). 
     262Explicit, new names.  E.g. {{{*}}} for terms, {{{@}}} for kinds, {{{&}}} for sorts (insert your own choices). 
    326263 
    327264''Pros:'' 
     
    335272Omega style level names.  So: {{{*}}} is a term, {{{*1}}} is a kind, {{{*2}}} is a sort etc. 
    336273 
    337 Possibly with some form of aliases to make the common levels more memorable, 
    338 e.g.  {{{*k}}} for kinds, {{{*s}}} for sorts. 
     274Possibly with some form of aliases to make the common levels more memorable, e.g.  {{{*k}}} for kinds, {{{*s}}} for sorts. 
    339275 
    340276''Pros:'' 
     
    345281* Possibly tricky to parse/lex 
    346282 
    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 (->)). 
     283Of 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 (->)). 
    350284 
    351285 
     
    354288With reference to: TypeNaming 
    355289 
    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. 
     290Strictly, 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. 
    360291 
    361292=== Option 1 : Collapse Type and Kind namespace === 
     
    366297 
    367298'''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}}}) 
    371300 
    372301=== Option 2 : Fix ambiguities === 
     
    404333TODO: I'm not so sure about the motivation of this anymore... 
    405334 
    406 However any data-level instantiations of the {{{k}}} in {{{List k}}} must be 
    407 monomorphic.  E.g. Lists parameterised by the types of their elements: 
     335However any data-level instantiations of the {{{k}}} in {{{List k}}} must be monomorphic.  E.g. Lists parameterised by the types of their elements: 
    408336 
    409337{{{