singletons-3.0.2: Basic singleton types and definitions

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

Data.Singletons

Contents

- Main singleton definitions
- Working with singletons
  - `WrappedSing`
  - Defunctionalization
  - Defunctionalized singletons
- Auxiliary functions
- Defunctionalization symbols

Description

This module exports the basic definitions to use singletons. See also `Prelude.Singletons` from the `singletons-base` library, which re-exports this module alongside many singled definitions based on the Prelude.

You may also want to read the original papers presenting this library, available at https://richarde.dev/papers/2012/singletons/paper.pdf and https://richarde.dev/papers/2014/promotion/promotion.pdf.

Synopsis

- type family Sing :: k -> Type
- newtype SLambda (f :: k1 ~> k2) = SLambda {
  - applySing :: forall t. Sing t -> Sing (f @@ t)
  }
- (@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
- class SingI a where
  - sing :: Sing a
- class (forall x. SingI x => SingI (f x)) => SingI1 f where
  - liftSing :: Sing x -> Sing (f x)
- sing1 :: (SingI1 f, SingI x) => Sing (f x)
- class (forall x y. (SingI x, SingI y) => SingI (f x y)) => SingI2 f where
  - liftSing2 :: Sing x -> Sing y -> Sing (f x y)
- sing2 :: (SingI2 f, SingI x, SingI y) => Sing (f x y)
- class SingKind k where
  - type Demote k = (r :: Type) | r -> k
  - fromSing :: Sing (a :: k) -> Demote k
  - toSing :: Demote k -> SomeSing k
- type KindOf (a :: k) = k
- type SameKind (a :: k) (b :: k) = () :: Constraint
- data SingInstance (a :: k) where
  - SingInstance :: SingI a => SingInstance a
- data SomeSing k where
  - SomeSing :: Sing (a :: k) -> SomeSing k
- singInstance :: forall k (a :: k). Sing a -> SingInstance a
- pattern Sing :: forall k (a :: k). () => SingI a => Sing a
- withSingI :: Sing n -> (SingI n => r) -> r
- withSomeSing :: forall k r. SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
- pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k
- usingSingI1 :: forall f x r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r
- usingSingI2 :: forall f x y r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => r) -> r
- singByProxy :: SingI a => proxy a -> Sing a
- singByProxy1 :: (SingI1 f, SingI x) => proxy (f x) -> Sing (f x)
- singByProxy2 :: (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y)
- demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k
- demote1 :: forall {k1} {k2} (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => Demote k2
- demote2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => Demote k3
- singByProxy# :: SingI a => Proxy# a -> Sing a
- singByProxy1# :: (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)
- singByProxy2# :: (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y)
- withSing :: SingI a => (Sing a -> b) -> b
- withSing1 :: (SingI1 f, SingI x) => (Sing (f x) -> b) -> b
- withSing2 :: (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> b) -> b
- singThat :: forall k (a :: k). (SingKind k, SingI a) => (Demote k -> Bool) -> Maybe (Sing a)
- singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => (Demote k2 -> Bool) -> Maybe (Sing (f x))
- singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => (Demote k3 -> Bool) -> Maybe (Sing (f x y))
- newtype WrappedSing :: forall k. k -> Type where
  - WrapSing :: forall k (a :: k). {..} -> WrappedSing a
- newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
  - SWrapSing :: forall k (a :: k) (ws :: WrappedSing a). {..} -> SWrappedSing ws
- type family UnwrapSing (ws :: WrappedSing (a :: k)) :: Sing a where ...
- data TyFun :: Type -> Type -> Type
- type (~>) a b = TyFun a b -> Type
- type TyCon1 = TyCon :: (k1 -> k2) -> k1 ~> k2
- type TyCon2 = TyCon :: (k1 -> k2 -> k3) -> k1 ~> (k2 ~> k3)
- type TyCon3 = TyCon :: (k1 -> k2 -> k3 -> k4) -> k1 ~> (k2 ~> (k3 ~> k4))
- type TyCon4 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> k5)))
- type TyCon5 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> k6))))
- type TyCon6 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> k7)))))
- type TyCon7 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> k8))))))
- type TyCon8 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> k9)))))))
- type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
- type (@@) a b = Apply a b
- data family TyCon :: (k1 -> k2) -> unmatchable_fun
- type family ApplyTyCon :: (k1 -> k2) -> k1 ~> unmatchable_fun where ...
- data ApplyTyConAux1 :: (k1 -> k2) -> k1 ~> k2
- data ApplyTyConAux2 :: (k1 -> k2 -> k3) -> k1 ~> unmatchable_fun
- singFun1 :: forall f. SingFunction1 f -> Sing f
- singFun2 :: forall f. SingFunction2 f -> Sing f
- singFun3 :: forall f. SingFunction3 f -> Sing f
- singFun4 :: forall f. SingFunction4 f -> Sing f
- singFun5 :: forall f. SingFunction5 f -> Sing f
- singFun6 :: forall f. SingFunction6 f -> Sing f
- singFun7 :: forall f. SingFunction7 f -> Sing f
- singFun8 :: forall f. SingFunction8 f -> Sing f
- unSingFun1 :: forall f. Sing f -> SingFunction1 f
- unSingFun2 :: forall f. Sing f -> SingFunction2 f
- unSingFun3 :: forall f. Sing f -> SingFunction3 f
- unSingFun4 :: forall f. Sing f -> SingFunction4 f
- unSingFun5 :: forall f. Sing f -> SingFunction5 f
- unSingFun6 :: forall f. Sing f -> SingFunction6 f
- unSingFun7 :: forall f. Sing f -> SingFunction7 f
- unSingFun8 :: forall f. Sing f -> SingFunction8 f
- pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
- applySing2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f
- pattern SLambda3 :: forall f. SingFunction3 f -> Sing f
- applySing3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> SingFunction3 f
- pattern SLambda4 :: forall f. SingFunction4 f -> Sing f
- applySing4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> SingFunction4 f
- pattern SLambda5 :: forall f. SingFunction5 f -> Sing f
- applySing5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> SingFunction5 f
- pattern SLambda6 :: forall f. SingFunction6 f -> Sing f
- applySing6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> SingFunction6 f
- pattern SLambda7 :: forall f. SingFunction7 f -> Sing f
- applySing7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> SingFunction7 f
- pattern SLambda8 :: forall f. SingFunction8 f -> Sing f
- applySing8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> SingFunction8 f
- type SingFunction1 (f :: a1 ~> b) = forall t. Sing t -> Sing (f @@ t)
- type SingFunction2 (f :: a1 ~> (a2 ~> b)) = forall t1 t2. Sing t1 -> Sing t2 -> Sing ((f @@ t1) @@ t2)
- type SingFunction3 (f :: a1 ~> (a2 ~> (a3 ~> b))) = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (((f @@ t1) @@ t2) @@ t3)
- type SingFunction4 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))) = forall t1 t2 t3 t4. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing ((((f @@ t1) @@ t2) @@ t3) @@ t4)
- type SingFunction5 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))) = forall t1 t2 t3 t4 t5. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing (((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)
- type SingFunction6 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))) = forall t1 t2 t3 t4 t5 t6. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing ((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)
- type SingFunction7 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))) = forall t1 t2 t3 t4 t5 t6 t7. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing (((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7)
- type SingFunction8 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))) = forall t1 t2 t3 t4 t5 t6 t7 t8. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8 -> Sing ((((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7) @@ t8)
- data Proxy (t :: k) = Proxy
- data DemoteSym0 :: Type ~> Type
- type DemoteSym1 x = Demote x
- data SameKindSym0 :: forall k. k ~> (k ~> Constraint)
- data SameKindSym1 :: forall k. k -> k ~> Constraint
- type SameKindSym2 (x :: k) (y :: k) = SameKind x y
- data KindOfSym0 :: forall k. k ~> Type
- type KindOfSym1 (x :: k) = KindOf x
- data (~>@#@$) :: Type ~> (Type ~> Type)
- data (~>@#@$$) :: Type -> Type ~> Type
- type (~>@#@$$$) x y = x ~> y
- data ApplySym0 :: forall a b. (a ~> b) ~> (a ~> b)
- data ApplySym1 :: forall a b. (a ~> b) -> a ~> b
- type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x
- data (@@@#@$) :: forall a b. (a ~> b) ~> (a ~> b)
- data (@@@#@$$) :: forall a b. (a ~> b) -> a ~> b
- type (@@@#@$$$) (f :: a ~> b) (x :: a) = f @@ x

# Main singleton definitions

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

#### Instances

Instances details

type Sing Source # |
Instance details Defined in Data.Singletons type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type

newtype SLambda (f :: k1 ~> k2) Source #

Constructors

SLambda |

Fields

- applySing :: forall t. Sing t -> Sing (f @@ t)

(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t) infixl 9 Source #

An infix synonym for `applySing`

class SingI a where Source #

A `SingI` constraint is essentially an implicitly-passed singleton. If you need to satisfy this constraint with an explicit singleton, please see `withSingI` or the `Sing` pattern synonym.

Methods

sing :: Sing a Source #

Produce the singleton explicitly. You will likely need the `ScopedTypeVariables` extension to use this method the way you want.

#### Instances

Instances details

SingI a => SingI ('WrapSing s :: WrappedSing a) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing ('WrapSing s) Source #
(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> TyFun k1 kr -> Type) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: TyFun k1 kr -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon1 f) Source #
(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> TyFun k2 kr -> Type) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: TyFun k1 (k2 ~> kr) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon2 f) Source #
(SingI fst, SingI b) => SingI (a ':&: b :: Sigma s t) Source # |
Instance details Defined in Data.Singletons.Sigma Methods sing :: Sing (a ':&: b) Source #
(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> TyFun k3 kr -> Type) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: TyFun k1 (k2 ~> (k3 ~> kr)) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon3 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> TyFun k4 kr -> Type) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> kr))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon4 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> TyFun k5 kr -> Type) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon5 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> TyFun k6 kr -> Type) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon6 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> TyFun k7 kr -> Type) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon7 f) Source #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> TyFun k8 kr -> Type) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))) -> Type) Source #

Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon8 f) Source #

