interface Foldable t where
foldrLazy : (a -> Lazy b -> b) -> Lazy b -> t a -> b
foldr : (a -> b -> b) -> b -> t a -> b
foldl : (b -> a -> b) -> b -> t a -> bA Foldable is a container you can collapse with a fold. foldr combines the elements from the right with a binary function and a seed value; over a List it is the ordinary right fold.
foldrLazy is the fold that can stop: its function receives the fold of the rest suspended (Lazy b) and computes it only if it reads it, so foldrLazy (||) False xs stops at the first True. The seed waits too: it is read only if the fold reaches the end.
An implementation gives foldrLazy or foldr; each has a default definition by the other, and foldl one by foldr. Giving foldrLazy is the complete answer. With foldr alone, the default foldrLazy examines no more elements than needed but walks the whole container once (it builds one closure per element, and calls them only as far as the function reads).