Version 3 (modified by diatchki, 3 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:

  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
  readsPrec p cs = do (x,ys) <- readsPrec p cs
                      case singThat (== x) of
                        Just y  -> [(y,ys)]
                        Nothing -> []