class (forall x. SingI x => SingI (f x)) => SingI1 f where Source #

A version of the `SingI` class lifted to unary type constructors.

Methods

liftSing :: Sing x -> Sing (f x) Source #

Lift an explicit singleton through a unary type constructor. You will likely need the `ScopedTypeVariables` extension to use this method the way you want.

sing1 :: (SingI1 f, SingI x) => Sing (f x) Source #

Produce a singleton explicitly using implicit `SingI1` and `SingI` constraints. You will likely need the `ScopedTypeVariables` extension to use this method the way you want.

class (forall x y. (SingI x, SingI y) => SingI (f x y)) => SingI2 f where Source #

A version of the `SingI` class lifted to binary type constructors.

Methods

liftSing2 :: Sing x -> Sing y -> Sing (f x y) Source #

Lift explicit singletons through a binary type constructor. You will likely need the `ScopedTypeVariables` extension to use this method the way you want.

sing2 :: (SingI2 f, SingI x, SingI y) => Sing (f x y) Source #

Produce a singleton explicitly using implicit `SingI2` and `SingI` constraints. You will likely need the `ScopedTypeVariables` extension to use this method the way you want.

class SingKind k where Source #

The `SingKind` class is a kind class. It classifies all kinds for which singletons are defined. The class supports converting between a singleton type and the base (unrefined) type which it is built from.

For a `SingKind` instance to be well behaved, it should obey the following laws:

    toSing . fromSing ≡ SomeSing
    (\x -> withSomeSing x fromSing) ≡ id

The final law can also be expressed in terms of the `FromSing` pattern synonym:

    (\(FromSing sing) -> FromSing sing) ≡ id

Associated Types

