packages feed

idris-0.9.9.1: lib/Prelude/Foldable.idr

module Prelude.Foldable

import Builtins
import Prelude.Algebra

%access public
%default total

class Foldable (t : Type -> Type) where
  foldr : (elt -> acc -> acc) -> acc -> t elt -> acc

foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
foldl f z t = foldr (flip (.) . flip f) id t z

concat : (Foldable t, Monoid a) => t a -> a
concat = foldr (<+>) neutral

concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
concatMap f = foldr ((<+>) . f) neutral

and : Foldable t => t Bool -> Bool
and = foldr (&&) True

or : Foldable t => t Bool -> Bool
or = foldr (||) False

any : Foldable t => (a -> Bool) -> t a -> Bool
any p = foldr ((||) . p) False

all : Foldable t => (a -> Bool) -> t a -> Bool
all p = foldr ((&&) . p) True

sum : (Foldable t, Num a) => t a -> a
sum = foldr (+) 0

product : (Foldable t, Num a) => t a -> a
product = foldr (*) 1