@@ -9,9 +9,30 @@ import Prelude.Algebra
99%access public export
1010%default total
1111
12+||| The `Foldable` interface describes how you can iterate over the
13+||| elements in a parameterised type and combine the elements
14+||| together, using a provided function, into a single result.
15+|||
16+||| @t The type of the 'Foldable' parameterised type.
1217interface Foldable (t : Type -> Type) where
13− foldr : (elem -> acc -> acc) -> acc -> t elem -> acc
14− foldl : (acc -> elem -> acc) -> acc -> t elem -> acc
18+
19+ ||| Successivly combine the elements in a parameterised type using
20+ ||| the provided function, starting with the element that is in the
21+ ||| final position i.e. the right-most position.
22+ |||
23+ ||| @func The function used to 'fold' an element into the accumulated result.
24+ ||| @input The parameterised type.
25+ ||| @init The starting value the results are being combined into.
26+ foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc
27+
28+ ||| The same as `foldr` but begins the folding from the element at
29+ ||| the initial position in the data structure i.e. the left-most
30+ ||| position.
31+ |||
32+ ||| @func The function used to 'fold' an element into the accumulated result.
33+ ||| @input The parameterised type.
34+ ||| @init The starting value the results are being combined into.
35+ foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
1536 foldl f z t = foldr (flip (.) . flip f) id t z
1637
1738||| Combine each element of a structure into a monoid