type Demote k = (r :: Type) | r -> k Source #

Get a base type from the promoted kind. For example, `Demote Bool` will be the type `Bool`. Rarely, the type and kind do not match. For example, `Demote Nat` is `Natural`.

Methods

fromSing :: Sing (a :: k) -> Demote k Source #

Convert a singleton to its unrefined version.

toSing :: Demote k -> SomeSing k Source #

Convert an unrefined type to an existentially-quantified singleton type.

#### Instances

Instances details

SingKind (WrappedSing a) Source # |
Instance details Defined in Data.Singletons Associated Types type Demote (WrappedSing a) = (r :: Type) Source # Methods fromSing :: forall (a0 :: WrappedSing a). Sing a0 -> Demote (WrappedSing a) Source # toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a) Source #
(SingKind k1, SingKind k2) => SingKind (k1 ~> k2) Source # | Note that this instance's `toSing` implementation crucially relies on the fact that the `SingKind` instances for `k1` and `k2` both satisfy the `SingKind` laws. If they don't, `toSing` might produce strange results!
Instance details Defined in Data.Singletons Associated Types type Demote (k1 ~> k2) = (r :: Type) Source # Methods fromSing :: forall (a :: k1 ~> k2). Sing a -> Demote (k1 ~> k2) Source # toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2) Source #

# Working with singletons

type KindOf (a :: k) = k Source #

Convenient synonym to refer to the kind of a type variable: `type KindOf (a :: k) = k`

type SameKind (a :: k) (b :: k) = () :: Constraint Source #

Force GHC to unify the kinds of `a` and `b`. Note that `SameKind a b` is different from `KindOf a ~ KindOf b` in that the former makes the kinds unify immediately, whereas the latter is a proposition that GHC considers as possibly false.

data SingInstance (a :: k) where Source #

A `SingInstance` wraps up a `SingI` instance for explicit handling.

Constructors

SingInstance :: SingI a => SingInstance a |

data SomeSing k where Source #

An existentially-quantified singleton. This type is useful when you want a singleton type, but there is no way of knowing, at compile-time, what the type index will be. To make use of this type, you will generally have to use a pattern-match:

    foo :: Bool -> ...
    foo b = case toSing b of
              SomeSing sb -> {- fancy dependently-typed code with sb -}

An example like the one above may be easier to write using `withSomeSing`.

Constructors

SomeSing :: Sing (a :: k) -> SomeSing k |

singInstance :: forall k (a :: k). Sing a -> SingInstance a Source #

Get an implicit singleton (a `SingI` instance) from an explicit one.

pattern Sing :: forall k (a :: k). () => SingI a => Sing a Source #

An explicitly bidirectional pattern synonym for implicit singletons.

As an expression: Constructs a singleton `Sing a` given a implicit singleton constraint `SingI a`.

As a pattern: Matches on an explicit `Sing a` witness bringing an implicit `SingI a` constraint into scope.

withSingI :: Sing n -> (SingI n => r) -> r Source #

Convenience function for creating a context with an implicit singleton available.

withSomeSing Source #

Arguments

:: forall k r. SingKind k |
=> Demote k | The original datatype
-> (forall (a :: k). Sing a -> r) | Function expecting a singleton
-> r |

Convert a normal datatype (like `Bool`) to a singleton for that datatype, passing it into a continuation.

pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k Source #

An explicitly bidirectional pattern synonym for going between a singleton and the corresponding demoted term.

As an expression: this takes a singleton to its demoted (base) type.

    >>> :t FromSing \@Bool
    FromSing \@Bool :: Sing a -> Bool
    >>> FromSing SFalse
    False

As a pattern: It extracts a singleton from its demoted (base) type.

    singAnd :: Bool -> Bool -> SomeSing Bool
    singAnd (FromSing singBool1) (FromSing singBool2) =
      SomeSing (singBool1 %&& singBool2)

instead of writing it with `withSomeSing`:

    singAnd bool1 bool2 =
      withSomeSing bool1 $ singBool1 ->
        withSomeSing bool2 $ singBool2 ->
          SomeSing (singBool1 %&& singBool2)

usingSingI1 :: forall f x r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r Source #

Convert a group of `SingI1` and `SingI` constraints (representing a function to apply and its argument, respectively) into a single `SingI` constraint representing the application. You will likely need the `ScopedTypeVariables` extension to use this method the way you want.

usingSingI2 :: forall f x y r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => r) -> r Source #

Convert a group of `SingI2` and `SingI` constraints (representing a function to apply and its arguments, respectively) into a single `SingI` constraint representing the application. You will likely need the `ScopedTypeVariables` extension to use this method the way you want.

singByProxy :: SingI a => proxy a -> Sing a Source #

Allows creation of a singleton when a proxy is at hand.

singByProxy1 :: (SingI1 f, SingI x) => proxy (f x) -> Sing (f x) Source #

Allows creation of a singleton for a unary type constructor when a proxy is at hand.

singByProxy2 :: (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y) Source #

Allows creation of a singleton for a binary type constructor when a proxy is at hand.

demote :: forall {k} (a :: k). (SingKind k, SingI a) => Demote k Source #

A convenience function that takes a type as input and demotes it to its value-level counterpart as output. This uses `SingKind` and `SingI` behind the scenes, so ``demote` = `fromSing` `sing``.

This function is intended to be used with `TypeApplications`. For example:

    >>> demote @True
    True

    >>> demote @(Nothing :: Maybe Ordering)
    Nothing

    >>> demote @(Just EQ)
    Just EQ

    >>> demote @'(True,EQ)
    (True,EQ)

