Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

## Synopsis

- data Some :: (k -> Type) -> Type where
- withSome :: Some b -> (forall i. b i -> a) -> a
- data All :: (x -> Type) -> [x] -> Type where
- makeAll :: (a -> Some b) -> [a] -> Some (All b)
- forgetAll :: (forall x. b x -> a) -> All b xs -> [a]
- data Index :: [x] -> x -> Type where
- 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 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ₙ`

.

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.

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.