Changes between Version 19 and Version 20 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 2:38:11 PM (7 years ago)
Author:
TristanAllwood
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v19 v20  
    176176 
    177177''Pros:'' 
    178 * Simple 
    179 * Follows behaviour of type classes, type functions and data type functions. 
     178  * Simple 
     179  * Follows behaviour of type classes, type functions and data type functions. 
    180180 
    181181''Cons:'' 
    182 * 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}}}) 
     182  * 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}}}) 
    183183 
    184184'''Option 2 : Fix ambiguities''' 
    185185 
    186186''Pros:'' 
    187 * As more extensions are put into the language, it'll have to happen sooner or later 
     187  * As more extensions are put into the language, it'll have to happen sooner or later 
    188188 
    189189''Cons:'' 
    190 * Will involve creating a whole new namespace 
    191 * Several corner cases 
    192  
    193  
    194  
     190  * Will involve creating a whole new namespace 
     191  * Several corner cases 
     192 
     193== Auto Promotion of Types to Kinds == 
     194 
     195Many simple data declarations it would be convinient to also have at the type level.  Assuming we resolve the TypeNaming and ambiguity issues above, we could support automatically deriving the data kind based on the data. 
     196 
     197There are some other issues to be wary of (care of Simon PJ): 
     198 
     199  * Auto lifting of: 
     200     
     201    {{{ 
     202    data Foo = Foo Int 
     203    }}} 
     204 
     205    Automated lifting this would try and create a kind {{{Foo}}} with an associated type {{{Foo}}}.  But we've just declared a type {{{Foo}}} in the data declaration. 
     206 
     207  * Automatic lifting of GADTs / existentials and parametric types is tricky until we have a story for them. 
     208 
     209  * Automatic lifting of some non-data types could be problematic (what types parameterise the kind {{{Int}}} or {{{Double}}}?) 
     210 
     211  * We have no plan to auto-lift term *functions* to become type functions.  So it seems odd to auto-lift the type declarations which are, after all, the easy bit. 
     212 
     213Syntactically however, there are some options for how to do this in cases when it is safe to do:  
     214 
     215'''Option 0: Always promote [when safe]''' 
     216 
     217E.g. writing 
     218 
     219{{{ 
     220data Foo = Bar | Baz 
     221}}} 
     222 
     223will impliclty create a kind {{{Foo}}} and types {{{Bar}}} and {{{Baz}}} 
     224 
     225 
     226'''Option 1: Steal the {{{deriving}}} syntax''' 
     227This has an advantage of allowing standalone deriving for those data types that are declared elsewhere but not with Kind equivalents 
     228 
     229{{{ 
     230#!text/x-haskell 
     231 
     232data Maybe a = Nothing | Just a 
     233  deriving (Kind) 
     234 
     235deriving instance (Kind Bool) 
     236}}} 
     237 
     238'''Option 2: Add an extra flag to the {{{data}}} keyword''' 
     239 
     240{{{ 
     241data and kind Maybe a = Nothing | Just a 
     242}}} 
     243 
     244This has the problems of verbosity and is hard to apply after the fact to an existing data type. 
    195245 
    196246----------------------------------- 
     
    202252 
    203253 
    204 == Syntax == 
     254=== Syntax === 
    205255 
    206256We need a syntax for sorts as well as kinds: 
     
    212262  sort ::= ** | sort -> sort 
    213263}}} 
     264 
    214265Choices 
    215266 * What to use for the sort that classifies `*`, `*->*` etc?   
     
    225276 * Impredicative kinds?  No! 
    226277 
    227 == Examples ==  
     278=== Examples === 
    228279 
    229280{{{ 
     
    261312 
    262313 
    263  
    264 == A detour of Sorts == 
     314=== Sort Signatures === 
    265315 
    266316GHC currently allows users to specify simple kind signatures.  By allowing declaration of other kinds, and parameterisation of kinds, we will require kinds to have sorts.  Initially we may want to push everything up one layer, so our language of sorts is generated by the sort that classifies kinds {{{*}}}, or functions {{{sort -> sort}}}. 
     
    268318This means we could allow explicit sort-signatures on kind arguments, e.g.: 
    269319 
    270 TODO think really hard about this example. 
    271320 
    272321{{{ 
     
    284333}}}  
    285334 
    286  
    287  
    288 == Implementation things == 
    289  
    290 With bits stolen from IntermediateTypes 
    291  
    292 There are already 2 sorts, {{{TY}}} and {{{CO}}}, for kinds that classify types, and for coercions that classify evidence.   
    293  
    294 Previously I've called sort {{{TY}}} {{{*}}}. 
    295  
    296 == Syntax == 
    297  
    298 === Seeing Stars === 
    299  
    300 {{{*}}} now has many overloaded meanings in this document: 
    301  
    302 * As a term, it is an infix function 
    303 * It has no meaning as a type 
    304 * As a kind it is the kind of all lifted types 
    305 * As a sort it is the sort of all kinds that parameterise types 
    306  
    307 '''Option 1 : Just use {{{*}}} ''' 
    308  
    309 Since all these meanings are in different namespaces, they arn't ambiguous and can be left as-is. 
    310  
    311 ''Pros:'' 
    312 * Short, neat and syntactically light 
    313 * Simple to lex 
    314  
    315 ''Cons:'' 
    316 * Probably confusing without familiarity to the namespaces 
    317 * Not future compatible if we were to support arbitary stratification 
    318  
    319 '''Option 2 : Pick new symbols''' 
    320  
    321 Explicit, new names.  E.g. {{{*}}} for terms, {{{@}}} for kinds, {{{&}}} for sorts (insert your own choices). 
    322  
    323 ''Pros:'' 
    324 * Hopefully simpler to lex 
    325  
    326 ''Cons:'' 
    327 * Even more symbols to learn 
    328  
    329 '''Option 3 : Levelled Stars''' 
    330  
    331 Omega style level names.  So: {{{*}}} is a term, {{{*1}}} is a kind, {{{*2}}} is a sort etc. 
    332  
    333 Possibly with some form of aliases to make the common levels more memorable, e.g.  {{{*k}}} for kinds, {{{*s}}} for sorts. 
    334  
    335 ''Pros:'' 
    336 * Future compatible for arbitary stratification 
    337 * Aliases are mnemonic 
    338  
    339 ''Cons:'' 
    340 * Possibly tricky to parse/lex 
    341  
    342 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 (->)). 
    343  
    344  
    345  
    346 == Auto Promotion of Types to Kinds == 
    347  
    348 Many simple data declarations it would be convinient to also have at the type level.  Assuming we resolve the TypeNaming and ambiguity issues above, we could support automatically deriving the data kind based on the data. 
    349  
    350 There are some other issues to be wary of (care of Simon PJ): 
    351  
    352   * Auto lifting of: 
    353      
    354     {{{ 
    355     data Foo = Foo Int 
    356     }}} 
    357  
    358     Automated lifting this would try and create a kind {{{Foo}}} with an associated type {{{Foo}}}.  But we've just declared a type {{{Foo}}} in the data declaration. 
    359  
    360   * Automatic lifting of GADTs / existentials and parametric types is tricky until we have a story for them. 
    361  
    362   * Automatic lifting of some non-data types could be problematic (what types parameterise the kind {{{Int}}} or {{{Double}}}?) 
    363  
    364   * We have no plan to auto-lift term *functions* to become type functions.  So it seems odd to auto-lift the type declarations which are, after all, the easy bit. 
    365  
    366 Syntactically however, there are some options for how to do this in cases when it is safe to do:  
    367  
    368 '''Option 0: Always promote [when safe]''' 
    369  
    370 E.g. writing 
    371  
    372 {{{ 
    373 data Foo = Bar | Baz 
    374 }}} 
    375  
    376 will impliclty create a kind {{{Foo}}} and types {{{Bar}}} and {{{Baz}}} 
    377  
    378  
    379 '''Option 1: Steal the {{{deriving}}} syntax''' 
    380 This has an advantage of allowing standalone deriving for those data types that are declared elsewhere but not with Kind equivalents 
    381  
    382 {{{ 
    383 #!text/x-haskell 
    384  
    385 data Maybe a = Nothing | Just a 
    386   deriving (Kind) 
    387  
    388 deriving instance (Kind Bool) 
    389 }}} 
    390  
    391 '''Option 2: Add an extra flag to the {{{data}}} keyword''' 
    392  
    393 {{{ 
    394 data and kind Maybe a = Nothing | Just a 
    395 }}} 
    396  
    397 This has the problems of verbosity and is hard to apply after the fact to an existing data type. 
    398  
    399  
    400 == Kind Synonyms == 
    401  
    402 Simple type synonyms have a natural analogy at the kind level that could be a useful feature to provde.  Depending on whether we keep the kind and type namespaces separate (above) we could just abuse the current {{{type Foo = Either Baz Bang}}} syntax to also allow creating {{{kind synonyms}}}, or if we need to invent some new syntax.  {{{kind Foo = Either Baz Bang}}} would seen natural, or perhaps more safely {{{type kind Foo = Either Baz Bang}}}. 
     335=== Kind Synonyms === 
     336 
     337Simple type synonyms have a natural analogy at the kind level that could be a useful feature to provde once we have parameterizable kinds.  Depending on whether we keep the kind and type namespaces separate (above) we could just abuse the current {{{type Foo = Either Baz Bang}}} syntax to also allow creating {{{kind synonyms}}}, or if we need to invent some new syntax.  {{{kind Foo = Either Baz Bang}}} would seen natural, or perhaps more safely {{{type kind Foo = Either Baz Bang}}}. 
    403338 
    404339{{{newkind}}} doesn't make sense to add as there is no associated semantics to gain at the type level that {{{data kind}}} doesn't already provide. 
    405  
    406 == Unfiltered thoughts == 
    407  
    408 TODO: clean up, delete or something 
    409  
    410 {{{ 
    411 data kind List k = Nil | Cons k (List k) 
    412 }}} 
    413  
    414 This lets us represent a list of types of any kind, and it seems natural to write a function 
    415 to give us it's length: 
    416  
    417 {{{ 
    418 type family ListLength :: List k -> Nat 
    419 type instance ListLength Nil = Zero 
    420 type instance ListLength (Cons _ rest) = Succ (ListLength rest) 
    421 }}} 
    422  
    423 So here we want to be able to index type families by a polykind. 
    424  
    425 TODO: I'm not so sure about the motivation of this anymore... 
    426  
    427 However any data-level instantiations of the {{{k}}} in {{{List k}}} must be monomorphic.  E.g. Lists parameterised by the types of their elements: 
    428  
    429 {{{ 
    430 data SafeList :: (List *) -> * where 
    431   Nil  :: SafeList Nil 
    432   Cons :: a -> SafeList a rest -> SafeList (Cons a rest) 
    433  
    434 safeHead :: SafeList (Cons a rest) -> a 
    435 safeHead (Cons a _) = a 
    436 }}} 
    437  
    438 Or the value reflection of a bit list: 
    439  
    440 {{{ 
    441 data StaticBitString :: List Bool -> * where 
    442   BSTrue :: StaticBitString rest -> StaticBitString (Cons True rest) 
    443   BSFalse :: StaticBitString rest -> StaticBitString (Cons False rest) 
    444 }}} 
    445  
    446 Why not: 
    447  
    448 {{{ 
    449 data Blah :: forall_kind k . List k -> Nat (Length k) -> * 
    450   WitnessEmpty :: Blah Nil Zero 
    451   WitnessSucc  :: Blah rest n -> Blah (Cons ? rest) (Succ n) 
    452 }}} 
    453  
    454 What is the ? above? 
    455