
  0 | ||| An indexed Witherable
  1 | module Data.Witherable.Indexed
  2 | 
  3 | import public Data.Filterable.Indexed
  4 | import public Data.Traversable.Indexed
  5 | import public Data.Witherable
  6 | 
  7 | 
  8 | public export
  9 | interface (Witherable t, IndTraversable i t, IndFilterable i t) => IndWitherable i t | t where
 10 |   iwither : (Applicative f) => (i -> a -> f (Maybe b)) -> t a -> f (t b)
 11 |   iwither f = map catMaybes . itraverse f
 12 | 
 13 | 
 14 | export
 15 | IndWitherable () Maybe where
 16 | 
 17 | 
 18 | -- This is not a conformant implementation, because filtering changes
 19 | -- the indices, but it's useful functionality.
 20 | export
 21 | enumWither : (Applicative f) => (Nat -> a -> f (Maybe b)) -> List a -> f (List b)
 22 | enumWither g = inner 0 where
 23 |   inner : Nat -> List a -> f (List b)
 24 |   inner _ [] = pure []
 25 |   inner n (x::xs) = maybeCompose <$> g n x <*> inner (n+1) xs where
 26 |     maybeCompose : Maybe b -> List b -> List b
 27 |     maybeCompose Nothing ys = ys
 28 |     maybeCompose (Just y) ys = y :: ys
 29 |