Changes between Version 3 and Version 4 of KindSystem


Ignore:
Timestamp:
Oct 16, 2008 3:11:42 PM (6 years ago)
Author:
TristanAllwood
Comment:

More on autolifting

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v3 v4  
    313313== Auto Promotion of Types to Kinds == 
    314314 
    315 TODO 
     315Many 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. 
     316 
     317There are some other issues to be wary of (care of Simon PJ): 
     318 
     319  * Auto lifting of: 
     320     
     321    {{{ 
     322    data Foo = Foo Int 
     323    }}} 
     324 
     325    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. 
     326 
     327  * Automatic lifting of GADTs / existentials and parametric types is tricky until we have a story for them. 
     328 
     329  * Automatic lifting of some non-data types could be problematic (what types parameterise the kind {{{Int}}} or {{{Double}}}?) 
     330 
     331  * 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. 
     332 
     333Syntactically however, there are some options for how to do this in cases when it is safe to do:  
     334 
     335'''Option 0: Always promote [when safe]''' 
     336 
     337E.g. writing 
     338 
     339{{{ 
     340data Foo = Bar | Baz 
     341}}} 
     342 
     343will impliclty create a kind {{{Foo}}} and types {{{Bar}}} and {{{Baz}}} 
     344 
     345 
     346'''Option 1: Steal the {{{deriving}}} syntax''' 
     347This has an advantage of allowing standalone deriving for those data types that are declared elsewhere but not with Kind equivalents 
     348 
     349{{{ 
     350#!text/x-haskell 
     351 
     352data Maybe a = Nothing | Just a 
     353  deriving (Kind) 
     354 
     355deriving instance (Kind Bool) 
     356}}} 
     357 
     358'''Option 2: Add an extra flag to the {{{data}}} keyword''' 
     359 
     360{{{ 
     361data and kind Maybe a = Nothing | Just a 
     362}}} 
     363 
     364This has the problems of verbosity and is hard to apply after the fact to an existing data type. 
     365 
    316366 
    317367== Unfiltered thoughts == 
     368 
     369TODO: clean up, delete or something 
    318370 
    319371{{{