class Data.Foldable (F : Type u → Type v) : Type (max (u + 1) v)

Foldable captures the pattern of folding a structure into a single value.

For a Foldable container $F$: $$\text{foldr}(f, z, [x_1, \ldots, x_n]) = f(x_1, f(x_2, \ldots f(x_n, z)))$$ $$\text{foldl}(f, z, [x_1, \ldots, x_n]) = f(\ldots f(f(z, x_1), x_2) \ldots, x_n)$$

• foldr {α β : Type u} : (α → β → β) → β → F α → β

  Right fold: $\text{foldr}(f, z, t) = f(x_1, f(x_2, \ldots f(x_n, z)))$.

• foldl {β α : Type u} : (β → α → β) → β → F α → β

  Left fold: $\text{foldl}(f, z, t) = f(\ldots f(f(z, x_1), x_2) \ldots, x_n)$.

• toList {α : Type u} : F α → List α

  Convert to a list, preserving order.

@[inline]

def Data.Foldable.foldMap {F : Type u_1 → Type u_2} {β α : Type u_1} [Foldable F] [Append β] [Inhabited β] (f : α → β) (t : F α) : β

Map each element to a monoid and combine. $$\text{foldMap}(f, [x_1, \ldots, x_n]) = f(x_1) \mathbin{++} f(x_2) \mathbin{++} \cdots \mathbin{++} f(x_n)$$

Uses Append and starts from mempty.

Equations

• Data.Foldable.foldMap f t = Data.Foldable.foldr (fun (a : α) (b : β) => f a ++ b) default t

@[inline]

def Data.Foldable.null {F : Type → Type u_1} {α : Type} [Foldable F] (t : F α) : Bool

Is the structure empty? $$\text{null}(t) \iff |t| = 0$$

Equations

• Data.Foldable.null t = Data.Foldable.foldr (fun (x : α) (x_1 : Bool) => false) true t

@[inline]

def Data.Foldable.length {F : Type → Type u_1} {α : Type} [Foldable F] (t : F α) : Nat

Count of elements. $$\text{length}(t) = |t|$$

Equations

• Data.Foldable.length t = Data.Foldable.foldl (fun (n : Nat) (x : α) => n + 1) 0 t

@[inline]

def Data.Foldable.any {F : Type → Type u_1} {α : Type} [Foldable F] (p : α → Bool) (t : F α) : Bool

Does any element satisfy the predicate? $$\text{any}(p, t) \iff \exists x \in t,\; p(x) = \text{true}$$

Equations

• Data.Foldable.any p t = Data.Foldable.foldr (fun (a : α) (b : Bool) => p a || b) false t

@[inline]

def Data.Foldable.all {F : Type → Type u_1} {α : Type} [Foldable F] (p : α → Bool) (t : F α) : Bool

Do all elements satisfy the predicate? $$\text{all}(p, t) \iff \forall x \in t,\; p(x) = \text{true}$$

Equations

• Data.Foldable.all p t = Data.Foldable.foldr (fun (a : α) (b : Bool) => p a && b) true t

@[inline]

def Data.Foldable.find? {F : Type u_1 → Type u_2} {α : Type u_1} [Foldable F] (p : α → Bool) (t : F α) : Option α

Find the first element satisfying a predicate.

Equations

• Data.Foldable.find? p t = Data.Foldable.foldr (fun (a : α) (b : Option α) => if p a = true then some a else b) none t

@[inline]

def Data.Foldable.elem {F : Type → Type u_1} {α : Type} [Foldable F] [BEq α] (a : α) (t : F α) : Bool

Is the element in the structure? $$\text{elem}(x, t) \iff \exists y \in t,\; x = y$$

Equations

• Data.Foldable.elem a t = Data.Foldable.any (fun (x : α) => x == a) t

@[inline]

def Data.Foldable.minimum? {F : Type u_1 → Type u_2} {α : Type u_1} [Foldable F] [Min α] (t : F α) : Option α

The minimum element, if the structure is non-empty.

Equations

• Data.Foldable.minimum? t = Data.Foldable.foldl (fun (acc : Option α) (a : α) => some (match acc with | none => a | some m => min m a)) none t

@[inline]

def Data.Foldable.maximum? {F : Type u_1 → Type u_2} {α : Type u_1} [Foldable F] [Max α] (t : F α) : Option α

The maximum element, if the structure is non-empty.

Equations

• Data.Foldable.maximum? t = Data.Foldable.foldl (fun (acc : Option α) (a : α) => some (match acc with | none => a | some m => max m a)) none t

@[inline]

def Data.Foldable.sum {F : Type u_1 → Type u_2} {α : Type u_1} [Foldable F] [Add α] [OfNat α 0] (t : F α) : α

Sum of all elements. $$\text{sum}(t) = \sum_{x \in t} x$$

Equations

• Data.Foldable.sum t = Data.Foldable.foldl (fun (x1 x2 : α) => x1 + x2) 0 t

@[inline]

def Data.Foldable.product {F : Type u_1 → Type u_2} {α : Type u_1} [Foldable F] [Mul α] [OfNat α 1] (t : F α) : α

Product of all elements. $$\text{product}(t) = \prod_{x \in t} x$$

Equations

• Data.Foldable.product t = Data.Foldable.foldl (fun (x1 x2 : α) => x1 * x2) 1 t

@[inline]

def Data.Foldable.minimum1 {α : Type u_1} [Ord α] (ne : List.NonEmpty α) : α

Total minimum on a non-empty structure. No Option needed. $$\text{minimum1}([x_1, \ldots, x_n]) = \min(x_1, \ldots, x_n)$$

Equations

• Data.Foldable.minimum1 ne = List.foldl (fun (acc a : α) => if (compare a acc == Ordering.lt) = true then a else acc) ne.head ne.tail

@[inline]

def Data.Foldable.maximum1 {α : Type u_1} [Ord α] (ne : List.NonEmpty α) : α

Total maximum on a non-empty structure. No Option needed. $$\text{maximum1}([x_1, \ldots, x_n]) = \max(x_1, \ldots, x_n)$$

Equations

• Data.Foldable.maximum1 ne = List.foldl (fun (acc a : α) => if (compare a acc == Ordering.gt) = true then a else acc) ne.head ne.tail

@[implicit_reducible]

instance Data.instFoldableList : Foldable List

Equations

• Data.instFoldableList = { foldr := fun {α β : Type ?u.10} => List.foldr, foldl := fun {β α : Type ?u.10} => List.foldl, toList := fun {α : Type ?u.10} => id }

@[implicit_reducible]

instance Data.instFoldableOption : Foldable Option

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.instFoldableNonEmpty : Foldable List.NonEmpty

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.instFoldableEither {α : Type u_1} : Foldable (Either α)

Equations

• One or more equations did not get rendered due to their size.

theorem Data.foldr_nil {α β : Type u_1} {f : α → β → β} {z : β} : Foldable.foldr f z [] = z

foldr on an empty list is the initial accumulator.

theorem Data.foldl_nil {β α : Type u_1} {f : β → α → β} {z : β} : Foldable.foldl f z [] = z

foldl on an empty list is the initial accumulator.