
  0 | module Control.Applicative.Backwards
  1 | 
  2 | %default total
  3 | 
  4 | 
  5 | ||| Wrap an `Applicative` type constructor so that its actions are executed
  6 | ||| in the opposite order.
  7 | public export
  8 | record Backwards {0 k : Type} (f : k -> Type) a where
  9 |   constructor MkBackwards
 10 |   forwards : f a
 11 | 
 12 | 
 13 | public export
 14 | Functor f => Functor (Backwards f) where
 15 |   map f (MkBackwards x) = MkBackwards (map f x)
 16 | 
 17 | public export
 18 | Applicative f => Applicative (Backwards f) where
 19 |   pure = MkBackwards . pure
 20 |   MkBackwards f <*> MkBackwards x = MkBackwards (flip apply <$> x <*> f)
 21 |