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 -> bUn Foldable est un conteneur qu'on peut replier par un pli. foldr combine les éléments depuis la droite avec une fonction binaire et une valeur initiale ; sur une List c'est le pli à droite habituel.
foldrLazy est le pli qui peut s'arrêter : sa fonction reçoit le pli du reste en attente (Lazy b) et ne le calcule que si elle le lit ; ainsi foldrLazy (||) False xs s'arrête au premier True. La graine attend elle aussi : elle n'est lue que si le pli va jusqu'au bout.
Une implémentation donne foldrLazy ou foldr ; chacune a une définition par défaut par l'autre, et foldl en a une par foldr. Donner foldrLazy est la réponse complète. Avec foldr seul, le foldrLazy par défaut n'examine que les éléments nécessaires mais parcourt tout le conteneur une fois (il fabrique une fonction par élément, et ne les appelle qu'aussi loin que la fonction lit).