56 | | -- Built-in instances for all type0literals. |
57 | | instance SingI 0 where sing = // ... the singleton value representing 0 ... |
58 | | instance SingI 1 where sing = // ... the singleton value representing 1 ... |
59 | | instance SingI "hello" where sing = // ... the singleton value representing "hello" ... |
| 56 | -- Built-in instances for all type-literals. |
| 57 | instance SingI 0 where sing = ... the singleton value representing 0 ... |
| 58 | instance SingI 1 where sing = ... the singleton value representing 1 ... |
| 59 | instance SingI "hello" where sing = ... the singleton value representing "hello" ... |
| 62 | |
| 63 | Here are some examples on the GHCi prompt to get a feel of how `sing` works: |
| 64 | {{{ |
| 65 | > :set -XDataKinds |
| 66 | > sing :: Sing 1 |
| 67 | > 1 |
| 68 | > sing :: Sing "hello" |
| 69 | > "hello" |
| 70 | }}} |
| 71 | |
| 72 | The name ''SingI'' is a mnemonic for the different uses of the class: |
| 73 | * It is the ''introduction'' construct for 'Sing' values, |
| 74 | * It is an ''implicit'' singleton parameter (this is discussed in more detail bellow) |
| 75 | |
| 76 | Notice that GHCi could display values of type `Sing`, so they have a `Show` instance. As another example, here |
| 77 | is the definition of the `Show` instance: |
| 78 | {{{ |
| 79 | instance Show (SingRep a) => Show (Sing a) where |
| 80 | showsPrec p = showsPrec p . fromSing |
| 81 | }}} |
| 82 | Easy! We just convert the singleton into an ordinary value (integer or string), and use ''its'' `Show` instance to display it. |
| 83 | |
| 84 | Next, we show two functions which make it easier to work with singleton types: |
| 85 | |
| 86 | {{{ |
| 87 | withSing :: SingI a => (Sing a -> b) -> b |
| 88 | withSing f = f sing |
| 89 | |
| 90 | singThat :: SingI a => (SingRep a -> Bool) -> Maybe (Sing a) |
| 91 | singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing |
| 92 | }}} |
| 93 | |
| 94 | The first function, `withSing`, is useful when we want to work with the same singleton value multiple times. |
| 95 | The constant `sing` is polymorphic, so every time we use it in a program, it may refer to a potentially |
| 96 | different singleton, so to ensure that two singleton values are the same we have to resort to |
| 97 | explicit type signatures, which just adds noise to a definition. By using, `withSing` we avoid this problem |
| 98 | because we get an explicit (monomorphic) name for a given singleton, and so we can use the name many times |
| 99 | without any type signatures. This technique is shown in the definition of the second function, `singThat`. |
| 100 | |
| 101 | The function `singThat` is similar to the constant `sing` in that it defines new singleton values. However, |
| 102 | it allows us to specify a predicate on (the representation of) the value and it only succeeds if this predicate |
| 103 | holds. Here are some examples of how that works: |
| 104 | |
| 105 | {{{ |
| 106 | > singThat (== 1) :: Maybe (Sing 1) |
| 107 | > Just 1 |
| 108 | > singThat (== 1) :: Maybe (Sing 2) |
| 109 | > Nothing |
| 110 | > singThat ("he" `isPrefixOf`) :: Maybe (Sing "hello") |
| 111 | > Just "hello" |
| 112 | }}} |
| 113 | |
| 114 | Now, using `singThat` we can show the definition of the `Read` instance for singletons: |
| 115 | |
| 116 | {{{ |
| 117 | instance (SingI a, Read (SingRep a), Eq (SingRep a)) => Read (Sing a) where |
| 118 | readsPrec p cs = do (x,ys) <- readsPrec p cs |
| 119 | case singThat (== x) of |
| 120 | Just y -> [(y,ys)] |
| 121 | Nothing -> [] |
| 122 | }}} |
| 123 | |
| 124 | We use the `Read` instance of the representation for the singletons to parse a value, |
| 125 | and then, we use `singThat` to make sure that this was the value corresponding to |
| 126 | the singleton. |
73 | | -- Convenient derived functions |
74 | | tNatThat :: NatI n => (Integer -> Bool) -> Maybe (TNat n) |
75 | | withTNat :: NatI n => (TNat n -> a) -> a |
76 | | }}} |
77 | | The only "interesting" value of type {{{TNat n}}} is the number {{{n}}}. Technically, there is also an undefined element. |
78 | | The value of a singleton type may be named using {{{tNat}}}, which is a bit like a "smart" constructor for {{{TNat n}}}. |
79 | | Note that because {{{tNat}}} is polymorphic, we may have to use a type signature to specify which singleton we mean. For example: |
80 | | |
81 | | One may think of the smart constructor {{{tNat}}} as being a method of a special built-in class, {{{NatI}}}: |
82 | | {{{ |
83 | | class NatI n where |
84 | | tNat :: TNat n |
85 | | |
86 | | instance NatI 0 where tNat = ...singleton 0 value... |
87 | | instance NatI 1 where tNat = ...singleton 1 value... |
88 | | instance NatI 2 where tNat = ...singleton 2 value... |
89 | | etc. |
90 | | }}} |
91 | | |
92 | | The name ''NatI'' is a mnemonic for the different uses of the class: |
93 | | * It is the ''introduction'' construct for 'TNat' values, |
94 | | * It is an ''implicit'' parameter of kind 'TNat' (this is discussed in more detail bellow) |