demote1 :: forall {k1} {k2} (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => Demote k2 Source #

A convenience function that takes a unary type constructor and its argument as input, applies them, and demotes the result to its value-level counterpart as output. This uses `SingKind`, `SingI1`, and `SingI` behind the scenes, so ``demote1` = `fromSing` `sing1``.

This function is intended to be used with `TypeApplications`. For example:

    >>> demote1 @Just @EQ
    Just EQ

    >>> demote1 @('(,) True) @EQ
    (True,EQ)

demote2 :: forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => Demote k3 Source #

A convenience function that takes a binary type constructor and its arguments as input, applies them, and demotes the result to its value-level counterpart as output. This uses `SingKind`, `SingI2`, and `SingI` behind the scenes, so ``demote2` = `fromSing` `sing2``.

This function is intended to be used with `TypeApplications`. For example:

    >>> demote2 @'(,) @True @EQ
    (True,EQ)

singByProxy# :: SingI a => Proxy# a -> Sing a Source #

Allows creation of a singleton when a `proxy#` is at hand.

singByProxy1# :: (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x) Source #

Allows creation of a singleton for a unary type constructor when a `proxy#` is at hand.

singByProxy2# :: (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y) Source #

Allows creation of a singleton for a binary type constructor when a `proxy#` is at hand.

withSing :: SingI a => (Sing a -> b) -> b Source #

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 (often with `ScopedTypeVariables`) to ensure that they are the same.

withSing1 :: (SingI1 f, SingI x) => (Sing (f x) -> b) -> b Source #

A convenience function useful when we need to name a singleton value for a unary type constructor multiple times. Without this function, each use of `sing1` could potentially refer to a different singleton, and one has to use type signatures (often with `ScopedTypeVariables`) to ensure that they are the same.

withSing2 :: (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> b) -> b Source #

A convenience function useful when we need to name a singleton value for a binary type constructor multiple times. Without this function, each use of `sing1` could potentially refer to a different singleton, and one has to use type signatures (often with `ScopedTypeVariables`) to ensure that they are the same.

singThat :: forall k (a :: k). (SingKind k, SingI a) => (Demote k -> Bool) -> Maybe (Sing a) Source #

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.

singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => (Demote k2 -> Bool) -> Maybe (Sing (f x)) Source #

A convenience function that names a singleton for a unary type constructor 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.

singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => (Demote k3 -> Bool) -> Maybe (Sing (f x y)) Source #

A convenience function that names a singleton for a binary type constructor 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.

## `WrappedSing`

newtype WrappedSing :: forall k. k -> Type where Source #

A newtype around `Sing`.

Since `Sing` is a type family, it cannot be used directly in type class instances. As one example, one cannot write a catch-all `instance `SDecide` k => `TestEquality` (`Sing` k)`. On the other hand, `WrappedSing` is a perfectly ordinary data type, which means that it is quite possible to define an `instance `SDecide` k => `TestEquality` (`WrappedSing` k)`.

Constructors

WrapSing |

Fields

- :: forall k (a :: k). { unwrapSing :: Sing a
- } -> WrappedSing a

#### Instances

Instances details

SDecide k => TestCoercion (WrappedSing :: k -> Type) Source # |
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (Coercion a b) Source #
SDecide k => TestEquality (WrappedSing :: k -> Type) Source # |
Instance details Defined in Data.Singletons.Decide Methods testEquality :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (a :~: b) Source #
ShowSing k => Show (WrappedSing a) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> WrappedSing a -> ShowS Source # show :: WrappedSing a -> String Source # showList :: [WrappedSing a] -> ShowS Source #
SingKind (WrappedSing a) Source # |
Instance details Defined in Data.Singletons Associated Types type Demote (WrappedSing a) = (r :: Type) Source # Methods fromSing :: forall (a0 :: WrappedSing a). Sing a0 -> Demote (WrappedSing a) Source # toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a) Source #
SingI a => SingI ('WrapSing s :: WrappedSing a) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing ('WrapSing s) Source #
type Demote (WrappedSing a) Source # |
Instance details Defined in Data.Singletons type Demote (WrappedSing a) = WrappedSing a
type Sing Source # |
Instance details Defined in Data.Singletons type Sing = SWrappedSing :: WrappedSing a -> Type

newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where Source #

The singleton for `WrappedSing`s. Informally, this is the singleton type for other singletons.

Constructors

SWrapSing |

Fields

- :: forall k (a :: k) (ws :: WrappedSing a). { sUnwrapSing :: Sing a
- } -> SWrappedSing ws

#### Instances

Instances details

ShowSing k => Show (SWrappedSing ws) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SWrappedSing ws -> ShowS Source # show :: SWrappedSing ws -> String Source # showList :: [SWrappedSing ws] -> ShowS Source #

type family UnwrapSing (ws :: WrappedSing (a :: k)) :: Sing a where ... Source #

Equations

UnwrapSing ('WrapSing s) = s |

Aside from being a data type to hang instances off of, `WrappedSing` has another purpose as a general-purpose mechanism for allowing one to write code that uses singletons of other singletons. For instance, suppose you had the following data type:

    data T :: Type -> Type where
      MkT :: forall a (x :: a). Sing x -> F a -> T a

A naïve attempt at defining a singleton for `T` would look something like this:

    data ST :: forall a. T a -> Type where
      SMkT :: forall a (x :: a) (sx :: Sing x) (f :: F a).
              Sing sx -> Sing f -> ST (MkT sx f)

But there is a problem here: what exactly is ``Sing` sx`? If `x` were `True`, for instance, then `sx` would be `STrue`, but it's not clear what ``Sing` `STrue`` should be. One could define `SSBool` to be the singleton of `SBool`s, but in order to be thorough, one would have to generate a singleton for every singleton type out there. Plus, it's not clear when to stop. Should we also generate `SSSBool`, `SSSSBool`, etc.?

Instead, `WrappedSing` and its singleton `SWrappedSing` provide a way to talk about singletons of other arbitrary singletons without the need to generate a bazillion instances. For reference, here is the definition of `SWrappedSing`:

    newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where
      SWrapSing :: forall k (a :: k) (ws :: WrappedSing a).
                     { sUnwrapSing :: Sing a } -> SWrappedSing ws
    type instance Sing @(WrappedSing a) = SWrappedSing

`SWrappedSing` is a bit of an unusual singleton in that its field is a singleton for ``Sing` @k`, not ``WrappedSing` @k`. But that's exactly the point—a singleton of a singleton contains as much type information as the underlying singleton itself, so we can get away with just ``Sing` @k`.

As an example of this in action, here is how you would define the singleton for the earlier `T` type:

    data ST :: forall a. T a -> Type where
      SMkT :: forall a (x :: a) (sx :: Sing x) (f :: F a).
              Sing (WrapSing sx) -> Sing f -> ST (MkT sx f)

With this technique, we won't need anything like `SSBool` in order to instantiate `x` with `True`. Instead, the field of type ``Sing` (`WrapSing` sx)` will simply be a newtype around `SBool`. In general, you'll need n layers of `WrapSing` if you wish to single a singleton n times.

Note that this is not the only possible way to define a singleton for `T`. An alternative approach that does not make use of singletons-of-singletons is discussed at some length here. Due to the technical limitations of this approach, however, we do not use it in `singletons` at the moment, instead favoring the slightly-clunkier-but-more-reliable `WrappedSing` approach.

## Defunctionalization

data TyFun :: Type -> Type -> Type Source #

Representation of the kind of a type-level function. The difference between term-level arrows and this type-level arrow is that at the term level applications can be unsaturated, whereas at the type level all applications have to be fully saturated.

#### Instances

Instances details

(SingKind k1, SingKind k2) => SingKind (k1 ~> k2) Source # | Note that this instance's `toSing` implementation crucially relies on the fact that the `SingKind` instances for `k1` and `k2` both satisfy the `SingKind` laws. If they don't, `toSing` might produce strange results!
Instance details Defined in Data.Singletons Associated Types type Demote (k1 ~> k2) = (r :: Type) Source # Methods fromSing :: forall (a :: k1 ~> k2). Sing a -> Demote (k1 ~> k2) Source # toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2) Source #
(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> TyFun k1 kr -> Type) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: TyFun k1 kr -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon1 f) Source #
(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> TyFun k2 kr -> Type) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: TyFun k1 (k2 ~> kr) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon2 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> TyFun k3 kr -> Type) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: TyFun k1 (k2 ~> (k3 ~> kr)) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon3 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> TyFun k4 kr -> Type) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> kr))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon4 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> TyFun k5 kr -> Type) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon5 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> TyFun k6 kr -> Type) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon6 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> TyFun k7 kr -> Type) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon7 f) Source #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> TyFun k8 kr -> Type) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))) -> Type) Source #

Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon8 f) Source #
type Apply (TyCon f :: k1 ~> k5) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply (TyCon f :: k1 ~> k5) (x :: k1) = ApplyTyCon f @@ x
type Apply (~>@#@$) (x :: Type) Source # |
Instance details Defined in Data.Singletons type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x
type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) Source # |
Instance details Defined in Data.Singletons type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x
type Demote (k1 ~> k2) Source # |
Instance details Defined in Data.Singletons type Demote (k1 ~> k2) = Demote k1 -> Demote k2
type Sing Source # |
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) Source # |
Instance details Defined in Data.Singletons type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = (@@@#@$$) f
type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) Source # |
Instance details Defined in Data.Singletons type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = ApplySym1 f

