Safe Haskell	Safe-Inferred
Language	Haskell2010

Ouroboros.Consensus.Util.Singletons

Description

Singletons

This provides the core of the singletons package, using the same name, but without pulling in all the dependencies and craziness.

Synopsis

data family Sing (a ∷ k)
class SingI (a ∷ k) where
- sing ∷ Sing a
class SingKind k where
- type Demote k = (r ∷ Type) | r → k
- fromSing ∷ Sing (a ∷ k) → Demote k
- toSing ∷ Demote k → SomeSing k
data SomeSing k where
- SomeSing ∷ Sing (a ∷ k) → SomeSing k
withSomeSing ∷ ∀ k r. SingKind k ⇒ Demote k → (∀ (a ∷ k). Sing a → r) → r

Documentation

data family Sing (a ∷ k) Source #

Data family of singletons

Instances details

data Sing (xs ∷ [k]) Source #

Singletons for lists

NOTE: Unlike the singletons library, we do not require instances for the elements of the list.

Instance details

data Sing (xs ∷ [k]) where

class SingI (a ∷ k) where Source #

Methods

Instances details

SingI ('[] ∷ [k]) Source #
Instance details Defined in Ouroboros.Consensus.Util.Singletons Methods sing ∷ Sing '[] Source #
SingI xs ⇒ SingI (x ': xs ∷ [a]) Source #
Instance details Defined in Ouroboros.Consensus.Util.Singletons Methods sing ∷ Sing (x ': xs) Source #

class SingKind k where Source #

Associated Types

type Demote k = (r ∷ Type) | r → k Source #

Methods

Constructors

SomeSing ∷ Sing (a ∷ k) → SomeSing k

withSomeSing ∷ ∀ k r. SingKind k ⇒ Demote k → (∀ (a ∷ k). Sing a → r) → r Source #