partitionM -package:Agda

A version of partition that works with a monadic predicate.

partitionM (Just . even) [1,2,3] == Just ([2], [1,3])
partitionM (const Nothing) [1,2,3] == Nothing

Monadic version of partition

Partitions the Messages and returns a tuple which first element are the warnings, and the second the errors.

Partition a list into elements which evaluate to Just or Nothing by f.

forAllMaybeFn $ \f xs -> partitionMaybe f xs == (mapMaybe f xs, filter (isNothing . f) xs)

forAllPredicates $ \p xs -> partition p xs == partitionMaybe (\x -> toMaybe (p x) x) xs

Cf. catMaybesR

Deprecated: This will be removed in future releases.

Partition elements of the supplied mutable vector according to the predicate.

Example

>>> import Data.Massiv.Array as A

>>> import Data.Massiv.Array.Mutable.Algorithms

>>> :set -XOverloadedLists

>>> m <- thaw ([2,1,50,10,20,8] :: Array P Ix1 Int)

>>> unstablePartitionM m (pure . (<= 10))
4

>>> freeze Seq m
Array P Seq (Sz1 6)
[ 2, 1, 8, 10, 20, 50 ]