Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.IndexedList

Synopsis

- data Some :: (k -> *) -> * where
  - Some :: f i -> Some f
- withSome :: Some b -> (forall i. b i -> a) -> a
- data All :: (x -> *) -> [x] -> * 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 -> * 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 -> *) -> * 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 -> *) -> [x] -> * 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 -> * where Source #

An index into a type-level list.

Constructors

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

forgetIndex :: Index xs x -> Int Source #

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.

allIndices :: All p xs -> All (Index xs) xs Source #

All indices into an indexed list.