Copyright	(c) Galois Inc 2017
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	Safe
Language	Haskell98

Data.Parameterized.List

Contents

Constants

Description

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.

Synopsis

Documentation

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

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) Source #
Methods traverseFC :: Applicative m => (forall (s :: List k). e s -> m (f s)) -> t e c -> m (t f c) Source #
FoldableFC k [k] (List k) Source #
Methods foldMapFC :: Monoid m => (forall (s :: List k). e s -> m) -> t e c -> m Source # foldrFC :: (forall (s :: List k). e s -> b -> b) -> b -> t e c -> b Source # foldlFC :: (forall (s :: List k). b -> e s -> b) -> b -> t e c -> b Source # foldrFC' :: (forall (s :: List k). e s -> b -> b) -> b -> t e c -> b Source # foldlFC' :: (forall (s :: List k). b -> e s -> b) -> b -> t e c -> b Source # toListFC :: (forall (tp :: List k). f tp -> a) -> t f c -> [a] Source #
FunctorFC k [k] (List k) Source #
Methods fmapFC :: (forall (x :: List k). f x -> g x) -> forall (x :: k). m f x -> m g x Source #
TestEquality k f => TestEquality [k] (List k f) Source #
Methods testEquality :: f a -> f b -> Maybe ((List k f :~: a) b) #
ShowF k f => ShowF [k] (List k f) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
OrdF k f => OrdF [k] (List k f) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (List k f) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
KnownRepr [k] (List k f) ([] k) Source #
Methods knownRepr :: [k] ctx Source #
(KnownRepr a f s, KnownRepr [a] (List a f) sh) => KnownRepr [a] (List a f) ((:) a s sh) Source #
Methods knownRepr :: (a ': s) sh ctx Source #
ShowF k f => Show (List k f sh) Source #
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 Source #

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) Source #
Methods testEquality :: f a -> f b -> Maybe ((Index k l :~: a) b) #
ShowF k (Index k l) Source #
Methods withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source # showF :: f tp -> String Source # showsF :: f tp -> String -> String Source #
OrdF k (Index k l) Source #
Methods compareF :: ktp x -> ktp y -> OrderingF (Index k l) x y Source # leqF :: ktp x -> ktp y -> Bool Source # ltF :: ktp x -> ktp y -> Bool Source # geqF :: ktp x -> ktp y -> Bool Source # gtF :: ktp x -> ktp y -> Bool Source #
Eq (Index k l x) Source #
Methods (==) :: Index k l x -> Index k l x -> Bool # (/=) :: Index k l x -> Index k l x -> Bool #
Ord (Index k sh x) Source #
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) Source #
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 Source #

Return the index as an integer.

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

Return the value in a list at a given index

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

Update the List at an index

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

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 Source #

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 Source #

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) Source #

Traverse with an additional index.

Constants

index0 :: Index (x ': r) x Source #

Index 0

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

Index 1

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

Index 2

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

Index 3