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 | |
| 182 | We 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 | }}} |
| 189 | Choices |
| 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 | {{{ |
| 201 | data kind MaybeK k = NothingK | JustK k |
| 202 | }}} |
| 203 | |
| 204 | So 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 | |
| 211 | It might also be nice to support GADK (Generalized Algebraic Data Kind) syntax for declaring kinds, ala: |
| 212 | |
| 213 | {{{ |
| 214 | data kind MaybeK :: ** -> ** where |
| 215 | NothingK :: MaybeK k |
| 216 | JustK :: k -> MaybeK k |
| 217 | }}} |
| 218 | |
| 219 | Again, note that {{{Maybe}}} above is decorated with a {{{sort}}} signature. |
| 220 | |
| 221 | or |
| 222 | |
| 223 | {{{ |
| 224 | data kind MaybeK k where |
| 225 | NothingK :: MaybeK k |
| 226 | JustK :: k -> MaybeK k |
| 227 | }}} |
| 228 | |
| 229 | However no GADTs or existentials at the kind level (yet). TODO think about motivating examples. |
| 230 | |
| 231 | 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. |
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. |