Difference between revisions of "User:Zzo38/Proposal for additional kinds"
Jump to navigation
Jump to search
| (5 intermediate revisions by the same user not shown) | |||
| Line 3: | Line 3: | ||
==New kinds== |
==New kinds== |
||
## -- New name for (#) kind (although (#) is available for compatibility) |
## -- New name for (#) kind (although (#) is available for compatibility) |
||
| − | + | & -- Kind for classes |
|
+ -- 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== |
||
Example: |
Example: |
||
| − | + | * -> & -- Kind of Eq class. |
|
| − | + | (* -> *) -> & -- Kind of Monad class. |
|
| + | (* -> &) -> & -- Class of classes. |
||
| − | * -> [*] -- A class that requires a type as a parameter to make a class. |
||
| − | + | + -> * -> & -- Infinite series of classes, selected by a natural number. |
|
| − | <!-- <b></b> means make it appear correctly on HTML view --> |
||
==Natural number kind== |
==Natural number kind== |
||
| Line 18: | Line 18: | ||
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. |
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 <tt>+ -> + -> +</tt> can be a type of adding numbers or other stuff like that, too. |
||
| + | |||
| + | A natural number type would be a type with the number of values being that number, for example <tt>4</tt> is <tt>Maybe (Maybe (Maybe (Maybe Zero)))</tt>, and <tt>(->)</tt> would be the type for a array with a specific number of elements fixed by the type. |
||
| + | |||
| + | ==See also== |
||
| + | * [http://hackage.haskell.org/trac/ghc/wiki/KindFact KindFact] |
||
[[Category:Proposals]] |
[[Category:Proposals]] |
||
Latest revision as of 20:18, 12 January 2012
This document is proposal about additional kinds.
New kinds
## -- New name for (#) kind (although (#) is available for compatibility) & -- Kind for classes + -- 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. (* -> &) -> & -- Class of classes. + -> * -> & -- Infinite series of classes, selected by a natural number.
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.
A natural number type would be a type with the number of values being that number, for example 4 is Maybe (Maybe (Maybe (Maybe Zero))), and (->) would be the type for a array with a specific number of elements fixed by the type.