Changes between Version 12 and Version 13 of GhcKinds/KindsWithoutData


Ignore:
Timestamp:
Sep 8, 2013 11:26:37 PM (20 months 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.