
  0 | ||| We can treat any dependent functor as an independent functor by
  1 | ||| using constant index
  2 | module Data.Indexed.Independent
  3 | 
  4 | import Data.Witherable.Dependent
  5 | import Data.Witherable.Indexed
  6 | 
  7 | 
  8 | public export
  9 | record Independent {k : Type} (t : (k -> Type) -> Type) (v : Type) where
 10 |   constructor Indep
 11 |   dep : t (const v)
 12 | 
 13 | export
 14 | DepFunctor i t => Functor (Independent t) where
 15 |   map f (Indep m) = Indep $ dmap (const f) m
 16 | 
 17 | export
 18 | DepFunctor i t => IndFunctor i (Independent t) where
 19 |   imap f (Indep m) = Indep $ dmap f m
 20 | 
 21 | export
 22 | DepFoldable i t => Foldable (Independent t) where
 23 |   foldl f z (Indep m) = dfoldl (\x, _, y => f x y) z m
 24 |   foldr f z (Indep m) = dfoldr (\_, x, y => f x y) z m
 25 | 
 26 | export
 27 | (DepFoldable i t, DepFunctor i t) => IndFoldable i (Independent t) where
 28 |   ifoldl f z (Indep m) = dfoldl f z m
 29 |   ifoldr f z (Indep m) = dfoldr f z m
 30 |   iconcatMap f (Indep m) = dconcatMap f m
 31 | 
 32 | export
 33 | (DepTraversable i t, DepFunctor i t) => Traversable (Independent t) where
 34 |   traverse f (Indep m) = Indep <$> dtraverse (const f) m
 35 | 
 36 | export
 37 | (DepTraversable i t, DepFunctor i t, DepFoldable i t) => IndTraversable i (Independent t) where
 38 |   itraverse f (Indep m) = Indep <$> dtraverse f m
 39 | 
 40 | export
 41 | (DepFilterable i t, DepFoldable i t) => Filterable (Independent t) where
 42 |   mapMaybe f (Indep m) = Indep $ dmapMaybe (const f) m
 43 | 
 44 | export
 45 | (DepFilterable i t, DepFoldable i t) => IndFilterable i (Independent t) where
 46 |   imapMaybe f (Indep m) = Indep $ dmapMaybe f m
 47 | 
 48 | export
 49 | (DepWitherable i t) => Witherable (Independent t) where
 50 |   wither f (Indep m) = Indep <$> dwither (const f) m
 51 | 
 52 | export
 53 | [independentWitherable] (DepWitherable i t) => IndWitherable i (Independent t) where
 54 |   iwither f (Indep m) = Indep <$> dwither f m
 55 |