Data.Type.Combinator.Singletons

There's a lot of identical data types between type-combinators and singetons, as well as similar typeclasses. This module provides conversion functions between the two, and also many appropriate instances.

Documentation

prodSing :: Prod Sing as -> Sing as

Convert a Prod of Sings of individual values in as to a Sing for all as together.

singProd :: Sing as -> Prod Sing as

Convert a Sing for as to a Prod of Sings of each individual value in as.

singLength :: Sing as -> Length as

Convert a Sing for as into a Length representing the length of as.

Length as is equivalent to Prod Proxy as, so this is basically

singLength = map1 (const Proxy) . singProd

boolSing :: Boolean b -> Sing b

Convert a Boolean singleton for a into the Sing singleton for a.

singBool :: Sing b -> Boolean b

Convert a Sing singleton for b to a Boolean singleton for b.

data family Sing k (a :: k) :: *

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z0
• STrue :: Sing Bool z0

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z0
• SEQ :: Sing Ordering z0
• SGT :: Sing Ordering z0

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z0

data Sing N

data Sing N where

• SZ :: Sing N z
• SS :: Sing N z

type KnownC k (Sing k) a

type KnownC k (Sing k) a = SingI k a

type WitnessC ØC (SingI k a) (Sing k a)

type WitnessC ØC (SingI k a) (Sing k a) = ØC

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a0] z0
• SCons :: Sing [a0] z0

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a0) z0
• SJust :: Sing (Maybe a0) z0

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a0) z0

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a0 b0) z0
• SRight :: Sing (Either a0 b0) z0

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a0, b0) z0

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

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

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a0, b0, c0) z0

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a0, b0, c0, d0) z0

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a0, b0, c0, d0, e0) z0

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

type SN = (Sing :: N -> Type)

type ZSym0 = Z

data SSym0 l

Instances

SuppressUnusedWarnings (TyFun N N -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type Apply N N SSym0 l0

type Apply N N SSym0 l0 = SSym1 l0

type SSym1 t = S t

natSing :: Nat n -> Sing n

Convert a Nat singleton for n to a Sing singleton for n.

singNat :: Sing n -> Nat n

Convert a Sing singleton for n to a Nat singleton for n.

parSing :: (Sing :*: Sing) '(a, b) -> Sing '(a, b)

Convert a :*: tupling of Sing a and Sing b into a single Sing for '(a, b).

singPar :: Sing '(a, b) -> (Sing :*: Sing) '(a, b)

Convert a Sing of '(a, b) to a :*: tupling of Sing a and Sing b.

choiceSing :: (Sing :+: Sing) e -> Sing e

Convert a :+: sum between a Sing a and Sing b into a Sing of a sum (Either) of a and b.

singChoice :: Sing e -> (Sing :+: Sing) e

Convert a Sing of a sum (Either) of a and b to a :+: sum between Sing a and Sing b.

optionSing :: Option Sing a -> Sing a

Convert an Option of Sing a to a Sing of an optional (Maybe) a.

singOption :: Sing a -> Option Sing a

Convert a Sing of an optional (Maybe) a to an Option of Sing a.

Orphan instances

SingKind N

Associated Types

type DemoteRep N :: *

Methods

fromSing :: Sing N a -> DemoteRep N

toSing :: DemoteRep N -> SomeSing N

SingI N Z

Methods

sing :: Sing Z a

SingI N n0 => SingI N (S n0)

Methods

sing :: Sing (S n0) a

SEq k2 => Eq1 k2 (Sing k2)

Methods

eq1 :: f a -> f a -> Bool

neq1 :: f a -> f a -> Bool

SOrd k2 => Ord1 k2 (Sing k2)

Methods

compare1 :: f a -> f a -> Ordering

(<#) :: f a -> f a -> Bool

(>#) :: f a -> f a -> Bool

(<=#) :: f a -> f a -> Bool

(>=#) :: f a -> f a -> Bool

SingI k a => Known k (Sing k) a

Associated Types

type KnownC (Sing k) (a :: Sing k -> *) (a :: Sing k) :: Constraint

Methods

known :: a a

Witness ØC (SingI k a) (Sing k a)

Associated Types

type WitnessC (ØC :: Constraint) (SingI k a :: Constraint) (Sing k a) :: Constraint

Methods

(\\) :: ØC => (SingI k a -> r) -> Sing k a -> r