
  0 | ||| An IndTraversable is a Traversable able to read some extra data,
  1 | ||| the index.
  2 | module Data.Traversable.Indexed
  3 | 
  4 | import Control.Applicative.Const
  5 | import Data.Vect
  6 | 
  7 | import public Data.Foldable.Indexed
  8 | 
  9 | public export
 10 | interface (Traversable t, IndFoldable i t) => IndTraversable i t | t where
 11 |   itraverse : Applicative f => (i -> a -> f b) -> t a -> f (t b)
 12 | 
 13 | 
 14 | export
 15 | IndTraversable () Maybe where
 16 |   itraverse f = traverse (f ())
 17 | 
 18 | export
 19 | IndTraversable a (Pair a) where
 20 |   itraverse f (MkPair x y) = MkPair x <$> f x y
 21 | 
 22 | export
 23 | IndTraversable Nat List where
 24 |   itraverse g = inner 0 where
 25 |     inner : Nat -> List a -> f (List b)
 26 |     inner _ [] = pure []
 27 |     inner i (a::as) = (::) <$> g i a <*> inner (i+1) as
 28 | 
 29 | export
 30 | IndTraversable (Fin k) (Vect k) where
 31 |   itraverse f [] = pure []
 32 |   itraverse f (x::xs) = (::) <$> f FZ x <*> itraverse (f . FS) xs
 33 | 
 34 | ||| Any traversable is automatically foldable; this is a ifoldMap
 35 | ||| operation
 36 | indTraversableFoldMap : (IndTraversable i t, Monoid m) => (i -> a -> m) -> t a -> m
 37 | indTraversableFoldMap f = let
 38 |   g : i -> a -> Const m ()
 39 |   g x = MkConst . f x
 40 |   in runConst . itraverse g
 41 |