Changes between Version 2 and Version 3 of TypeNats/SingletonsAndKinds


Ignore:
Timestamp:
Oct 16, 2012 6:13:58 AM (18 months ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndKinds

    v2 v3  
    1 == Kind Parameters and Overloading On Kinds == 
     1== Kind Parameters == 
    22 
    33We start by defining a ''kind'', which is useful for passing kinds as parameters. 
     
    2525 
    2626 
     27== Kind-based Overloading == 
    2728 
     29Using these types we can define functions that are overloaded based on their ''kind'' (rather than ''type''). 
     30An example of such a function is `fromSing`, which given an element of a singleton family returns the run-time 
     31value representing the singleton.  This function uses kind overloading because it uses the same representation 
     32for all singletons of a given kind.  For example, here are two concrete instances of its type: 
    2833{{{ 
    29 -- | (Kind) This is the kind of type-level natural numbers. 
    30 data Nat 
     34fromSing :: Sing (a :: Nat) -> Integer 
     35fromSing :: Sing (a :: Symbol) -> String 
     36}}} 
    3137 
    32 -- | (Kind) This is the kind of type-level symbols. 
    33 data Symbol 
    34  
    35  
    36 -------------------------------------------------------------------------------- 
    37 data family Sing (n :: k) 
    38  
    39 newtype instance Sing (n :: Nat)    = SNat Integer 
    40  
    41 newtype instance Sing (n :: Symbol) = SSym String 
    42  
    43 -------------------------------------------------------------------------------- 
    44  
    45 -- | The class 'SingI' provides a \"smart\" constructor for singleton types. 
    46 -- There are built-in instances for the singleton types corresponding 
    47 -- to type literals. 
    48  
    49 class SingI a where 
    50  
    51   -- | The only value of type @Sing a@ 
    52   sing :: Sing a 
    53  
    54  
    55 {- | A class that converts singletons of a given kind into values of some 
    56 representation type (i.e., we "forget" the extra information carried 
    57 by the singletons, and convert them to ordinary values). 
    58  
    59 Note that 'fromSing' is overloaded based on the /kind/ of the values 
    60 and not their type---all types of a given kind are processed by the 
    61 same instances. 
    62 -} 
    63  
     38Here is how we can define `fromSing` in its full generality: 
     39{{{ 
    6440class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where 
    6541  type DemoteRep kparam :: * 
    6642  fromSing :: Sing (a :: k) -> DemoteRep kparam 
     43}}} 
    6744 
     45Here are the different components of this declaration: 
     46  1. The class has a single parameter `kparam`, which is of kind `OfKind k`. 
     47  2. The super-class constraint makes it explicit that the value of the parameter will always be `KindParam` 
     48     (One we eliminate `Any`, GHC could probably work this out on its own, but for now we make this explicit.) 
     49  3. The associated type synonym `DemoteRep` chooses the representation for singletons of the given kind. 
     50  4. Finally, the method `fromSing` maps singletons to their representation. 
     51 
     52This might look a bit complex, but defining instances is pretty simple.  Here are some examples: 
     53{{{ 
    6854instance SingE (KindParam :: OfKind Nat) where 
    6955  type DemoteRep (KindParam :: OfKind Nat) = Integer 
     
    7359  type DemoteRep (KindParam :: OfKind Symbol) = String 
    7460  fromSing (SSym s) = s 
     61}}} 
    7562 
     63 
     64 
     65{{{ 
    7666{- | A convenient name for the type used to representing the values 
    7767for a particular singleton family.  For example, @Demote 2 ~ Integer@,