Difference between revisions of "User:Zzo38/Proposal for additional kinds"
Jump to navigation
Jump to search
Line 5: | Line 5: | ||
[x] -- If x is a kind, [x] is the kind of classes of types of kind x |
[x] -- If x is a kind, [x] is the kind of classes of types of kind x |
||
+ -- Kind for type-level natural numbers |
+ -- Kind for type-level natural numbers |
||
+ | $ -- Means make up a kind from a Template Haskell code |
||
==Kind of classes== |
==Kind of classes== |
||
Line 12: | Line 13: | ||
* -> [*] -- A class that requires a type as a parameter to make a class. |
* -> [*] -- A class that requires a type as a parameter to make a class. |
||
[<b></b>[*]] -- Class of classes. |
[<b></b>[*]] -- Class of classes. |
||
+ | + -> [*] -- Infinite series of classes, selected by a natural number. |
||
+ | forall k. k -> [k] -- Polymorphic class that corresponds to any given kind. |
||
<!-- <b></b> means make it appear correctly on HTML view --> |
<!-- <b></b> means make it appear correctly on HTML view --> |
||
Revision as of 21:58, 3 September 2011
This document is proposal about additional kinds.
New kinds
## -- New name for (#) kind (although (#) is available for compatibility) [x] -- If x is a kind, [x] is the kind of classes of types of kind x + -- Kind for type-level natural numbers $ -- Means make up a kind from a Template Haskell code
Kind of classes
Example:
[*] -- Kind of Eq class. [* -> *] -- Kind of Monad class. * -> [*] -- A class that requires a type as a parameter to make a class. [[*]] -- Class of classes. + -> [*] -- Infinite series of classes, selected by a natural number. forall k. k -> [k] -- Polymorphic class that corresponds to any given kind.
Natural number kind
If a type requires a parameter, it can be a + kind, meaning numbers.
There should be some way to specify a type taking natural numbers by defining it for zero and them for a successor, so that it applies for all natural numbers.
It also means a type of kind + -> + -> + can be a type of adding numbers or other stuff like that, too.