35 | | But, if we have a value of type `Sing a`, how do we get the actual integer or string? |

36 | | We can do this with the overloaded function `fromSing`. Its type is quite general because |

37 | | it can support various singleton families, but for the purposes of this explanation |

38 | | it is sufficient t |

39 | | |

40 | | {{{ |

41 | | fromSing :: Sing (a :: Nat) -> Integer |

42 | | fromSing :: Sing (a :: Symbol) -> String |

43 | | }}} |

44 | | |

45 | | The function `fromSing` has an interesting type: it maps singletons to ordinary values, |

46 | | but the type of the result depends on the ''kind'' of the singleton parameter. |

47 | | So, if we apply it to a value of type `Sing 3` we get the ''number'' `3`, but, |

48 | | if we apply it to a value of type `Sing "hello"` we get the ''string'' `"hello"`. |

49 | | |

50 | | So, how do we make values of type `Sing n` in the first place? This is done with |

| 35 | So, how do we make values of type `Sing n`? This is done with |

| 60 | |

| 61 | |

| 62 | It is also useful to get the actual integer or string associated with a singleton. |

| 63 | We can do this with the overloaded function `fromSing`. Its type is quite general because |

| 64 | it can support various singleton families, but to start, consider the following two instances |

| 65 | of its type: |

| 66 | {{{ |

| 67 | fromSing :: Sing (a :: Nat) -> Integer |

| 68 | fromSing :: Sing (a :: Symbol) -> String |

| 69 | }}} |

| 70 | |

| 71 | Notice that the return type of the function is determined by the ''kind'' of the |

| 72 | singleton family, not the concrete type. For example, for any type `n` of |

| 73 | kind `Nat` we get an `Integer`, while for any type `s` of kind `Symbol` we get a |

| 74 | string. Based on this idea, here is a more general type for `fromSing`: |

| 75 | {{{ |

| 76 | fromSing :: SingE (KindOf a) => Sing a -> Demote a |

| 77 | }}} |

| 78 | |