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