Changes between Version 10 and Version 11 of GhcKinds/KindsWithoutData


Ignore:
Timestamp:
Dec 7, 2012 9:50:43 AM (3 years 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.