type (~>) a b = TyFun a b -> Type infixr 0 Source #

Something of kind `a `~>` b` is a defunctionalized type function that is not necessarily generative or injective. Defunctionalized type functions (also called "defunctionalization symbols") can be partially applied, even if the original type function cannot be. For more information on how this works, see the "Promotion and partial application" section of the `README`.

Normal type-level arrows `(->)` can be converted into defunctionalization arrows `(`~>`)` by the use of the `TyCon` family of types. (Refer to the Haddocks for `TyCon1` to see an example of this in practice.) For this reason, we do not make an effort to define defunctionalization symbols for most type constructors of kind `a -> b`, as they can be used in defunctionalized settings by simply applying `TyCon{N}` with an appropriate `N`.

This includes the `(->)` type constructor itself, which is of kind ``Type` -> `Type` -> `Type``. One can turn it into something of kind ``Type` `~>` `Type` `~>` `Type`` by writing ``TyCon2` (->)`, or something of kind ``Type` -> `Type` `~>` `Type`` by writing ``TyCon1` ((->) t)` (where `t :: `Type``).

type TyCon1 = TyCon :: (k1 -> k2) -> k1 ~> k2 Source #

Wrapper for converting the normal type-level arrow into a `~>`. For example, given:

    data Nat = Zero | Succ Nat
    type family Map (a :: a ~> b) (a :: [a]) :: [b]
      Map f '[] = '[]
      Map f (x ': xs) = Apply f x ': Map f xs

We can write:

    Map (TyCon1 Succ) [Zero, Succ Zero]

type TyCon2 = TyCon :: (k1 -> k2 -> k3) -> k1 ~> (k2 ~> k3) Source #

Similar to `TyCon1`, but for two-parameter type constructors.

type TyCon3 = TyCon :: (k1 -> k2 -> k3 -> k4) -> k1 ~> (k2 ~> (k3 ~> k4)) Source #

type TyCon4 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> k5))) Source #

type TyCon5 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> k6)))) Source #

type TyCon6 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> k7))))) Source #

type TyCon7 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> k8)))))) Source #

type TyCon8 = TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> k9))))))) Source #

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 Source #

Type level function application

#### Instances

Instances details

type Apply DemoteSym0 (x :: Type) Source # |
Instance details Defined in Data.Singletons type Apply DemoteSym0 (x :: Type) = Demote x
type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) Source # |
Instance details Defined in Data.Singletons type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y
type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) Source # |
Instance details Defined in Data.Singletons type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) = KindOf x
type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k) Source # |
Instance details Defined in Data.Singletons type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k) = SameKind x y
type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1) = f @@ x
type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1) = Apply f x
type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x
type Apply (TyCon f :: k1 ~> k5) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply (TyCon f :: k1 ~> k5) (x :: k1) = ApplyTyCon f @@ x
type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) Source # |
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) = TyCon (f x)
type Apply (~>@#@$) (x :: Type) Source # |
Instance details Defined in Data.Singletons type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x
type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) Source # |
Instance details Defined in Data.Singletons type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x
type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) Source # |
Instance details Defined in Data.Singletons type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = (@@@#@$$) f
type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) Source # |
Instance details Defined in Data.Singletons type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = ApplySym1 f

