Changes between Version 2 and Version 3 of GhcKinds/KindsWithoutData


Ignore:
Timestamp:
Jun 25, 2012 10:50:22 AM (3 years ago)
Author:
dreixel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindsWithoutData

    v2 v3  
    1 Pedro will write this. Notes:
     1= Defining kinds without an associated datatype =
     2
     3When using `-XDataKinds` GHC automatically promotes every datatype to a kind, and its constructors to
     4types. This forces us to declare a datatype for every kind. However, sometimes we are not interested
     5in the datatype at all, only on the kind. Consider the following data kind that defines a small
     6universe for generic programming:
     7
     8{{{
     9data Universe star = Sum  Universe Universe
     10                   | Prod Universe Universe
     11                   | K star
     12}}}
     13
     14This universe comes with an associated interpretation:
     15
     16{{{
     17data Interpretation :: Universe * -> * where
     18  L    :: Interpretation a -> Interpretation (Sum a b)
     19  R    :: Interpretation b -> Interpretation (Sum a b)
     20  Prod :: Interpretation a -> Interpretation b -> Interpretation (Prod a b)
     21  K    :: a -> Interpretation (K a)
     22}}}
     23
     24In this case, having to declare a datatype for `Universe` has two disadvantages:
     25
     26 * We lose constructor name space, because the datatype constructor names will be taken, even though
     27   we will never use them. So `Prod` and `K` cannot be used as constructors of `Interpretation` as above,
     28   because those are also constructors of `Universe`.
     29
     30 * We cannot use kinds (such as `*`) while defining a datatype, so we are forced to make `Universe` a
     31   parametrised datatype, and later always instantiate this parameter to `*` (like in the kind of
     32   `Interpretation`).
     33
     34'''Proposal:''' allow defining kinds directly, as in the following example:
     35
     36{{{
     37data kind Universe = Sum  Universe Universe
     38                   | Prod Universe Universe
     39                   | K *
     40}}}
     41
     42By using `data kind`, we tell GHC that we are only interested in the `Universe` kind, and not the datatype.
     43Consequently, `Sum`, `Prod`, and `K` will be types only, and not constructors.
     44
     45= Notes =
    246
    347 * `data kind K ...`