| 47 | == Examples == |

| 48 | |

| 49 | Here is how we can use this API to define a `Show` instance for singleton types: |

| 50 | {{{ |

| 51 | instance Show (Nat n) where |

| 52 | showsPrec p n = showsPrec p (natToInteger n) |

| 53 | }}} |

| 54 | |

| 55 | A more interesting example is to define a function which maps integers into singleton types: |

| 56 | {{{ |

| 57 | integerToMaybeNat :: TypeNat n => Integer -> Maybe (Nat n) |

| 58 | integerToMaybeNat x = check nat |

| 59 | where check y = if x == natToInteger y then Just y else Nothing |

| 60 | }}} |

| 61 | |

| 62 | The implementation of `integerToMaybeNat` is a little subtle: by using |

| 63 | the helper function `check`, we ensure that the two occurrences of |

| 64 | `nat` (aka `y`) both have the same type, namely `Nat n`. There are other |

| 65 | ways to achieve the same, for example, by using scoped type variables, |

| 66 | and providing explicit type signatures. |

| 67 | |

| 68 | Now, we can use `integerToNat` to provide a `Read` instance for singleton types: |

| 69 | {{{ |

| 70 | instance TypeNat n => Read (Nat n) where |

| 71 | readsPrec p x = do (x,xs) <- readsPrec p x |

| 72 | case integerToMaybeNat x of |

| 73 | Just n -> [(n,xs)] |

| 74 | Nothing -> [] |

| 75 | }}} |

| 76 | |