singletons-2.6: A framework for generating singleton types

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.Instances type Sing = SNonEmpty :: NonEmpty 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 = SIdentity :: Identity 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 = SMax :: Max a -> 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 = SOption :: Option 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 = SDual :: Dual 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.Semigroup.Internal type Sing = SSum :: Sum 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.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.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.Prelude.Semigroup type Sing = SArg :: Arg a b -> 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 #