Version 1 (modified by diatchki, 18 months ago) (diff) |
---|

-- | (Kind) A kind useful for passing kinds as parameters. data OfKind (a :: *) = KindParam {- | A shortcut for naming the kind parameter corresponding to the kind of a some type. For example, @KindOf Int ~ (KindParam :: OfKind *)@, but @KindOf 2 ~ (KindParam :: OfKind Nat)@. -} type KindOf (a :: k) = (KindParam :: OfKind k) -- | (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 -> []