Changes between Version 17 and Version 18 of GhcKinds/KindsWithoutData


Ignore:
Timestamp:
Jan 3, 2016 1:21:43 PM (4 years ago)
Author:
jstolarek
Comment:

Rewrite the page to include proposal of open data kinds

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindsWithoutData

    v17 v18  
    1 = Defining kinds without an associated datatype = 
     1= Defining kinds without an associated datatype =
    22
    3 This ticket to track this request is #6024.
     3This page tracks feature requests for declaring closed data kinds without
     4associated data types (#6024) and declaring open data kinds that can be freely
     5extended after they are declared (#11080).  What comes below is a design
     6proposal that is not yet implemented (as of Jan 2015).  Main person responsible
     7for working on the implementation is Jan Stolarek (JS).
    48
    5 When using `-XDataKinds` GHC automatically promotes every datatype to a kind, and its constructors to
    6 types. This forces us to declare a datatype for every kind. However, sometimes we are not interested
    7 in the datatype at all, only on the kind. Consider the following data kind that defines a small
    8 universe for generic programming:
     9== Motivation for closed data kinds (#6024) ==
    910
    10 {{{
    11 data Universe star = Sum  Universe Universe
    12                    | Prod Universe Universe
     11When using `-XDataKinds` GHC automatically promotes every datatype to a kind,
     12and its constructors to types. This forces us to declare a datatype for every
     13kind.  However, sometimes we are not interested in the datatype at all, only on
     14the kind.  Consider the following data kind that defines a small universe for
     15generic programming:
     16
     17{{{#!hs
     18data Universe star = Sum  (Universe star) (Universe star)
     19                   | Prod (Universe star) (Universe star)
    1320                   | K star
    1421}}}
     
    1623This universe comes with an associated interpretation:
    1724
    18 {{{
     25{{{#!hs
    1926data Interpretation :: Universe * -> * where
    2027  L    :: Interpretation a -> Interpretation (Sum a b)
     
    2633In this case, having to declare a datatype for `Universe` has two disadvantages:
    2734
    28   1. We cannot use kinds (such as `*`) while defining a datatype, so we are forced to make `Universe` a parametrised datatype, and later always instantiate this parameter to `*` (like in the kind of `Interpretation`).
     35  1. We cannot use kinds (such as `*`) while defining a datatype, so we are
     36     forced to make `Universe` a parametrised datatype, and later always
     37     instantiate this parameter to `*` (like in the kind of `Interpretation`).
     38     '''Note''': this is no longer the case - see below.
    2939
    30   2. We lose constructor name space, because the datatype constructor names will be taken, even though we will never use them. So `Prod` and `K` cannot be used as constructors of `Interpretation` as above, because those are also constructors of `Universe`.
     40  2. We lose constructor name space, because the datatype constructor names will
     41     be taken, even though we will never use them to construct terms.  So `Prod`
     42     and `K` cannot be used as constructors of `Interpretation` as above,
     43     because those are also constructors of `Universe`.
    3144
    32 '''Solution''': let users define things like
    33 {{{
     45== Motivation for open data kinds (#11080) ==
     46
     47Users might want to create type-level symbols for the purpose of indexing types.
     48In the past one way of doing this was by using `-XEmptyDataDecls`.  But symbols
     49created in this way were always placed in `*` and that does not allow to use
     50kinds to limit what types are admitted as indices.  `-XDataKinds` allows to
     51create symbols that are assigned a kind other than `*` but these kinds are
     52closed and adding new symbols is not possible. Thus:
     53
     54  3. We want a way of defining open kinds that can be later extended with new
     55     inhabitants.
     56
     57= Solution =
     58
     59I (JS) propose that the mechanism for declaring closed and open data kinds
     60becomes part of `-XDataKinds`.  The proposal is backwards compatible.
     61
     62== Closed kinds ==
     63
     64Starting with GHC 8.0 users can use `-XTypeInType` extension to write:
     65
     66{{{#!hs
     67data Universe = Sum  Universe Universe
     68              | Prod Universe Universe
     69              | K (*)
     70}}}
     71
     72This addresses disadvantage (1) but still leaves us with disadvantage (2).  So
     73the idea behind #6024 is to let users define things like:
     74
     75{{{#!hs
     76-- closed kind using H98 syntax
    3477data kind Universe = Sum  Universe Universe
    3578                   | Prod Universe Universe
    36                    | K *
     79                   | K (*)
     80
     81-- closed kind using GADTs syntax
     82data kind Universe where
     83  Sum  :: Universe -> Universe -> Universe
     84  Prod :: Universe -> Universe -> Universe
     85  K    :: *                    -> Universe
    3786}}}
    38 By using `data kind`, we tell GHC that we are only interested in the `Universe` kind, and not the datatype.
    39 Consequently, `Sum`, `Prod`, and `K` will be types only, and not constructors.
    4087
    41 Also,
    42 {{{
    43 data type D = C
     88By using `data kind`, we tell GHC that we are only interested in the `Universe`
     89kind, and not the datatype.  Consequently, `Sum`, `Prod`, and `K` will be valid
     90only in types only, and not in terms.
     91
     92== Open kinds ==
     93
     94Open data kinds would be declared using following syntax:
     95
     96{{{#!hs
     97-- open kind
     98data kind open Universe
     99data kind member Sum  :: Universe -> Universe -> Universe
     100data kind member Prod :: Universe -> Universe -> Universe
     101data kind member K    :: *                    -> Universe
    44102}}}
    45 defines a datatype `D` which is not promoted to a kind, and its constructor `C` is
    46 not promoted to a type.
    47103
    48 == Caveats ==
     104Note that open kinds can be parametrized just like closed kinds:
    49105
     106{{{#!hs
     107data kind open Dimension :: *
     108data kind member Length :: Dimension
    50109
    51 === Star in Star ===
    52 If, in the future, we make `* :: *`, we will no longer have separation of
    53 types and kinds, so we won't be able to make such fine distinctions.
     110data kind open Unit :: Dimension -> *
     111data kind member Meter :: Unit 'Length
     112data kind member Foot  :: Unit 'Length
     113}}}
    54114
     115= Caveats =
    55116
    56 === Recursive Groups ===
     117== Kind and Type Namespaces ==
    57118
     119Currently GHC has separate namespaces for types and data constructors.  We have
     120a simple rule: all data constructors go into data namespace.  With `-XDataKinds`
     121promoted data constructors still live in data constructor namespace and there is
     122a hack in the renamer: when renaming types it first looks for a symbol in type
     123namespace and if that fails then it searches for the symbol in the data
     124namespace.
    58125
    59 === Kind and Type Namespaces ===
    60 As kinds and types currently share a namespace, `data kind` and
    61 `data type` declarations '''in the same module''' can still
    62 conflict.  However, if they are in separate modules, this can be controlled by
    63 use of the module system.
     126Assume we have:
    64127
     128{{{#!hs
     129data kind Foo = MkFoo
     130}}}
    65131
    66 == Alternative Solutions ==
     132In order to resolve disadvantage (2), ie. not pollute data constructor namespace
     133with `MkFoo`, we would have to put `MkFoo` in the type namespace.  This means
     134that our simple rule "data constructors go into data namespace" would have to be
     135broken.
     136[https://mail.haskell.org/pipermail/ghc-devs/2015-December/010812.html Richard Eisenberg argues]
     137that this is bad and in the case of above declaration
     138`MkFoo` should go into data namespace.  But that does not solve disadvantage (2)
     139and thus misses the point of #6024 (given that disadvantage (1) is already
     140solved by `-XTypeInType`).  Richard also argues that members of an open data
     141kind should also be placed in data namespace.  Putting `MkFoo` into data
     142namespace will also allow us to have quite good error messages from the
     143typechecker, rather than cryptic error messages from the renamer about things
     144being out of scope.
    67145
    68 Add
    69 {{{
    70 data Star
     146== Non-promotable data types? ==
     147
     148Let's assume for a moment that we decide to place kind-only constructors in the
     149type namespace (ie. not follow Richard's proposal).  Consider again the example
     150of `Universe` kind and `Interpretation` data type.  Enabling `-XTypeInType`
     151makes GADTs promotable.  This means that data constructors `K` and `Prod` if
     152`Interpretation` data type could be validly used in types.  But this would lead
     153to name collission with `K` and `Prod` constructors of `Universe` kind.  There
     154would be no way of disambiguating whether `K` refers to constructor of
     155`Universe` or promoted constructor of `Interpretation`.  We don't want to end up
     156in a situation where some of the data constructors can be promoted (`L`, `R`)
     157and some can't (`K`, `Prod`).  So we would need to make `Interpretation` data
     158type unpromotable.  But detecting that seems Real Hard.
     159
     160== Recursive Groups ==
     161
     162We need to be careful about recursive groups.  For example, this is valid:
     163
     164{{{#!hs
     165data S = S T
     166data T = T S
    71167}}}
    72 in `GHC.Exts` such that the promotion of datatype `Star` is the kind `*`. As a
    73 datatype, `Star` is just an empty datatype.
    74168
    75 ''Advantages'': very easy, backwards compatible
     169but this is not:
    76170
    77 ''Disadvantages'': somewhat verbose, doesn't fix (2)
     171{{{#!hs
     172data kind S = S T
     173data T = T S
     174}}}
    78175
     176== Future-proofing the design ==
    79177
    80 == Alternative Notations ==
     178GHC is growing more and more type level symbols.  These symbols vary in their
     179properties like generativity, injectivity, matchability or being open/closed -
     180see [ticket:9840#comment:6] for an overview.
     181Here we propose adding yet another way of defining symbols.  Can we introduce
     182more order into world of type-level symbols?  Can we have some unifying syntax?
     183Can we anticipate what kind of symbols we might want to have in the future?
     184
     185= Alternative Notations =
    81186
    82187 * Use `data only` instead of `data type`.
    83  * Use `'data` instead of `data kind`, suggested by Gabor Greif.
    84  * Use `type data` instead of `data kind`, suggested (preferred) by Gabor Greif.
    85 
    86 In both cases, we felt that using `type` and `kind` as the modifiers to the `data` declaration better reflect what's being defined.
     188 * Use `'data` instead of `data kind`
     189 * Use `type data` instead of `data kind`
     190 * Use `data constructor` instead of `data kind member`
     191 * Use `data extension Unit where { Meter :: Unit;  Foot :: Unit }` instead of
     192   `data kind member`