Changes between Version 1 and Version 2 of TypeNats/SingletonsAndKinds


Ignore:
Timestamp:
Oct 16, 2012 5:54:53 AM (18 months 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