type (@@) a b = Apply a b infixl 9 Source #

An infix synonym for `Apply`

data family TyCon :: (k1 -> k2) -> unmatchable_fun Source #

Workhorse for the `TyCon1`, etc., types. This can be used directly in place of any of the `TyConN` types, but it will work only with monomorphic types. When GHC#14645 is fixed, this should fully supersede the `TyConN` types.

Note that this is only defined on GHC 8.6 or later. Prior to GHC 8.6, `TyCon1` et al. were defined as separate data types.

#### Instances

Instances details

(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> TyFun k1 kr -> Type) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: TyFun k1 kr -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon1 f) Source #
(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> TyFun k2 kr -> Type) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: TyFun k1 (k2 ~> kr) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon2 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> TyFun k3 kr -> Type) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: TyFun k1 (k2 ~> (k3 ~> kr)) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon3 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> TyFun k4 kr -> Type) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> kr))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon4 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> TyFun k5 kr -> Type) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon5 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> TyFun k6 kr -> Type) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon6 f) Source #
(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> TyFun k7 kr -> Type) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))) -> Type) Source # |
Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon7 f) Source #

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> TyFun k8 kr -> Type) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: TyFun k1 (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))) -> Type) Source #

Instance details Defined in Data.Singletons Methods sing :: Sing (TyCon8 f) Source #
type Apply (TyCon f :: k1 ~> k5) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply (TyCon f :: k1 ~> k5) (x :: k1) = ApplyTyCon f @@ x

type family ApplyTyCon :: (k1 -> k2) -> k1 ~> unmatchable_fun where ... Source #

An "internal" definition used primary in the `Apply` instance for `TyCon`.

Note that this only defined on GHC 8.6 or later.

Equations

ApplyTyCon @k1 @(k2 -> k3) @unmatchable_fun = ApplyTyConAux2 |
ApplyTyCon @k1 @k2 @k2 = ApplyTyConAux1 |

data ApplyTyConAux1 :: (k1 -> k2) -> k1 ~> k2 Source #

An "internal" defunctionalization symbol used primarily in the definition of `ApplyTyCon`, as well as the `SingI` instances for `TyCon1`, `TyCon2`, etc.

Note that this is only defined on GHC 8.6 or later.

#### Instances

Instances details

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x

data ApplyTyConAux2 :: (k1 -> k2 -> k3) -> k1 ~> unmatchable_fun Source #

An "internal" defunctionalization symbol used primarily in the definition of `ApplyTyCon`.

Note that this is only defined on GHC 8.6 or later.

#### Instances

Instances details

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) Source # |
Instance details Defined in Data.Singletons type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) = TyCon (f x)

## Defunctionalized singletons

When calling a higher-order singleton function, you need to use a `singFun...` function to wrap it. See `singFun1`.

singFun1 :: forall f. SingFunction1 f -> Sing f Source #

Use this function when passing a function on singletons as a higher-order function. You will need visible type application to get this to work. For example:

    falses = sMap (singFun1 @NotSym0 sNot)
                  (STrue `SCons` STrue `SCons` SNil)

There are a family of `singFun...` functions, keyed by the number of parameters of the function.

singFun2 :: forall f. SingFunction2 f -> Sing f Source #

singFun3 :: forall f. SingFunction3 f -> Sing f Source #

singFun4 :: forall f. SingFunction4 f -> Sing f Source #

singFun5 :: forall f. SingFunction5 f -> Sing f Source #

singFun6 :: forall f. SingFunction6 f -> Sing f Source #

singFun7 :: forall f. SingFunction7 f -> Sing f Source #

singFun8 :: forall f. SingFunction8 f -> Sing f Source #

unSingFun1 :: forall f. Sing f -> SingFunction1 f Source #

This is the inverse of `singFun1`, and likewise for the other `unSingFun...` functions.

unSingFun2 :: forall f. Sing f -> SingFunction2 f Source #

unSingFun3 :: forall f. Sing f -> SingFunction3 f Source #

unSingFun4 :: forall f. Sing f -> SingFunction4 f Source #

unSingFun5 :: forall f. Sing f -> SingFunction5 f Source #

unSingFun6 :: forall f. Sing f -> SingFunction6 f Source #

unSingFun7 :: forall f. Sing f -> SingFunction7 f Source #

unSingFun8 :: forall f. Sing f -> SingFunction8 f Source #

`SLambda{2...8}` are explicitly bidirectional pattern synonyms for defunctionalized singletons (``Sing` (f :: k `~>` k' `~>` k'')`).

As constructors: Same as `singFun{2..8}`. For example, one can turn a binary function on singletons `sTake :: `SingFunction2` TakeSym0` into a defunctionalized singleton ``Sing` (TakeSym :: Nat `~>` [a] `~>` [a])`:

    >>> import Data.List.Singletons
    >>> :set -XTypeApplications
    >>>
    >>> :t SLambda2
    SLambda2 :: SingFunction2 f -> Sing f
    >>> :t SLambda2 @TakeSym0
    SLambda2 :: SingFunction2 TakeSym0 -> Sing TakeSym0
    >>> :t SLambda2 @TakeSym0 sTake
    SLambda2 :: Sing TakeSym0

This is useful for functions on singletons that expect a defunctionalized singleton as an argument, such as `sZipWith :: `SingFunction3` ZipWithSym0`:

    sZipWith :: Sing (f :: a ~> b ~> c) -> Sing (xs :: [a]) -> Sing (ys :: [b]) -> Sing (ZipWith f xs ys :: [c])
    sZipWith (SLambda2 @TakeSym0 sTake) :: Sing (xs :: [Nat]) -> Sing (ys :: [[a]]) -> Sing (ZipWith TakeSym0 xs ys :: [[a]])

