Data.Filterable

A Filterable is a functor where elements can be thrown away

Definitions

interface Filterable : (Type -> Type) -> Type

Parameters: t
Constraints: Functor t
Methods:

mapMaybe : (a -> Maybe b) -> t a -> t b

catMaybes : t (Maybe a) -> t a

filter : (a -> Bool) -> t a -> t a

flush : t a -> t b

Implementations:

Filterable Maybe

Filterable List

(Monad m, Alternative m) => Filterable (Kleisli m a')

mapMaybe : Filterable t => (a -> Maybe b) -> t a -> t b

Visibility: public export

catMaybes : Filterable t => t (Maybe a) -> t a

Visibility: public export

filter : Filterable t => (a -> Bool) -> t a -> t a

Visibility: public export

flush : Filterable t => t a -> t b

Visibility: public export