Changes between Version 2 and Version 3 of GhcKinds/KindsWithoutData


Ignore:
Timestamp:
Jun 25, 2012 10:50:22 AM (22 months 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 ...`