Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.TypeRepTYPE

Contents

Orphan instances

Description

This module defines singleton instances making TypeRep the singleton for the kind TYPE rep (for some RuntimeRep rep), an instantiation of which is the famous kind Type. The definitions don't fully line up with what is expected within the singletons library, so expect unusual results!

Synopsis

type family Sing :: k -> Type
data SomeTypeRepTYPE :: RuntimeRep -> Type where
- SomeTypeRepTYPE :: forall (rep :: RuntimeRep) (a :: TYPE rep). !(TypeRep a) -> SomeTypeRepTYPE rep

Documentation

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type
type Sing Source #	A choice of singleton for the kind `TYPE rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`. Conceivably, one could generalize this instance to `Sing @k` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks). We cannot produce explicit singleton values for everything in `TYPE rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.
Instance details Defined in Data.Singletons.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

Here is the definition of the singleton for TYPE rep:

type instance Sing \@(TYPE rep) = TypeRep

Instances for SingI, SingKind, SEq, SDecide, and TestCoercion are also supplied.

data SomeTypeRepTYPE :: RuntimeRep -> Type where Source #

A variant of SomeTypeRep whose underlying TypeRep is restricted to kind TYPE rep (for some RuntimeRep rep).

Constructors

SomeTypeRepTYPE :: forall (rep :: RuntimeRep) (a :: TYPE rep). !(TypeRep a) -> SomeTypeRepTYPE rep

Instances

Instances details

Eq (SomeTypeRepTYPE rep) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods (==) :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool # (/=) :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool #
Ord (SomeTypeRepTYPE rep) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods compare :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Ordering # (<) :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool # (<=) :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool # (>) :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool # (>=) :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool # max :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep # min :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep #
Show (SomeTypeRepTYPE rep) Source #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods showsPrec :: Int -> SomeTypeRepTYPE rep -> ShowS # show :: SomeTypeRepTYPE rep -> String # showList :: [SomeTypeRepTYPE rep] -> ShowS #

Orphan instances

SingKind (TYPE rep) Source #
Instance details Associated Types type Demote (TYPE rep) = (r :: Type) Source # Methods fromSing :: forall (a :: TYPE rep). Sing a -> Demote (TYPE rep) Source # toSing :: Demote (TYPE rep) -> SomeSing (TYPE rep) Source #
SDecide (TYPE rep) Source #
Instance details Methods (%~) :: forall (a :: TYPE rep) (b :: TYPE rep). Sing a -> Sing b -> Decision (a :~: b) Source #
PEq (TYPE rep) Source #
Instance details Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq (TYPE rep) Source #
Instance details Methods (%==) :: forall (a :: TYPE rep) (b :: TYPE rep). Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: forall (a :: TYPE rep) (b :: TYPE rep). Sing a -> Sing b -> Sing (a /= b) Source #
Typeable a => SingI (a :: TYPE rep) Source #
Instance details Methods sing :: Sing a Source #