Version 3 (modified by diatchki, 7 years ago) (diff)

--

## Kind Parameters

We start by defining a kind, which is useful for passing kinds as parameters.

```data OfKind (a :: *) = KindParam
```

Note that we are only interested in the promoted version of this datatype, so basically we just defined a singe type constant with a polymorphic kind:

```KindParam :: OfKind k
```

In addition, it is also convenient to define the following type synonym:

```type KindOf (a :: k) = (KindParam :: OfKind k)
```

This makes it easy to write kind parameters in terms of existing types. Here are some examples:

```KindOf Int  ~ (KindParam :: OfKind *)
KindOf 1    ~ (KindParam :: OfKind Nat)
KindOf "Hi" ~ (KindParam :: OfKind Symbol)
```

Using these types we can define functions that are overloaded based on their kind (rather than type). An example of such a function is `fromSing`, which given an element of a singleton family returns the run-time value representing the singleton. This function uses kind overloading because it uses the same representation for all singletons of a given kind. For example, here are two concrete instances of its type:

```fromSing :: Sing (a :: Nat) -> Integer
fromSing :: Sing (a :: Symbol) -> String
```

Here is how we can define `fromSing` in its full generality:

```class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where
type DemoteRep kparam :: *
fromSing :: Sing (a :: k) -> DemoteRep kparam
```

Here are the different components of this declaration:

1. The class has a single parameter `kparam`, which is of kind `OfKind k`.
2. The super-class constraint makes it explicit that the value of the parameter will always be `KindParam` (One we eliminate `Any`, GHC could probably work this out on its own, but for now we make this explicit.)
3. The associated type synonym `DemoteRep` chooses the representation for singletons of the given kind.
4. Finally, the method `fromSing` maps singletons to their representation.

This might look a bit complex, but defining instances is pretty simple. Here are some examples:

```instance SingE (KindParam :: OfKind Nat) where
type DemoteRep (KindParam :: OfKind Nat) = Integer
fromSing (SNat n) = n

instance SingE (KindParam :: OfKind Symbol) where
type DemoteRep (KindParam :: OfKind Symbol) = String
fromSing (SSym s) = s
```
```{- | A convenient name for the type used to representing the values
for a particular singleton family.  For example, @Demote 2 ~ Integer@,
and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String@. -}
type Demote a = DemoteRep (KindOf a)

{- | A convenience class, useful when we need to both introduce and eliminate
a given singleton value. Users should never need to define instances of
this classes. -}
class    (SingI a, SingE (KindOf a)) => SingRep (a :: k)
instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)

{- | A convenience function useful when we need to name a singleton value
multiple times.  Without this function, each use of 'sing' could potentially
refer to a different singleton, and one has to use type signatures to
ensure that they are the same. -}

withSing :: SingI a => (Sing a -> b) -> b
withSing f = f sing

{- | A convenience function that names a singleton satisfying a certain
property.  If the singleton does not satisfy the property, then the function
returns 'Nothing'. The property is expressed in terms of the underlying
representation of the singleton. -}

singThat :: SingRep a => (Demote a -> Bool) -> Maybe (Sing a)
singThat p = withSing \$ \x -> if p (fromSing x) then Just x else Nothing

instance (SingE (KindOf a), Show (Demote a)) => Show (Sing a) where
showsPrec p = showsPrec p . fromSing

instance (SingRep a, Read (Demote a), Eq (Demote a)) => Read (Sing a) where