FoldLeft in Terms of FoldRight

I [believe that I] wrote foldl in terms of foldr:

myFoldl :: (a -> b -> a) -> a -> [b] -> a
myFoldl f base xs = foldr (flip f) base (reverse xs)

Is this an idiomatic implementation?

Yes, I believe it's equivalent to the third duality theorem which states that for any finite list xs,

foldr op u xs = foldl (flip op) u (reverse xs)

Without appealing to the theorem, we can still prove your definition correct for any finite list xs. We'll need definitions of foldl and foldr:

Definition

(1) foldr _ u [] = u
(2) foldr op u (x:xs) = op x (foldr op u xs)

Definition

(3) foldl _ u [] = u
(4) foldl op u (x:xs) = foldl op (op u x) xs

And the following:

Lemma For finite lists xs, ys, foldr op u (ys ++ xs) = foldr op (foldr op u xs) ys.

Case []

RHS = foldr op (foldr op u xs) []
    = foldr op u xs -- by (1)
    = foldr op u ([] ++ xs)
    = LHS

Case y:ys

RHS = foldr op (foldr op u xs) (y:ys)
    = op y (foldr op (foldr op u xs) ys) -- by (2)
    = op y (foldr op u (ys ++ xs)) -- by induction hypothesis
    = foldr op u (y:ys ++ xs) -- by (2)
    = LHS

∎

Claim For any finite list xs, foldr (flip op) u (reverse xs) = foldl op u xs.

Case []

LHS = foldr (flip op) u (reverse [])
    = foldr (flip op) u []
    = [] -- by (1)
    = foldl op u [] -- by (3)
    = RHS

Case x:xs

LHS = foldr (flip op) u (reverse (x:xs))
    = foldr (flip op) u ((reverse xs) ++ [x])
    = foldr (flip op) (foldr (flip op) u [x]) (reverse xs) -- by the lemma
    = foldr (flip op) ((flip op) x (foldr (flip op) u [])) (reverse xs) -- by (2)
    = foldr (flip op) ((flip op) x u) (reverse xs) -- by (1)
    = foldl op ((flip op) x u) xs -- by induction hypothesis
    = foldl op (op u x) xs -- by definition of flip
    = foldl op u (x:xs) -- by (4)
    = RHS

∎

StackExchange Code Review Q#65241, answer score: 5