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 k [k] (List k)

Methods

traverseFC :: Applicative m => (forall (s :: List k). e s -> m (f s)) -> t e c -> m (t f c)

FoldableFC k [k] (List k)

Methods

foldMapFC :: Monoid m => (forall (s :: List k). e s -> m) -> t e c -> m

foldrFC :: (forall (s :: List k). e s -> b -> b) -> b -> t e c -> b

foldlFC :: (forall (s :: List k). b -> e s -> b) -> b -> t e c -> b

foldrFC' :: (forall (s :: List k). e s -> b -> b) -> b -> t e c -> b

foldlFC' :: (forall (s :: List k). b -> e s -> b) -> b -> t e c -> b

toListFC :: (forall (tp :: List k). f tp -> a) -> t f c -> [a]

FunctorFC k [k] (List k)

Methods

fmapFC :: (forall (x :: List k). f x -> g x) -> forall (x :: k). m f x -> m g x

TestEquality k f => TestEquality [k] (List k f)

Methods

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

ShowF k f => ShowF [k] (List k f)

Methods

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

showF :: f tp -> String

showsF :: f tp -> String -> String

OrdF k f => OrdF [k] (List k f)

Methods

compareF :: ktp x -> ktp y -> OrderingF (List k f) x y

leqF :: ktp x -> ktp y -> Bool

ltF :: ktp x -> ktp y -> Bool

geqF :: ktp x -> ktp y -> Bool

gtF :: ktp x -> ktp y -> Bool

KnownRepr [k] (List k f) ([] k)

Methods

knownRepr :: [k] ctx

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

Methods

knownRepr :: (a ': s) sh ctx

ShowF k f => Show (List k f sh)

Methods

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

show :: List k f sh -> String

showList :: [List k 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 k (Index k l)

Methods

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

ShowF k (Index k l)

Methods

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

showF :: f tp -> String

showsF :: f tp -> String -> String

OrdF k (Index k l)

Methods

compareF :: ktp x -> ktp y -> OrderingF (Index k l) x y

leqF :: ktp x -> ktp y -> Bool

ltF :: ktp x -> ktp y -> Bool

geqF :: ktp x -> ktp y -> Bool

gtF :: ktp x -> ktp y -> Bool

Eq (Index k l x)

Methods

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

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

Ord (Index k sh x)

Methods

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

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

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

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

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

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

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

Show (Index k l x)

Methods

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

show :: Index k l x -> String

showList :: [Index k 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.

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