/Prelude-v20.0.0/List/fold.dhall

Copy path to clipboard

fold is the primitive function for consuming Lists

If you treat the list [ x, y, z ] as cons x (cons y (cons z nil)), then a fold just replaces each cons and nil with something else

Examples

  fold Natural [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) 0
≡ 10
  ( λ(nil : Natural) →
fold
Natural
[ 2, 3, 5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
nil
)
≡ (λ(nil : Natural) → 2 + (3 + (5 + nil)))
  ( λ(list : Type) →
λ(cons : Natural → listlist) →
λ(nil : list) →
fold Natural [ 2, 3, 5 ] list cons nil
)
≡ ( λ(list : Type) →
λ(cons : Natural → listlist) →
λ(nil : list) →
cons 2 (cons 3 (cons 5 nil))
)

Source

{-|
`fold` is the primitive function for consuming `List`s

If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a
`fold` just replaces each `cons` and `nil` with something else
-}
let fold
: ∀(a : Type) →
List a →
∀(list : Type) →
∀(cons : a → list → list) →
∀(nil : list) →
list
= List/fold

let example0 =
assert
: fold
Natural
[ 2, 3, 5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
0
≡ 10

let example1 =
assert
: ( λ(nil : Natural) →
fold
Natural
[ 2, 3, 5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
nil
)
≡ (λ(nil : Natural) → 2 + (3 + (5 + nil)))

let example2 =
assert
: ( λ(list : Type) →
λ(cons : Natural → listlist) →
λ(nil : list) →
fold Natural [ 2, 3, 5 ] list cons nil
)
≡ ( λ(list : Type) →
λ(cons : Natural → listlist) →
λ(nil : list) →
cons 2 (cons 3 (cons 5 nil))
)

in fold