Changes between Version 10 and Version 11 of GhcKinds/KindsWithoutData


Ignore:
Timestamp:
Dec 7, 2012 9:50:43 AM (17 months ago)
Author:
dreixel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindsWithoutData

    v10 v11  
    2424In this case, having to declare a datatype for `Universe` has two disadvantages: 
    2525 
    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`. 
     26  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`). 
    2927 
    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`). 
     28  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`. 
    3329 
    34 '''Proposal:''' allow defining kinds directly, as in the following example: 
     30'''Solution 1''': add 
     31{{{ 
     32data Star 
     33}}} 
     34in `GHC.Exts` such that the promotion of datatype `Star` is the kind `*`. As a 
     35datatype, `Star` is just an empty datatype. 
    3536 
     37''Advantages'': very easy, backwards compatible 
     38 
     39''Disadvantages'': somewhat verbose, doesn't fix (2) 
     40 
     41 
     42'''Solution 2''': let users define things like 
    3643{{{ 
    3744data kind Universe = Sum  Universe Universe 
     
    3946                   | K * 
    4047}}} 
     48By using `data kind`, we tell GHC that we are only interested in the `Universe` kind, and not the datatype. 
     49Consequently, `Sum`, `Prod`, and `K` will be types only, and not constructors. 
    4150 
    42 By using `data kind`, we tell GHC that we are only interested in the `Universe` kind, and not the datatype. 
    43 Consequently, `Sum`, `Prod`, and `K` will be types only, and not constructors. Note however that this would 
    44 imply being able to parse kinds (`*`, at the very least) on the right-hand side of data kind declarations. 
    45 To avoid this, we propose instead using a kind `Type` (or `Star`), defined in `GHC.Exts`, that acts as a 
    46 synonym of `*`. 
     51Also, 
     52{{{ 
     53data only (i :: D) where C :: I ('C Int) 
     54}}} 
     55defines a datatype `D` which is not promoted to a kind, and its constructors 
     56are not promoted to types. We would then also have ‘type only T = Int -> Int`. 
    4757 
    48 This ticket to track this request is #6024. 
     58''Advantages'': solves (1) and (2) 
    4959 
    50 One potential problem is that is we ever get `* :: *` then this will no longer be possible... 
     60''Disadvantages'': 
    5161 
     621. If, in the future, we make `* :: *`, we will no longer have separation of 
     63types and kinds, so things like `D`/`I` above will become impossible. 
    5264 
    53 = Defining datatypes without an associated kind = 
     652. Requires changing the parser 
    5466 
    55 By extension, we might want to define a datatype that will never be promoted, even with `-XDataKinds`. 
    56 For that we propose the syntax `data type D ...`. 
     67Currently we are planning to implement the second solution. If we do get `* :: *` other things will break due to name clashes, so that shouldn't prevent us from going ahead now. This ticket to track this request is #6024.