Changes between Version 3 and Version 4 of KindSystem

Oct 16, 2008 3:11:42 PM (9 years ago)

More on autolifting


  • KindSystem

    v3 v4  
    313313== Auto Promotion of Types to Kinds ==
    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.
     317There are some other issues to be wary of (care of Simon PJ):
     319  * Auto lifting of:
     321    {{{
     322    data Foo = Foo Int
     323    }}}
     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.
     327  * Automatic lifting of GADTs / existentials and parametric types is tricky until we have a story for them.
     329  * Automatic lifting of some non-data types could be problematic (what types parameterise the kind {{{Int}}} or {{{Double}}}?)
     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.
     333Syntactically however, there are some options for how to do this in cases when it is safe to do:
     335'''Option 0: Always promote [when safe]'''
     337E.g. writing
     340data Foo = Bar | Baz
     343will impliclty create a kind {{{Foo}}} and types {{{Bar}}} and {{{Baz}}}
     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
     352data Maybe a = Nothing | Just a
     353  deriving (Kind)
     355deriving instance (Kind Bool)
     358'''Option 2: Add an extra flag to the {{{data}}} keyword'''
     361data and kind Maybe a = Nothing | Just a
     364This has the problems of verbosity and is hard to apply after the fact to an existing data type.
    317367== Unfiltered thoughts ==
     369TODO: clean up, delete or something