Skip to main content

One post tagged with "fold_left"

View All Tags

ยท 8 min read
Natalie Klaus

OCaml developers at Tezos often use fold_left function in the code. Maybe the reason is that it is a bit easier to write efficient code using fold_left than fold_right.

fold_left and fold_right from OCaml library: List

val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a

fold_left f init [b1; ...; bn] is f (... (f (f init b1) b2) ...) bn.

val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b

fold_right f [a1; ...; an] init is f a1 (f a2 (... (f an init) ...)).
Not tail-recursive.

And from formal verification point of view, it is much easier to prove statements about fold_right either than about fold_left. Why? The reason is in how these functions are organized. Formal verification often uses mathematical induction as an instrument for proving statements on the lists.