git.iko.soy/Idris-dev
on master help sign in
add Foldable
c7fa2c7Melvar Chen
lib/Prelude/Foldable.idrnew file+29
compare with master
unifiedsplit
@@ -0,0 +1,29 @@
1+module Prelude.Foldable
2+
3+import Builtins
4+import Prelude.Algebra
5+
6+%access public
7+%default total
8+
9+class Foldable (t : Type -> Type) where
10+ foldr : (elt -> acc -> acc) -> acc -> t elt -> acc
11+
12+foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
13+foldl f z t = foldr (flip (.) . flip f) id t z
14+
15+concat : (Foldable t, Monoid a) => t a -> a
16+concat = foldr (<+>) neutral
17+
18+and : Foldable t => t Bool -> Bool
19+and = foldr (&&) True
20+
21+or : Foldable t => t Bool -> Bool
22+or = foldr (||) False
23+
24+any : (Foldable t, Functor t) => (a -> Bool) -> t a -> Bool
25+any p = Foldable.or . fmap p
26+
27+all : (Foldable t, Functor t) => (a -> Bool) -> t a -> Bool
28+all p = Foldable.and . fmap p
29+