Fusion law for foldr1?

Question

For foldr we have the fusion law: if f is strict, f a = b, and

f (g x y) = h x (f y) for all x, y, then f . foldr g a = foldr h b.

How can one discover/derive a similar law for foldr1? (It clearly can't even take the same form - consider the case when both sides act on [x].)

Answer 1

You can use free theorems to derive statements like the fusion law. The Automatic generation of free theorems does this work for you, it automatically derives the following statement if you enter foldr1 or the type (a -> a -> a) -> [a] -> a.

If f strict and f (p x y) = q (f x) (f y)) for all x and y you have f (foldr1 p z) = foldr1 q (map f z)). That is, in contrast to you statement about foldr you get an additional map f on the right hand side.

Also note that the free theorem for foldr is slightly more general than your fusion law and, therefore, looks quite similar to the law for foldr1. Namely you have for strict functions g and f if g (p x y) = q (f x) (g y)) for all x and y then g (foldr p z v) = foldr q (g z) (map f v)).

Answer 2

I don't know if there's going to be anything satisfying for foldr1. [I think] It's just defined as

foldr1 f (x:xs) = foldr f x xs

let's first expand what you have above to work on the entire list,

f (foldr g x xs) = foldr h (f x) xs

for foldr1, you could say,

f (foldr1 g xs) = f (foldr g x xs)
= foldr h (f x) xs

to recondense into foldr1, you can create some imaginary function that maps f to the left element, for a result of,

f . foldr1 g = foldr1 h (mapfst f) where
    mapfst (x:xs) = f x : xs