Version 3 (modified by 5 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)

## Kind-based Overloading

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:

- The class has a single parameter
`kparam`

, which is of kind`OfKind k`

. - 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.) - The associated type synonym
`DemoteRep`

chooses the representation for singletons of the given kind. - 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 readsPrec p cs = do (x,ys) <- readsPrec p cs case singThat (== x) of Just y -> [(y,ys)] Nothing -> []