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 (through the TC typeclass), and also many appropriate orphan instances.

Conversion functions

class TC f where

Typeclass for type-combinator types that can be converted to and from singletons.

Minimal complete definition

fromTC, toTC

Methods

fromTC :: f a -> Sing a

Convert a type-combinator type that is equivalent to a singleton into its equivalent Sing.

toTC :: Sing a -> f a

Convert a Sing into its equivalent type-combinator type.

Instances

TC Bool Boolean

Methods

fromTC :: f a -> Sing Boolean a

toTC :: Sing Boolean a -> f a

TC N Nat

Methods

fromTC :: f a -> Sing Nat a

toTC :: Sing Nat a -> f a

TC [k] (Prod k (Sing k))

Methods

fromTC :: f a -> Sing (Prod k (Sing k)) a

toTC :: Sing (Prod k (Sing k)) a -> f a

TC (Maybe k) (Option k (Sing k))

Methods

fromTC :: f a -> Sing (Option k (Sing k)) a

toTC :: Sing (Option k (Sing k)) a -> f a

TC (Either k l) ((:+:) k l (Sing k) (Sing l))

Methods

fromTC :: f a -> Sing ((k :+: l) (Sing k) (Sing l)) a

toTC :: Sing ((k :+: l) (Sing k) (Sing l)) a -> f a

TC (k, l) ((:*:) k l (Sing k) (Sing l))

Methods

fromTC :: f a -> Sing ((k :*: l) (Sing k) (Sing l)) a

toTC :: Sing ((k :*: l) (Sing k) (Sing l)) a -> f a

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 :: Sing as -> Prod Proxy as
singLength = map1 (const Proxy) . toTC

This function is one-way, since the actual run-time information on the types in as is lost.

Orphan singleton instance for N

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

The singleton kind-indexed data family.

Instances

TC [k] (Prod k (Sing k))

Methods

fromTC :: f a -> Sing (Prod k (Sing k)) a

toTC :: Sing (Prod k (Sing k)) a -> f a

TC (Maybe k) (Option k (Sing k))

Methods

fromTC :: f a -> Sing (Option k (Sing k)) a

toTC :: Sing (Option k (Sing k)) a -> f a

TC (Either k l) ((:+:) k l (Sing k) (Sing l))

Methods

fromTC :: f a -> Sing ((k :+: l) (Sing k) (Sing l)) a

toTC :: Sing ((k :+: l) (Sing k) (Sing l)) a -> f a

TC (k, l) ((:*:) k l (Sing k) (Sing l))

Methods

fromTC :: f a -> Sing ((k :*: l) (Sing k) (Sing l)) a

toTC :: Sing ((k :*: l) (Sing k) (Sing l)) a -> f a

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

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

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 [a]

data Sing [a] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a)

data Sing (Maybe a) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a)

data Sing (NonEmpty a) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a b)

data Sing (Either a b) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a, b)

data Sing (a, b) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

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

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

}

data Sing (a, b, c)

data Sing (a, b, c) where

• STuple3 :: Sing (a, b, c) z

data Sing (a, b, c, d)

data Sing (a, b, c, d) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a, b, c, d, e)

data Sing (a, b, c, d, e) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a, b, c, d, e, f)

data Sing (a, b, c, d, e, f) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a, b, c, d, e, f, g)

data Sing (a, b, c, d, e, f, g) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

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

type ZSym0 = Z

data SSym0 (l :: TyFun N N)

Instances

SuppressUnusedWarnings (TyFun N N -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type Apply N N SSym0 l

type Apply N N SSym0 l = S l

type SSym1 (t :: N) = S t

Orphan instances

SingKind N

Associated Types

type Demote N = (r :: *)

Methods

fromSing :: Sing N a -> Demote N

toSing :: Demote N -> SomeSing N

SingI N Z

Methods

sing :: Sing Z a

SingI N n => SingI N (S n)

Methods

sing :: Sing (S n) a

SEq k3 => Eq1 k3 (Sing k3)

Methods

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

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

SOrd k3 => Ord1 k3 (Sing k3)

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 (SingI k a) (Sing k a) :: Constraint

Methods

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