As patterns: Same as `unSingFun{2..8}`. Gets a binary term-level Haskell function on singletons ``Sing` (x :: k) -> `Sing` (y :: k') -> `Sing` (f @@ x @@ y)` from a defunctionalised ``Sing` f`. Alternatively, as a record field accessor:

    applySing2 :: Sing (f :: k ~> k' ~> k'') -> SingFunction2 f

pattern SLambda2 :: forall f. SingFunction2 f -> Sing f Source #

applySing2 :: forall {a1} {a2} {b} (f :: a1 ~> (a2 ~> b)). Sing f -> SingFunction2 f Source #

pattern SLambda3 :: forall f. SingFunction3 f -> Sing f Source #

applySing3 :: forall {a1} {a2} {a3} {b} (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> SingFunction3 f Source #

pattern SLambda4 :: forall f. SingFunction4 f -> Sing f Source #

applySing4 :: forall {a1} {a2} {a3} {a4} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> SingFunction4 f Source #

pattern SLambda5 :: forall f. SingFunction5 f -> Sing f Source #

applySing5 :: forall {a1} {a2} {a3} {a4} {a5} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> SingFunction5 f Source #

pattern SLambda6 :: forall f. SingFunction6 f -> Sing f Source #

applySing6 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> SingFunction6 f Source #

pattern SLambda7 :: forall f. SingFunction7 f -> Sing f Source #

applySing7 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> SingFunction7 f Source #

pattern SLambda8 :: forall f. SingFunction8 f -> Sing f Source #

applySing8 :: forall {a1} {a2} {a3} {a4} {a5} {a6} {a7} {a8} {b} (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> SingFunction8 f Source #

These type synonyms are exported only to improve error messages; users should not have to mention them.

type SingFunction1 (f :: a1 ~> b) = forall t. Sing t -> Sing (f @@ t) Source #

type SingFunction2 (f :: a1 ~> (a2 ~> b)) = forall t1 t2. Sing t1 -> Sing t2 -> Sing ((f @@ t1) @@ t2) Source #

type SingFunction3 (f :: a1 ~> (a2 ~> (a3 ~> b))) = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (((f @@ t1) @@ t2) @@ t3) Source #

type SingFunction4 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))) = forall t1 t2 t3 t4. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing ((((f @@ t1) @@ t2) @@ t3) @@ t4) Source #

type SingFunction5 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))) = forall t1 t2 t3 t4 t5. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing (((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) Source #

type SingFunction6 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))) = forall t1 t2 t3 t4 t5 t6. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing ((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) Source #

type SingFunction7 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))) = forall t1 t2 t3 t4 t5 t6 t7. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing (((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7) Source #

type SingFunction8 (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))) = forall t1 t2 t3 t4 t5 t6 t7 t8. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8 -> Sing ((((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7) @@ t8) Source #

# Auxiliary functions

data Proxy (t :: k) Source #

`Proxy` is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, ``Proxy` :: `Proxy` a` is a safer alternative to the ``undefined` :: a` idiom.

    >>> Proxy :: Proxy (Void, Int -> Int)
    Proxy

Proxy can even hold types of higher kinds,

    >>> Proxy :: Proxy Either
    Proxy

    >>> Proxy :: Proxy Functor
    Proxy

    >>> Proxy :: Proxy complicatedStructure
    Proxy

Constructors

Proxy |

#### Instances

Instances details

Generic1 (Proxy :: k -> Type) |
Instance details Defined in GHC.Generics Associated Types type Rep1 Proxy :: k -> Type Source # Methods from1 :: forall (a :: k0). Proxy a -> Rep1 Proxy a Source # to1 :: forall (a :: k0). Rep1 Proxy a -> Proxy a Source #
Foldable (Proxy :: Type -> Type) | Since: base-4.7.0.0

Instance details

Defined in Data.Foldable

Methods

fold :: Monoid m => Proxy m -> m Source #

foldMap :: Monoid m => (a -> m) -> Proxy a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Proxy a -> m Source #

foldr :: (a -> b -> b) -> b -> Proxy a -> b Source #

foldr' :: (a -> b -> b) -> b -> Proxy a -> b Source #

foldl :: (b -> a -> b) -> b -> Proxy a -> b Source #

foldl' :: (b -> a -> b) -> b -> Proxy a -> b Source #

foldr1 :: (a -> a -> a) -> Proxy a -> a Source #

foldl1 :: (a -> a -> a) -> Proxy a -> a Source #

toList :: Proxy a -> [a] Source #

null :: Proxy a -> Bool Source #

length :: Proxy a -> Int Source #

elem :: Eq a => a -> Proxy a -> Bool Source #

maximum :: Ord a => Proxy a -> a Source #

minimum :: Ord a => Proxy a -> a Source #

sum :: Num a => Proxy a -> a Source #

product :: Num a => Proxy a -> a Source #

Traversable (Proxy :: Type -> Type) | Since: base-4.7.0.0
Instance details Defined in Data.Traversable Methods traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b) Source # sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a) Source # mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b) Source # sequence :: Monad m => Proxy (m a) -> m (Proxy a) Source #
Alternative (Proxy :: Type -> Type) | Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods empty :: Proxy a Source # (<|>) :: Proxy a -> Proxy a -> Proxy a Source # some :: Proxy a -> Proxy [a] Source # many :: Proxy a -> Proxy [a] Source #
Applicative (Proxy :: Type -> Type) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods pure :: a -> Proxy a Source # (<*>) :: Proxy (a -> b) -> Proxy a -> Proxy b Source # liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c Source # (*>) :: Proxy a -> Proxy b -> Proxy b Source # (<*) :: Proxy a -> Proxy b -> Proxy a Source #
Functor (Proxy :: Type -> Type) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods fmap :: (a -> b) -> Proxy a -> Proxy b Source # (<$) :: a -> Proxy b -> Proxy a Source #
Monad (Proxy :: Type -> Type) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b Source # (>>) :: Proxy a -> Proxy b -> Proxy b Source # return :: a -> Proxy a Source #
MonadPlus (Proxy :: Type -> Type) | Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods mzero :: Proxy a Source # mplus :: Proxy a -> Proxy a -> Proxy a Source #
Monoid (Proxy s) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods mempty :: Proxy s Source # mappend :: Proxy s -> Proxy s -> Proxy s Source # mconcat :: [Proxy s] -> Proxy s Source #
Semigroup (Proxy s) | Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods (<>) :: Proxy s -> Proxy s -> Proxy s Source # sconcat :: NonEmpty (Proxy s) -> Proxy s Source # stimes :: Integral b => b -> Proxy s -> Proxy s Source #
Bounded (Proxy t) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods minBound :: Proxy t Source # maxBound :: Proxy t Source #
Enum (Proxy s) | Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

succ :: Proxy s -> Proxy s Source #

pred :: Proxy s -> Proxy s Source #

toEnum :: Int -> Proxy s Source #

fromEnum :: Proxy s -> Int Source #

enumFrom :: Proxy s -> [Proxy s] Source #

enumFromThen :: Proxy s -> Proxy s -> [Proxy s] Source #

enumFromTo :: Proxy s -> Proxy s -> [Proxy s] Source #

enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s] Source #

