Changes between Version 1 and Version 2 of TypeNats/SingletonsAndKinds


Ignore:
Timestamp:
Oct 16, 2012 5:54:53 AM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndKinds

    v1 v2  
     1== Kind Parameters and Overloading On Kinds ==
     2
     3We start by defining a ''kind'', which is useful for passing kinds as parameters.
     4{{{
     5data OfKind (a :: *) = KindParam
     6}}}
     7Note that we are only interested in the promoted version of this datatype,
     8so basically we just defined a singe type constant with a polymorphic kind:
     9{{{
     10KindParam :: OfKind k
     11}}}
     12
     13In addition, it is also convenient to define the following type synonym:
     14{{{
     15type KindOf (a :: k) = (KindParam :: OfKind k)
     16}}}
     17
     18This makes it easy to write kind parameters in terms of existing types.
     19Here are some examples:
     20{{{
     21KindOf Int  ~ (KindParam :: OfKind *)
     22KindOf 1    ~ (KindParam :: OfKind Nat)
     23KindOf "Hi" ~ (KindParam :: OfKind Symbol)
     24}}}
     25
    126
    227
    328{{{
    4 -- | (Kind) A kind useful for passing kinds as parameters.
    5 data OfKind (a :: *) = KindParam
    6 
    7 {- | A shortcut for naming the kind parameter corresponding to the
    8 kind of a some type.  For example, @KindOf Int ~ (KindParam :: OfKind *)@,
    9 but @KindOf 2 ~ (KindParam :: OfKind Nat)@. -}
    10 type KindOf (a :: k) = (KindParam :: OfKind k)
    11 
    12 
    1329-- | (Kind) This is the kind of type-level natural numbers.
    1430data Nat