
  0 | ||| A Filterable is a functor where elements can be thrown away
  1 | module Data.Filterable
  2 | 
  3 | 
  4 | public export
  5 | interface (Functor t) => Filterable t where
  6 | 
  7 |   mapMaybe : (a -> Maybe b) -> t a -> t b
  8 |   mapMaybe f = catMaybes . map f
  9 | 
 10 |   catMaybes : t (Maybe a) -> t a
 11 |   catMaybes = mapMaybe id
 12 | 
 13 |   filter : (a -> Bool) -> t a -> t a
 14 |   filter f = catMaybes . map g where
 15 |     g : a -> Maybe a
 16 |     g x = if f x then Just x else Nothing
 17 | 
 18 |   flush : t a -> t b
 19 |   flush = mapMaybe (const Nothing)
 20 | 
 21 | 
 22 | export
 23 | Filterable Maybe where
 24 |   mapMaybe = (=<<)
 25 | 
 26 | export
 27 | Filterable List where
 28 |   mapMaybe = Prelude.List.mapMaybe
 29 |