Changes between Version 3 and Version 4 of TypeNats/SingletonsAndKinds
 Timestamp:
 Oct 16, 2012 6:22:01 AM (7 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeNats/SingletonsAndKinds
v3 v4 61 61 }}} 62 62 63 It is convenient to define another type synonym, which lets us name 64 the representation type for a given singleton: 65 {{{ 66 type Demote a = DemoteRep (KindOf a) 67 }}} 63 68 69 Here are some examples of using this synonym: 70 {{{ 71 Demote 1 ~ Integer 72 Demote 2 ~ Integer 73 Demote "hi" ~ String 74 }}} 64 75 76 Using this synonym we can write the type of `fromSing` like this: 65 77 {{{ 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) 78 fromSing :: SingE (KindOf a) => Sing a > Demote a 79 }}} 70 80 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 81 Here is an example of using all this to provide a `Show` instance 82 for singleton families: 83 {{{ 96 84 instance (SingE (KindOf a), Show (Demote a)) => Show (Sing a) where 97 85 showsPrec p = showsPrec p . fromSing 98 86 99 instance (SingRep a, Read (Demote a), Eq (Demote a)) => Read (Sing a) where100 readsPrec p cs = do (x,ys) < readsPrec p cs101 case singThat (== x) of102 Just y > [(y,ys)]103 Nothing > []104 87 }}} 105 88 106