Changes between Version 3 and Version 4 of TypeNats/SingletonsAndKinds


Ignore:
Timestamp:
Oct 16, 2012 6:22:01 AM (3 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