
  0 | ||| Is there a more common name for this transformer?
  1 | ||| `ListT m a` is for `m (List a)` rather than this more progressive thing
  2 | 
  3 | module Libraries.Data.Tap
  4 | 
  5 | -- Note that `Tap m` is not strictly positive if `m` is not
  6 | %default covering
  7 | 
  8 | public export
  9 | data Tap : (Type -> Type) -> Type -> Type where
 10 |   Nil : Tap m a
 11 |   (::) : a -> m (Tap m a) -> Tap m a
 12 | 
 13 | export
 14 | Functor m => Functor (Tap m) where
 15 |   map f = \case
 16 |     [] => []
 17 |     x :: mxs => f x :: map (map f) mxs
 18 | 
 19 | export
 20 | traverse : Monad m => (a -> m b) -> Tap m a -> m (Tap m b)
 21 | traverse f [] = pure []
 22 | traverse f (x :: mxs) = pure (!(f x) :: (mxs >>= traverse f))
 23 | 
 24 | export
 25 | filter : Monad m => (a -> Bool) -> Tap m a -> m (Tap m a)
 26 | filter p [] = pure []
 27 | filter p (x :: mxs)
 28 |   = do let mxs = mxs >>= filter p
 29 |        if p x
 30 |          then pure $ x :: mxs
 31 |          else mxs
 32 |