User:Zzo38/Proposal for additional kinds
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
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
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.
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.