Version 2 (modified by diatchki, 4 years ago) (diff) |
---|

## Kind Parameters and Overloading On Kinds

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) This is the kind of type-level natural numbers. data Nat -- | (Kind) This is the kind of type-level symbols. data Symbol -------------------------------------------------------------------------------- data family Sing (n :: k) newtype instance Sing (n :: Nat) = SNat Integer newtype instance Sing (n :: Symbol) = SSym String -------------------------------------------------------------------------------- -- | The class 'SingI' provides a \"smart\" constructor for singleton types. -- There are built-in instances for the singleton types corresponding -- to type literals. class SingI a where -- | The only value of type @Sing a@ sing :: Sing a {- | A class that converts singletons of a given kind into values of some representation type (i.e., we "forget" the extra information carried by the singletons, and convert them to ordinary values). Note that 'fromSing' is overloaded based on the /kind/ of the values and not their type---all types of a given kind are processed by the same instances. -} class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where type DemoteRep kparam :: * fromSing :: Sing (a :: k) -> DemoteRep kparam 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 -> []