@@ -9,9 +9,30 @@ import Prelude.Algebra
9%access public export
9%access public export
10%default total
10%default total
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.
16+||| @t The type of the 'Foldable' parameterised type.
12interface Foldable (t : Type -> Type) where
17interface Foldable (t : Type -> Type) where
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.
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.
13− foldr : (elem -> acc -> acc) -> acc -> t elem -> acc
26+ foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc
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
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.
14− foldl : (acc -> elem -> acc) -> acc -> t elem -> acc
35+ foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
15 foldl f z t = foldr (flip (.) . flip f) id t z
36 foldl f z t = foldr (flip (.) . flip f) id t z
17||| Combine each element of a structure into a monoid
38||| Combine each element of a structure into a monoid