Changes between Version 3 and Version 4 of TypeNats/SingletonsAndKinds


Ignore:
Timestamp:
Oct 16, 2012 6:22:01 AM (2 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/SingletonsAndKinds

    v3 v4  
    6161}}} 
    6262 
     63It is convenient to define another type synonym, which lets us name 
     64the representation type for a given singleton: 
     65{{{ 
     66type Demote a = DemoteRep (KindOf a) 
     67}}} 
    6368 
     69Here are some examples of using this synonym: 
     70{{{ 
     71Demote 1    ~ Integer 
     72Demote 2    ~ Integer 
     73Demote "hi" ~ String 
     74}}} 
    6475 
     76Using this synonym we can write the type of `fromSing` like this: 
    6577{{{ 
    66 {- | A convenient name for the type used to representing the values 
    67 for a particular singleton family.  For example, @Demote 2 ~ Integer@, 
    68 and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String@. -} 
    69 type Demote a = DemoteRep (KindOf a) 
     78fromSing :: SingE (KindOf a) => Sing a -> Demote a 
     79}}} 
    7080 
    71 {- | A convenience class, useful when we need to both introduce and eliminate 
    72 a given singleton value. Users should never need to define instances of 
    73 this classes. -} 
    74 class    (SingI a, SingE (KindOf a)) => SingRep (a :: k) 
    75 instance (SingI a, SingE (KindOf a)) => SingRep (a :: k) 
    76  
    77  
    78 {- | A convenience function useful when we need to name a singleton value 
    79 multiple times.  Without this function, each use of 'sing' could potentially 
    80 refer to a different singleton, and one has to use type signatures to 
    81 ensure that they are the same. -} 
    82  
    83 withSing :: SingI a => (Sing a -> b) -> b 
    84 withSing f = f sing 
    85  
    86  
    87 {- | A convenience function that names a singleton satisfying a certain 
    88 property.  If the singleton does not satisfy the property, then the function 
    89 returns 'Nothing'. The property is expressed in terms of the underlying 
    90 representation of the singleton. -} 
    91  
    92 singThat :: SingRep a => (Demote a -> Bool) -> Maybe (Sing a) 
    93 singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing 
    94  
    95  
     81Here is an example of using all this to provide a `Show` instance 
     82for singleton families: 
     83{{{ 
    9684instance (SingE (KindOf a), Show (Demote a)) => Show (Sing a) where 
    9785  showsPrec p = showsPrec p . fromSing 
    9886 
    99 instance (SingRep a, Read (Demote a), Eq (Demote a)) => Read (Sing a) where 
    100   readsPrec p cs = do (x,ys) <- readsPrec p cs 
    101                       case singThat (== x) of 
    102                         Just y  -> [(y,ys)] 
    103                         Nothing -> [] 
    10487}}} 
    10588 
    106