Data.Singletons

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.

Main singleton definitions

type family Sing :: k -> Type

The singleton kind-indexed type family.

Instances

type Sing

Defined in Data.Singletons

type Sing = SWrappedSing :: WrappedSing a -> Type

type Sing

Defined in Data.Singletons

type Sing = SLambda :: (k1 ~> k2) -> Type

type Sing

Defined in Data.Singletons.Sigma

type Sing = SSigma :: Sigma s t -> Type

newtype SLambda (f :: k1 ~> k2)

The singleton type for functions. Functions have somewhat special treatment in singletons (see the Haddocks for (~>) for more information about this), and as a result, the Sing instance for SLambda is one of the only such instances defined in the singletons library rather than, say, singletons-base.

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

An infix synonym for applySing

class SingI a where

A SingI constraint is essentially an implicitly-passed singleton.

In contrast to the SingKind class, which is parameterized over data types promoted to the kind level, the SingI class is parameterized over values promoted to the type level. To explain this distinction another way, consider this code:

f = fromSing (sing @(T :: K))

Here, f uses methods from both SingI and SingKind. However, the shape of each constraint is rather different: using sing requires a 'SingI T' constraint, whereas using fromSing requires a 'SingKind K' constraint.

If you need to satisfy this constraint with an explicit singleton, please see withSingI or the Sing pattern synonym.

Methods

sing :: Sing a

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

Instances

SingI a => SingI ('WrapSing s :: WrappedSing a)

Defined in Data.Singletons

Methods

sing :: Sing ('WrapSing s)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f)

(SingI fst, SingI b) => SingI (a ':&: b :: Sigma s t)

Defined in Data.Singletons.Sigma

Methods

sing :: Sing (a ':&: b)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f)

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

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

Methods

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

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)

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

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

Methods

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

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)

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

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

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

Convert a singleton to its unrefined version.

toSing :: Demote k -> SomeSing k

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

Instances

SingKind (WrappedSing a)

Defined in Data.Singletons

Associated Types

type Demote (WrappedSing a) = (r :: Type)

Methods

fromSing :: forall (a0 :: WrappedSing a). Sing a0 -> Demote (WrappedSing a)

toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a)

(SingKind k1, SingKind k2) => SingKind (k1 ~> k2)

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!

Defined in Data.Singletons

Associated Types

type Demote (k1 ~> k2) = (r :: Type)

Methods

fromSing :: forall (a :: k1 ~> k2). Sing a -> Demote (k1 ~> k2)

toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2)

Working with singletons

type KindOf (a :: k) = k

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

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

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

A SingInstance wraps up a SingI instance for explicit handling.

Constructors

SingInstance :: SingI a => SingInstance a

data SomeSing k where

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

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

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

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

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

withSomeSing

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

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

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

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

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

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

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)

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

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

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

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

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

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

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)

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

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

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

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

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)

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))

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))

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

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

SDecide k => TestCoercion (WrappedSing :: k -> Type)

Defined in Data.Singletons.Decide

Methods

testCoercion :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (Coercion a b)

SDecide k => TestEquality (WrappedSing :: k -> Type)

Defined in Data.Singletons.Decide

Methods

testEquality :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (a :~: b)

ShowSing k => Show (WrappedSing a)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> WrappedSing a -> ShowS

show :: WrappedSing a -> String

showList :: [WrappedSing a] -> ShowS

SingKind (WrappedSing a)

Defined in Data.Singletons

Associated Types

type Demote (WrappedSing a) = (r :: Type)

Methods

fromSing :: forall (a0 :: WrappedSing a). Sing a0 -> Demote (WrappedSing a)

toSing :: Demote (WrappedSing a) -> SomeSing (WrappedSing a)

