Data.Type.Index

A singleton-esque type for representing indices in a type-level list.

Documentation

data Index :: [k] -> k -> * where

Constructors

IZ :: Index (a :< as) a

IS :: !(Index as a) -> Index (b :< as) a

Instances

Read2 l [l] (Index l)

Methods

readsPrec2 :: Int -> ReadS (Some2 (Index l) k f)

IxTraversable1 k [k] (Index k) (Sum k)

Methods

itraverse1 :: Applicative h => (forall a. i b a -> f a -> h (g a)) -> t f b -> h (t g b)

IxTraversable1 k [k] (Index k) (Prod k)

Methods

itraverse1 :: Applicative h => (forall a. i b a -> f a -> h (g a)) -> t f b -> h (t g b)

IxFoldable1 k [k] (Index k) (Sum k)

Methods

ifoldMap1 :: Monoid m => (forall a. i b a -> f a -> m) -> t f b -> m

IxFoldable1 k [k] (Index k) (Prod k)

Methods

ifoldMap1 :: Monoid m => (forall a. i b a -> f a -> m) -> t f b -> m

IxFunctor1 k [k] (Index k) (Sum k)

Methods

imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b

IxFunctor1 k [k] (Index k) (Prod k)

Methods

imap1 :: (forall a. i b a -> f a -> g a) -> t f b -> t g b

TestEquality k (Index k as)

Methods

testEquality :: f a -> f b -> Maybe ((Index k as :~: a) b)

Show1 k (Index k as)

Methods

showsPrec1 :: Int -> f a -> ShowS

show1 :: f a -> String

Ord1 k (Index k as)

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

Eq1 k (Index k as)

Methods

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

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

(∈) k a as => Known k (Index k as) a

Associated Types

type KnownC (Index k as) (a :: Index k as -> *) (a :: Index k as) :: Constraint

Methods

known :: a a

Witness ØC (Elem k as a) (Index k as a)

Associated Types

type WitnessC (ØC :: Constraint) (Elem k as a :: Constraint) (Index k as a) :: Constraint

Methods

(\\) :: ØC => (Elem k as a -> r) -> Index k as a -> r

Eq (Index k as a)

Methods

(==) :: Index k as a -> Index k as a -> Bool

(/=) :: Index k as a -> Index k as a -> Bool

Ord (Index k as a)

Methods

compare :: Index k as a -> Index k as a -> Ordering

(<) :: Index k as a -> Index k as a -> Bool

(<=) :: Index k as a -> Index k as a -> Bool

(>) :: Index k as a -> Index k as a -> Bool

(>=) :: Index k as a -> Index k as a -> Bool

max :: Index k as a -> Index k as a -> Index k as a

min :: Index k as a -> Index k as a -> Index k as a

Show (Index k as a)

Methods

showsPrec :: Int -> Index k as a -> ShowS

show :: Index k as a -> String

showList :: [Index k as a] -> ShowS

type KnownC k (Index k as) a

type KnownC k (Index k as) a = (∈) k a as

type WitnessC ØC (Elem k as a) (Index k as a)

type WitnessC ØC (Elem k as a) (Index k as a) = ØC

elimIndex :: (forall xs. p (a :< xs) a) -> (forall x xs. Index xs a -> p xs a -> p (x :< xs) a) -> Index as a -> p as a

ixNil :: Index Ø a -> b

onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a

type (∈) a as = Elem as a infix 6

class Elem as a where

Minimal complete definition

elemIndex

Methods

elemIndex :: Index as a

Instances

Elem k as a => Elem k ((:<) k b as) a

Methods

elemIndex :: Index ((k :< b) as) a a

Elem k ((:<) k a as) a

Methods

elemIndex :: Index ((k :< a) as) a a

Witness ØC (Elem k as a) (Index k as a)

Associated Types

type WitnessC (ØC :: Constraint) (Elem k as a :: Constraint) (Index k as a) :: Constraint

Methods

(\\) :: ØC => (Elem k as a -> r) -> Index k as a -> r

type WitnessC ØC (Elem k as a) (Index k as a)

type WitnessC ØC (Elem k as a) (Index k as a) = ØC

class EveryC c as => Every c as where

Minimal complete definition

every

Associated Types

type EveryC c as :: Constraint

Methods

every :: Index as a -> Wit (c a)

Instances

Every k c (Ø k)

Associated Types

type EveryC c (Ø k :: c -> Constraint) (as :: [c]) :: Constraint

Methods

every :: Index c as a -> Wit (Ø k a)

(c a1, Every a c as) => Every a c ((:<) a a1 as)

Associated Types

type EveryC c ((:<) a a1 as :: c -> Constraint) (as :: [c]) :: Constraint

Methods

every :: Index c as a -> Wit ((a :< a1) as a)

class ListC ((c <$> xs) <&> y) => Every2 c xs y where

Minimal complete definition

every2

Methods

every2 :: Index xs x -> Wit (c x y)

Instances

Every2 l k c (Ø k) y

Methods

every2 :: Index (Ø k) xs x -> Wit (y x y)

(c x y, Every2 l a c xs y) => Every2 l a c ((:<) a x xs) y

Methods

every2 :: Index ((a :< x) xs) xs x -> Wit (y x y)