Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Some (a :: k -> Type) where
- withSome :: Some b -> (forall (i :: k). b i -> a) -> a
- data All (a :: x -> Type) (b :: [x]) where
- makeAll :: forall {x} a (b :: x -> Type). (a -> Some b) -> [a] -> Some (All b)
- forgetAll :: forall {x} b a (xs :: [x]). (forall (x1 :: x). b x1 -> a) -> All b xs -> [a]
- data Index (a :: [x]) (b :: x) where
- forgetIndex :: forall {x1} (xs :: [x1]) (x2 :: x1). Index xs x2 -> Int
- mapWithIndex :: forall {x} (xs :: [x]) p q. (forall (x1 :: x). Index xs x1 -> p x1 -> q x1) -> All p xs -> All q xs
- lIndex :: forall {x1} (xs :: [x1]) (x2 :: x1) (p :: x1 -> Type). Index xs x2 -> Lens' (All p xs) (p x2)
- lookupIndex :: forall {x1} p (xs :: [x1]) (x2 :: x1). All p xs -> Index xs x2 -> p x2
- allIndices :: forall {x} (p :: x -> Type) (xs :: [x]). All p xs -> All (Index xs) xs
Documentation
data All (a :: x -> Type) (b :: [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ₙ
.
makeAll :: forall {x} a (b :: x -> Type). (a -> Some b) -> [a] -> Some (All b) Source #
Constructing an indexed list from a plain list.
forgetAll :: forall {x} b a (xs :: [x]). (forall (x1 :: x). b x1 -> a) -> All b xs -> [a] Source #
Turning an indexed list back into a plain list.
forgetIndex :: forall {x1} (xs :: [x1]) (x2 :: x1). Index xs x2 -> Int Source #
Indices are just natural numbers.
mapWithIndex :: forall {x} (xs :: [x]) p q. (forall (x1 :: x). Index xs x1 -> p x1 -> q x1) -> All p xs -> All q xs Source #
Mapping over an indexed list.
lIndex :: forall {x1} (xs :: [x1]) (x2 :: x1) (p :: x1 -> Type). Index xs x2 -> Lens' (All p xs) (p x2) Source #
If you have an index you can get a lens for the given element.
lookupIndex :: forall {x1} p (xs :: [x1]) (x2 :: x1). All p xs -> Index xs x2 -> p x2 Source #
Looking up an element in an indexed list.