32 | | -- | (Kind) This is the kind of type-level symbols. |
33 | | data Symbol |
34 | | |
35 | | |
36 | | -------------------------------------------------------------------------------- |
37 | | data family Sing (n :: k) |
38 | | |
39 | | newtype instance Sing (n :: Nat) = SNat Integer |
40 | | |
41 | | newtype instance Sing (n :: Symbol) = SSym String |
42 | | |
43 | | -------------------------------------------------------------------------------- |
44 | | |
45 | | -- | The class 'SingI' provides a \"smart\" constructor for singleton types. |
46 | | -- There are built-in instances for the singleton types corresponding |
47 | | -- to type literals. |
48 | | |
49 | | class SingI a where |
50 | | |
51 | | -- | The only value of type @Sing a@ |
52 | | sing :: Sing a |
53 | | |
54 | | |
55 | | {- | A class that converts singletons of a given kind into values of some |
56 | | representation type (i.e., we "forget" the extra information carried |
57 | | by the singletons, and convert them to ordinary values). |
58 | | |
59 | | Note that 'fromSing' is overloaded based on the /kind/ of the values |
60 | | and not their type---all types of a given kind are processed by the |
61 | | same instances. |
62 | | -} |
63 | | |
| 38 | Here is how we can define `fromSing` in its full generality: |
| 39 | {{{ |
| 45 | Here are the different components of this declaration: |
| 46 | 1. The class has a single parameter `kparam`, which is of kind `OfKind k`. |
| 47 | 2. The super-class constraint makes it explicit that the value of the parameter will always be `KindParam` |
| 48 | (One we eliminate `Any`, GHC could probably work this out on its own, but for now we make this explicit.) |
| 49 | 3. The associated type synonym `DemoteRep` chooses the representation for singletons of the given kind. |
| 50 | 4. Finally, the method `fromSing` maps singletons to their representation. |
| 51 | |
| 52 | This might look a bit complex, but defining instances is pretty simple. Here are some examples: |
| 53 | {{{ |