0 | ||| We can regarding any functor as indexed, with a specified fixed
 1 | ||| index.
 2 | module Data.Indexed.Fixed
 3 |
 4 | import Data.Witherable.Indexed
 5 |
 6 |
 7 | public export
 8 | record FixIndex {0 i : Type} (x : i) (f : Type -> Type) (a : Type) where
 9 |   constructor WithIndex
10 |   unIndex : f a
11 |
12 |
13 | export
14 | Functor f => Functor (FixIndex x f) where
15 |   map f (WithIndex m) = WithIndex $ map f m
16 |
17 | export
18 | {x : i} -> Functor f => IndFunctor i (FixIndex x f) where
19 |   imap f (WithIndex m) = WithIndex $ map (f x) m
20 |
21 | export
22 | Foldable f => Foldable (FixIndex x f) where
23 |   foldl f z (WithIndex m) = foldl f z m
24 |   foldr f z (WithIndex m) = foldr f z m
25 |
26 | export
27 | {x : i} -> Foldable f => IndFoldable i (FixIndex x f) where
28 |   ifoldl f z (WithIndex m) = foldl (flip f x) z m
29 |   ifoldr f z (WithIndex m) = foldr (f x) z m
30 |
31 | export
32 | Traversable f => Traversable (FixIndex x f) where
33 |   traverse f (WithIndex m) = WithIndex <$> traverse f m
34 |
35 | export
36 | {x : i} -> Traversable f => IndTraversable i (FixIndex x f) where
37 |   itraverse f (WithIndex m) = WithIndex <$> traverse (f x) m
38 |
39 | export
40 | Filterable f => Filterable (FixIndex x f) where
41 |   mapMaybe f (WithIndex m) = WithIndex $ mapMaybe f m
42 |
43 | export
44 | {x : i} -> Filterable f => IndFilterable i (FixIndex x f) where
45 |   imapMaybe f (WithIndex m) = WithIndex $ mapMaybe (f x) m
46 |
47 | export
48 | Witherable f => Witherable (FixIndex x f) where
49 |   wither f (WithIndex m) = WithIndex <$> wither f m
50 |
51 | export
52 | {x : i} -> Witherable f => IndWitherable i (FixIndex x f) where
53 |   iwither f (WithIndex m) = WithIndex <$> wither (f x) m
54 |