
  0 | module Control.Functor.Indexed
  1 | 
  2 | export
  3 | infixl 1 <<&>>
  4 | 
  5 | export
  6 | infixr 4 <<$>>, <<$, $>>
  7 | 
  8 | ||| An Indexed Functor.
  9 | ||| This interface is indexed backwards of similar utlities in Haskell
 10 | ||| to make it more readily compatible with the evolution of a type from
 11 | ||| Indexed simply on values (or types) but also on functions that depend on
 12 | ||| those values.
 13 | |||
 14 | ||| An indexed functor where the mappable type comes last does not later
 15 | ||| refactor into what this library calls a TransitionIndexed type as readily.
 16 | public export
 17 | interface IndexedFunctor x y (0 f : Type -> x -> y -> Type) | f where
 18 |   total
 19 |   map : {0 j : x} -> {0 k : y} -> (a -> b) -> f a j k -> f b j k 
 20 | 
 21 | ||| Map for indexed functors.
 22 | public export
 23 | (<<$>>) : IndexedFunctor x y f => (a -> b) -> f a j k -> f b j k
 24 | (<<$>>) = map
 25 | 
 26 | ||| Flipped version of `<<$>>`
 27 | public export
 28 | (<<&>>) : IndexedFunctor x y f => f a j k -> (a -> b) -> f b j k
 29 | (<<&>>) = flip (<<$>>)
 30 | 
 31 | ||| Run something for effects, replacing the return value afterwards.
 32 | public export
 33 | (<<$) : IndexedFunctor x y f => b -> f a j k -> f b j k
 34 | (<<$) = map . const
 35 | 
 36 | ||| Flipped version of `<<$`
 37 | public export
 38 | ($>>) : IndexedFunctor x y f => f a j k -> b -> f b j k
 39 | ($>>) = flip (<<$)
 40 | 
 41 | ||| Run something for effects, throwing away the return value.
 42 | %inline
 43 | public export
 44 | ignore : IndexedFunctor x y f => f a j k -> f () j k
 45 | ignore = map (const ())
 46 | 
 47 |