Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Utils.IndexedList

Synopsis

data Some :: (k -> Type) -> Type where
- Some :: f i -> Some f
withSome :: Some b -> (forall i. b i -> a) -> a
data All :: (x -> Type) -> [x] -> Type where
- Nil :: All p '[]
- Cons :: p x -> All p xs -> All p (x ': xs)
makeAll :: (a -> Some b) -> [a] -> Some (All b)
forgetAll :: (forall x. b x -> a) -> All b xs -> [a]
data Index :: [x] -> x -> Type where
- Zero :: Index (x ': xs) x
- Suc :: Index xs x -> Index (y ': xs) x
forgetIndex :: Index xs x -> Int
mapWithIndex :: (forall x. Index xs x -> p x -> q x) -> All p xs -> All q xs
lIndex :: Index xs x -> Lens' (p x) (All p xs)
lookupIndex :: All p xs -> Index xs x -> p x
allIndices :: All p xs -> All (Index xs) xs

Documentation

data Some :: (k -> Type) -> Type where Source #

Existential wrapper for indexed types.

Constructors

Some :: f i -> Some f

withSome :: Some b -> (forall i. b i -> a) -> a Source #

Unpacking a wrapped value.

data All :: (x -> Type) -> [x] -> Type where Source #

Lists indexed by a type-level list. A value of type All p [x₁..xₙ] is a sequence of values of types p x₁, .., p xₙ.

Constructors

Nil :: All p '[]
Cons :: p x -> All p xs -> All p (x ': xs)

makeAll :: (a -> Some b) -> [a] -> Some (All b) Source #

Constructing an indexed list from a plain list.

forgetAll :: (forall x. b x -> a) -> All b xs -> [a] Source #

Turning an indexed list back into a plain list.

data Index :: [x] -> x -> Type where Source #

An index into a type-level list.

Constructors

Zero :: Index (x ': xs) x
Suc :: Index xs x -> Index (y ': xs) x

Indices are just natural numbers.

mapWithIndex :: (forall x. Index xs x -> p x -> q x) -> All p xs -> All q xs Source #

Mapping over an indexed list.

lIndex :: Index xs x -> Lens' (p x) (All p xs) Source #

If you have an index you can get a lens for the given element.

lookupIndex :: All p xs -> Index xs x -> p x Source #

Looking up an element in an indexed list.

All indices into an indexed list.