Data.Singletons

The singleton kind-indexed type family.

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.

An infix synonym for applySing

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.

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

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.

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

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.

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

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

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.

A SingInstance wraps up a SingI instance for explicit handling.

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.

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

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.

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

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

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 \@BoolFromSing \@Bool :: Sing a -> Bool>>> FromSing SFalseFalse

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)

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.

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.

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

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

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

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 @TrueTrue

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

>>> demote @(Just EQ)Just EQ

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

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 @EQJust EQ

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

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)

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

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

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

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.

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.

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.

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.

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.

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.

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 EitherProxy

>>> Proxy :: Proxy FunctorProxy

>>> Proxy :: Proxy complicatedStructureProxy