Generic (Proxy t) |
Instance details Defined in GHC.Generics Associated Types type Rep (Proxy t) :: Type -> Type Source # Methods from :: Proxy t -> Rep (Proxy t) x Source # to :: Rep (Proxy t) x -> Proxy t Source #
Ix (Proxy s) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods range :: (Proxy s, Proxy s) -> [Proxy s] Source # index :: (Proxy s, Proxy s) -> Proxy s -> Int Source # unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int Source # inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool Source # rangeSize :: (Proxy s, Proxy s) -> Int Source # unsafeRangeSize :: (Proxy s, Proxy s) -> Int Source #
Read (Proxy t) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods readsPrec :: Int -> ReadS (Proxy t) Source # readList :: ReadS [Proxy t] Source # readPrec :: ReadPrec (Proxy t) Source # readListPrec :: ReadPrec [Proxy t] Source #
Show (Proxy s) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods showsPrec :: Int -> Proxy s -> ShowS Source # show :: Proxy s -> String Source # showList :: [Proxy s] -> ShowS Source #
Eq (Proxy s) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (==) :: Proxy s -> Proxy s -> Bool Source # (/=) :: Proxy s -> Proxy s -> Bool Source #
Ord (Proxy s) | Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods compare :: Proxy s -> Proxy s -> Ordering Source # (<) :: Proxy s -> Proxy s -> Bool Source # (<=) :: Proxy s -> Proxy s -> Bool Source # (>) :: Proxy s -> Proxy s -> Bool Source # (>=) :: Proxy s -> Proxy s -> Bool Source # max :: Proxy s -> Proxy s -> Proxy s Source # min :: Proxy s -> Proxy s -> Proxy s Source #
type Rep1 (Proxy :: k -> Type) | Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep1 (Proxy :: k -> Type) = D1 ('MetaData "Proxy" "Data.Proxy" "base" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: k -> Type))
type Rep (Proxy t) | Since: base-4.6.0.0
Instance details Defined in GHC.Generics type Rep (Proxy t) = D1 ('MetaData "Proxy" "Data.Proxy" "base" 'False) (C1 ('MetaCons "Proxy" 'PrefixI 'False) (U1 :: Type -> Type))

# Defunctionalization symbols

data DemoteSym0 :: Type ~> Type Source #

#### Instances

Instances details

type Apply DemoteSym0 (x :: Type) Source # |
Instance details Defined in Data.Singletons type Apply DemoteSym0 (x :: Type) = Demote x

type DemoteSym1 x = Demote x Source #

data SameKindSym0 :: forall k. k ~> (k ~> Constraint) Source #

#### Instances

Instances details

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) Source # |
Instance details Defined in Data.Singletons type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x

data SameKindSym1 :: forall k. k -> k ~> Constraint Source #

#### Instances

Instances details

type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k) Source # |
Instance details Defined in Data.Singletons type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k) = SameKind x y

type SameKindSym2 (x :: k) (y :: k) = SameKind x y Source #

data KindOfSym0 :: forall k. k ~> Type Source #

#### Instances

Instances details

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) Source # |
Instance details Defined in Data.Singletons type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) = KindOf x

type KindOfSym1 (x :: k) = KindOf x Source #

data (~>@#@$) :: Type ~> (Type ~> Type) infixr 0 Source #

#### Instances

Instances details

type Apply (~>@#@$) (x :: Type) Source # |
Instance details Defined in Data.Singletons type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

data (~>@#@$$) :: Type -> Type ~> Type infixr 0 Source #

#### Instances

Instances details

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) Source # |
Instance details Defined in Data.Singletons type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y

type (~>@#@$$$) x y = x ~> y infixr 0 Source #

data ApplySym0 :: forall a b. (a ~> b) ~> (a ~> b) Source #

#### Instances

Instances details

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) Source # |
Instance details Defined in Data.Singletons type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = ApplySym1 f

data ApplySym1 :: forall a b. (a ~> b) -> a ~> b Source #

#### Instances

Instances details

type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1) = Apply f x

type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x Source #

data (@@@#@$) :: forall a b. (a ~> b) ~> (a ~> b) infixl 9 Source #

#### Instances

Instances details

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) Source # |
Instance details Defined in Data.Singletons type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b) = (@@@#@$$) f

data (@@@#@$$) :: forall a b. (a ~> b) -> a ~> b infixl 9 Source #

#### Instances

Instances details

type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1) Source # |
Instance details Defined in Data.Singletons type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1) = f @@ x

type (@@@#@$$$) (f :: a ~> b) (x :: a) = f @@ x infixl 9 Source #