SingI a => SingI ('WrapSing s :: WrappedSing a)

Defined in Data.Singletons

Methods

sing :: Sing ('WrapSing s)

type Demote (WrappedSing a)

Defined in Data.Singletons

type Demote (WrappedSing a) = WrappedSing a

type Sing

Defined in Data.Singletons

type Sing = SWrappedSing :: WrappedSing a -> Type

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

The singleton for WrappedSings. 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

ShowSing k => Show (SWrappedSing ws)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> SWrappedSing ws -> ShowS

show :: SWrappedSing ws -> String

showList :: [SWrappedSing ws] -> ShowS

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

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 SBools, 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

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

(SingKind k1, SingKind k2) => SingKind (k1 ~> k2)

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!

Defined in Data.Singletons

Associated Types

type Demote (k1 ~> k2) = (r :: Type)

Methods

fromSing :: forall (a :: k1 ~> k2). Sing a -> Demote (k1 ~> k2)

toSing :: Demote (k1 ~> k2) -> SomeSing (k1 ~> k2)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f)

type Apply (TyCon f :: k1 ~> k5) (x :: k1)

Defined in Data.Singletons

type Apply (TyCon f :: k1 ~> k5) (x :: k1) = ApplyTyCon f @@ x

type Apply (~>@#@$) (x :: Type)

Defined in Data.Singletons

type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)

Defined in Data.Singletons

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x

type Demote (k1 ~> k2)

Defined in Data.Singletons

type Demote (k1 ~> k2) = Demote k1 -> Demote k2

type Sing

Defined in Data.Singletons

type Sing = SLambda :: (k1 ~> k2) -> Type

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

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)

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

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.

The singleton for things of kind a ~> b is SLambda. SLambda values can be constructed in one of two ways:

1. With the singFun* family of combinators (e.g., singFun1). For example, if you have:

   type Id :: a -> a
   sId :: Sing a -> Sing (Id a)
   

Then you can construct a value of type Sing @(a ~> a) (that is, SLambda @a @a like so:

   sIdFun :: Sing @(a ~> a) IdSym0
   sIdFun = singFun1 @IdSym0 sId
   

Where IdSym0 :: a ~> a is the defunctionlized version of Id.

2. Using the SingI class. For example, sing @IdSym0 is another way of defining sIdFun above. The singletons-th library automatically generates SingI instances for defunctionalization symbols such as IdSym0.

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

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)

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

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 level function application

Instances

type Apply DemoteSym0 (x :: Type)

Defined in Data.Singletons

type Apply DemoteSym0 (x :: Type) = Demote x

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type)

Defined in Data.Singletons

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k)

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)

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)

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)

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)

Defined in Data.Singletons

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x

type Apply (TyCon f :: k1 ~> k5) (x :: k1)

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)

Defined in Data.Singletons

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4) = TyCon (f x)

type Apply (~>@#@$) (x :: Type)

Defined in Data.Singletons

type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)

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)

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)

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

An infix synonym for Apply

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

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

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f)

(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)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f)

type Apply (TyCon f :: k1 ~> k5) (x :: k1)

Defined in Data.Singletons

type Apply (TyCon f :: k1 ~> k5) (x :: k1) = ApplyTyCon f @@ x

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

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

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

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1)

Defined in Data.Singletons

type Apply (ApplyTyConAux1 f :: TyFun k1 k2 -> Type) (x :: k1) = f x

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

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

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

Instances

type Apply (ApplyTyConAux2 f :: TyFun k4 k7 -> Type) (x :: k4)

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

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

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

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

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

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

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

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)

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)

Auxiliary functions

data Proxy (t :: k)

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

Foldable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Foldable

Methods

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

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

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

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

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

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

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

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

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

toList :: Proxy a -> [a]

null :: Proxy a -> Bool

length :: Proxy a -> Int

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

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

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

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

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

Traversable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Traversable

Methods

traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b)

sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a)

mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b)

sequence :: Monad m => Proxy (m a) -> m (Proxy a)

