Data.Parameterized.List

This module defines a list over two parameters. The first is a fixed type-level function k -> * for some kind k, and the second is a list of types with kind k that provide the indices for the values in the list.

This type is closely related to the Context type in Data.Parameterized.Context.

Documentation

data List :: (k -> *) -> [k] -> * where

Parameterized list of elements.

Constructors

Nil :: List f '[]

(:<) :: f tp -> List f tps -> List f (tp ': tps) infixr 5

Instances

TraversableFC (List :: (k -> Type) -> [k] -> Type)

Defined in Data.Parameterized.List

Methods

traverseFC :: Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). List f x -> m (List g x)

FoldableFC (List :: (k -> Type) -> [k] -> Type)

Defined in Data.Parameterized.List

Methods

foldMapFC :: Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). List f x -> m

foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> List f x -> b

foldlFC :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> List f x -> b

foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> List f x -> b

foldlFC' :: (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> List f x -> b

toListFC :: (forall (x :: k0). f x -> a) -> forall (x :: l). List f x -> [a]

FunctorFC (List :: (k -> Type) -> [k] -> Type)

Defined in Data.Parameterized.List

Methods

fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). List f x -> List g x

TestEquality f => TestEquality (List f :: [k] -> Type)

Defined in Data.Parameterized.List

Methods

testEquality :: List f a -> List f b -> Maybe (a :~: b)

ShowF f => ShowF (List f :: [k] -> Type)

Defined in Data.Parameterized.List

Methods

withShow :: p (List f) -> q tp -> (Show (List f tp) -> a) -> a

showF :: List f tp -> String

showsPrecF :: Int -> List f tp -> String -> String

OrdF f => OrdF (List f :: [k] -> Type)

Defined in Data.Parameterized.List

Methods

compareF :: List f x -> List f y -> OrderingF x y

leqF :: List f x -> List f y -> Bool

ltF :: List f x -> List f y -> Bool

geqF :: List f x -> List f y -> Bool

gtF :: List f x -> List f y -> Bool

IsRepr f => IsRepr (List f :: [k] -> Type)

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: List f a -> (KnownRepr (List f) a -> r) -> r

KnownRepr (List f :: [k] -> Type) ([] :: [k])

Defined in Data.Parameterized.List

Methods

knownRepr :: List f []

(KnownRepr f s, KnownRepr (List f) sh) => KnownRepr (List f :: [a] -> Type) (s ': sh :: [a])

Defined in Data.Parameterized.List

Methods

knownRepr :: List f (s ': sh)

ShowF f => Show (List f sh)

Defined in Data.Parameterized.List

Methods

showsPrec :: Int -> List f sh -> ShowS

show :: List f sh -> String

showList :: [List f sh] -> ShowS

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

Represents an index into a type-level list. Used in place of integers to 1. ensure that the given index *does* exist in the list 2. guarantee that it has the given kind

Constructors

IndexHere :: Index (x ': r) x

IndexThere :: !(Index r y) -> Index (x ': r) y

Instances

TestEquality (Index l :: k -> Type)

Defined in Data.Parameterized.List

Methods

testEquality :: Index l a -> Index l b -> Maybe (a :~: b)

ShowF (Index l :: k -> Type)

Defined in Data.Parameterized.List

Methods

withShow :: p (Index l) -> q tp -> (Show (Index l tp) -> a) -> a

showF :: Index l tp -> String

showsPrecF :: Int -> Index l tp -> String -> String

OrdF (Index l :: k -> Type)

Defined in Data.Parameterized.List

Methods

compareF :: Index l x -> Index l y -> OrderingF x y

leqF :: Index l x -> Index l y -> Bool

ltF :: Index l x -> Index l y -> Bool

geqF :: Index l x -> Index l y -> Bool

gtF :: Index l x -> Index l y -> Bool

Eq (Index l x)

Defined in Data.Parameterized.List

Methods

(==) :: Index l x -> Index l x -> Bool

(/=) :: Index l x -> Index l x -> Bool

Ord (Index sh x)

Defined in Data.Parameterized.List

Methods

compare :: Index sh x -> Index sh x -> Ordering

(<) :: Index sh x -> Index sh x -> Bool

(<=) :: Index sh x -> Index sh x -> Bool

(>) :: Index sh x -> Index sh x -> Bool

(>=) :: Index sh x -> Index sh x -> Bool

max :: Index sh x -> Index sh x -> Index sh x

min :: Index sh x -> Index sh x -> Index sh x

Show (Index l x)

Defined in Data.Parameterized.List

Methods

showsPrec :: Int -> Index l x -> ShowS

show :: Index l x -> String

showList :: [Index l x] -> ShowS

indexValue :: Index l tp -> Integer

Return the index as an integer.

(!!) :: List f l -> Index l x -> f x

Return the value in a list at a given index

update :: List f l -> Index l s -> (f s -> f s) -> List f l

Update the List at an index

indexed :: Index l x -> Simple Lens (List f l) (f x)

Provides a lens for manipulating the element at the given index.

imap :: forall f g l. (forall x. Index l x -> f x -> g x) -> List f l -> List g l

Map over the elements in the list, and provide the index into each element along with the element itself.

ifoldr :: forall sh a b. (forall tp. Index sh tp -> a tp -> b -> b) -> b -> List a sh -> b

Right-fold with an additional index.

izipWith :: forall a b c sh. (forall tp. Index sh tp -> a tp -> b tp -> c tp) -> List a sh -> List b sh -> List c sh

Zip up two lists with a zipper function, which can use the index.

itraverse :: forall a b sh t. Applicative t => (forall tp. Index sh tp -> a tp -> t (b tp)) -> List a sh -> t (List b sh)

Traverse with an additional index.

Constants

index0 :: Index (x ': r) x

Index 0

index1 :: Index (x0 ': (x1 ': r)) x1

Index 1

index2 :: Index (x0 ': (x1 ': (x2 ': r))) x2

Index 2

index3 :: Index (x0 ': (x1 ': (x2 ': (x3 ': r)))) x3

Index 3