Changes between Version 13 and Version 14 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 8:37:50 AM (7 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