Changes between Version 13 and Version 14 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 8:37:50 AM (6 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v13 v14  
    177177Data kinds could also be parameterised by kinds in the same way that data types can be parameterised by types.  This will require ''polymorphic kinds'', see below: 
    178178 
    179 {{{ 
    180 data kind Maybe k = Nothing | Just k 
    181 }}} 
    182  
    183 So here, {{{Maybe}}} has ''sort'' {{{* -> *}}}, 
    184 {{{Nothing}}} has ''kind'' {{{forall k . Maybe k}}} and {{{Just}}} has ''kind'' 
    185 {{{forall k . k -> Maybe k}}}. 
     179 
     180== Syntax == 
     181 
     182We need a syntax for sorts as well as kinds: 
     183{{{ 
     184  kind variable ::= k, ... etc 
     185  kind ::= * | kind -> kind | forall k. kind | k 
     186 
     187  sort ::= ** | sort -> sort 
     188}}} 
     189Choices 
     190 * What to use for the sort that classifies `*`, `*->*` etc?   
     191   * `*2` (as in Omega; but *2 isn't a Haskell lexeme) 
     192   * `**` (using unary notation) 
     193   * `*s` (Tristan) 
     194   * `kind` (use a keyword) 
     195 
     196 * Do we have sort polymorphism?  No! 
     197 
     198== Examples ==  
     199 
     200{{{ 
     201data kind MaybeK k = NothingK | JustK k 
     202}}} 
     203 
     204So here we have 
     205{{{ 
     206  MaybeK   :: ** -> **                      -- Sort of MaybeK 
     207  NothingK :: forall k::**. MaybeK k        -- Kind of NothingK 
     208  JustK    :: forall k::**. k -> MaybeK k   -- Kind of JustK 
     209}}} 
     210 
     211It might also be nice to support GADK (Generalized Algebraic Data Kind) syntax for declaring kinds, ala: 
     212 
     213{{{ 
     214data kind MaybeK :: ** -> ** where 
     215  NothingK :: MaybeK k 
     216  JustK :: k -> MaybeK k 
     217}}} 
     218 
     219Again, note that {{{Maybe}}} above is decorated with a {{{sort}}} signature. 
     220 
     221or 
     222 
     223{{{ 
     224data kind MaybeK k where 
     225  NothingK :: MaybeK k 
     226  JustK :: k -> MaybeK k 
     227}}} 
     228 
     229However no GADTs or existentials at the kind level (yet).  TODO think about motivating examples. 
     230 
     231Note: I don't think it's worth having existential kinds without kind-refinement as we don't have kind-classes, and so no user could ever make use of them.  Kind refinement does allow existential kinds to make sense however (or at least be usable).  The question then is when does kind-refinement come into play - pattern matches.  TODO generate some examples to motivate this. 
    186232 
    187233 
     
    211257 
    212258== GADK Syntax == 
    213  
    214 It might also be nice to support GADK (Generalized Algebraic Data Kind) syntax for declaring kinds, ala: 
    215  
    216 {{{ 
    217 data kind Maybe :: * -> * where 
    218   Nothing :: Maybe k 
    219   Just :: k -> Maybe k 
    220 }}} 
    221  
    222 Again, note that {{{Maybe}}} above is decorated with a {{{sort}}} signature. 
    223  
    224 or 
    225  
    226 {{{ 
    227 data kind Maybe k where 
    228   Nothing :: Maybe k 
    229   Just :: k -> Maybe k 
    230 }}} 
    231  
    232 At the moment I haven't thought about existential kinds or kind-refinement that GADK syntax makes natural. Probably beyond the scope of this work, but should be open for someone to add in the future.  TODO think about motivating examples. 
    233  
    234 Note: I don't think it's worth having existential kinds without kind-refinement as we don't have kind-classes, and so no user could ever make use of them.  Kind refinement does allow existential kinds to make sense however (or at least be usable).  The question then is when does kind-refinement come into play - pattern matches.  TODO generate some examples to motivate this. 
    235259 
    236260