Alternative (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

empty :: Proxy a

(<|>) :: Proxy a -> Proxy a -> Proxy a

some :: Proxy a -> Proxy [a]

many :: Proxy a -> Proxy [a]

Applicative (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

pure :: a -> Proxy a

(<*>) :: Proxy (a -> b) -> Proxy a -> Proxy b

liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c

(*>) :: Proxy a -> Proxy b -> Proxy b

(<*) :: Proxy a -> Proxy b -> Proxy a

Functor (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

fmap :: (a -> b) -> Proxy a -> Proxy b

(<$) :: a -> Proxy b -> Proxy a

Monad (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b

(>>) :: Proxy a -> Proxy b -> Proxy b

return :: a -> Proxy a

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

mzero :: Proxy a

mplus :: Proxy a -> Proxy a -> Proxy a

Monoid (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

mempty :: Proxy s

mappend :: Proxy s -> Proxy s -> Proxy s

mconcat :: [Proxy s] -> Proxy s

Semigroup (Proxy s)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

(<>) :: Proxy s -> Proxy s -> Proxy s

sconcat :: NonEmpty (Proxy s) -> Proxy s

stimes :: Integral b => b -> Proxy s -> Proxy s

Bounded (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

minBound :: Proxy t

maxBound :: Proxy t

Enum (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

succ :: Proxy s -> Proxy s

pred :: Proxy s -> Proxy s

toEnum :: Int -> Proxy s

fromEnum :: Proxy s -> Int

enumFrom :: Proxy s -> [Proxy s]

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

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

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

Ix (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

range :: (Proxy s, Proxy s) -> [Proxy s]

index :: (Proxy s, Proxy s) -> Proxy s -> Int

unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int

inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool

rangeSize :: (Proxy s, Proxy s) -> Int

unsafeRangeSize :: (Proxy s, Proxy s) -> Int

Read (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

readsPrec :: Int -> ReadS (Proxy t)

readList :: ReadS [Proxy t]

readPrec :: ReadPrec (Proxy t)

readListPrec :: ReadPrec [Proxy t]

Show (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

showsPrec :: Int -> Proxy s -> ShowS

show :: Proxy s -> String

showList :: [Proxy s] -> ShowS

Eq (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(==) :: Proxy s -> Proxy s -> Bool

(/=) :: Proxy s -> Proxy s -> Bool

Ord (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

compare :: Proxy s -> Proxy s -> Ordering

(<) :: Proxy s -> Proxy s -> Bool

(<=) :: Proxy s -> Proxy s -> Bool

(>) :: Proxy s -> Proxy s -> Bool

(>=) :: Proxy s -> Proxy s -> Bool

max :: Proxy s -> Proxy s -> Proxy s

min :: Proxy s -> Proxy s -> Proxy s

Defunctionalization symbols

data DemoteSym0 :: Type ~> Type

Instances

type Apply DemoteSym0 (x :: Type)

Defined in Data.Singletons

type Apply DemoteSym0 (x :: Type) = Demote x

type DemoteSym1 x = Demote x

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

Instances

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k)

Defined in Data.Singletons

type Apply (SameKindSym0 :: TyFun k (k ~> Constraint) -> Type) (x :: k) = SameKindSym1 x

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

Instances

type Apply (SameKindSym1 x :: TyFun k Constraint -> Type) (y :: k)

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

data KindOfSym0 :: forall k. k ~> Type

Instances

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k)

Defined in Data.Singletons

type Apply (KindOfSym0 :: TyFun k Type -> Type) (x :: k) = KindOf x

type KindOfSym1 (x :: k) = KindOf x

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

Instances

type Apply (~>@#@$) (x :: Type)

Defined in Data.Singletons

type Apply (~>@#@$) (x :: Type) = (~>@#@$$) x

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

Instances

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type)

Defined in Data.Singletons

type Apply ((~>@#@$$) x :: TyFun Type Type -> Type) (y :: Type) = x ~> y

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

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

Instances

type Apply (ApplySym0 :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

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

Instances

type Apply (ApplySym1 f :: TyFun k1 k2 -> Type) (x :: k1)

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

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

Instances

type Apply ((@@@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (f :: a ~> b)

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

Instances

type Apply ((@@@#@$$) f :: TyFun k1 k2 -> Type) (x :: k1)

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