Take This is its standalone principal type; in the right fold,
h = (.):h :: (b -> c) -> (a -> b) -> a -> c
h f g x = f (g x)c specializes to the type of a function from the accumulator to itself.For fixed The second equality is the induction hypothesis. Function extensionality gives the required equality of composed functions. This is an instance of the right-fold fusion law.
f, g and e, prove equality pointwise by structural induction on the list. At [] both sides return e. For x:xs, assume the equality for xs and calculate:foldr f e (map g (x:xs))
= f (g x) (foldr f e (map g xs))
= f (g x) (foldr (h f g) e xs)
= h f g x (foldr (h f g) e xs)
= foldr (h f g) e (x:xs)For the full lazy Haskell interpretation, include a bottom value for an undefined list spine: both sides are bottom there. The same constructor argument covers every finite approximation with an undefined tail. The Scott continuity of the list operations then extends equality to their limits, including infinite lists. Ordinary induction on finite total lists alone proves only that restricted case.
Articles by others on the same topic
There are currently no matching articles.