Changes between Version 12 and Version 13 of GhcKinds/KindsWithoutData


Ignore:
Timestamp:
Sep 8, 2013 11:26:37 PM (2 years ago)
Author:
elliottt
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindsWithoutData

    v12 v13  
    2828  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`.
    2929
    30 '''Solution 1''': add
    31 {{{
    32 data Star
    33 }}}
    34 in `GHC.Exts` such that the promotion of datatype `Star` is the kind `*`. As a
    35 datatype, `Star` is just an empty datatype.
    36 
    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
     30'''Solution''': let users define things like
    4331{{{
    4432data kind Universe = Sum  Universe Universe
     
    5139Also,
    5240{{{
    53 data only (i :: D) where C :: I ('C Int)
     41data type (i :: D) where C :: I ('C Int)
    5442}}}
    5543defines a datatype `D` which is not promoted to a kind, and its constructors
     
    6755Currently 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.
    6856
    69 == Thoughts (Gabor Greif) ==
     57== Alternative Solutions ==
    7058
    71 I'd prefer writing
     59Add
    7260{{{
    73 'data Universe = Sum  Universe Universe
    74                | Prod Universe Universe
    75                | K *
     61data Star
    7662}}}
    77 over `data kind` to only obtain the `Universe` kind and `Sum`, `Prod` and `K` types. This would extrapolate the `'Universe` notation for grabbing the kind when a type also exists with the same name.
    78 I am also a bit less enthusiastic with `data only`. Why not `data data`? (Still does not feel right.)
     63in `GHC.Exts` such that the promotion of datatype `Star` is the kind `*`. As a
     64datatype, `Star` is just an empty datatype.
     65
     66''Advantages'': very easy, backwards compatible
     67
     68''Disadvantages'': somewhat verbose, doesn't fix (2)
     69
     70
     71== Alternative Notations ==
     72
     73 * Use `data only` instead of `data type`.
     74 * Use `'data` instead of `data kind`, suggested by Gabor Greif.
     75
     76In both cases, we felt that using `type` and `kind` as the modifiers to the `data` declaration better reflect what's being defined.