It is unclear what is the definition of a folded type

Question

foldl :: (a -> b -> a) -> a -> [b] -> a foldl step zero (x:xs) = foldl step (step zero x) xs foldl _ zero [] = zero 

I don’t quite understand why (a → b → a ) returns a , also (a → b → a) → a → [b] → a returns a . I would think that it should be: (a → b → c ) → a → [b] → c . Can someone explain this to me in the example below. Thanks!

 foldl (+) 0 (1:2:3:[]) foldl (+) (0 + 1) (2:3:[]) foldl (+) ((0 + 1) + 2) (3:[]) foldl (+) (((0 + 1) + 2) + 3) ([]) foldl (+) (((0 + 1) + 2) + 3) 

Answer 1

a represents the type of battery value, and b represents the type of each input element. (a -> b -> a) is a function that takes a battery value, some element in the list and returns a new battery value, which can be passed to the next step.

The type of the initial value must be a , so the first function call can take on the value of the accumulator. The battery function must take a and return a so that the value of the battery can be passed on to each bend step. The final fold value must be a , because it is the type of battery that will be returned by the final call to the fold function.

(a -> b -> c) -> a -> [b] -> c cannot represent bending, since the bending function does not accept a c . The input and output of the folding function must be of the same type, so that the battery can be transferred to the next fold step.

Let's see an example of what happens if the fold function returns a c .

 f :: Integer -> Integer -> Bool -- this is a valid (a -> b -> c) f acc n = (acc + n) > 0 

Suppose we use a dynamic language and we try to collapse f . What happens at runtime?

 foldl f 0 [1] ~ (0 + 1) > 0 == True :: Bool foldl f 0 [1, 2] ~ ((0 + 1) > 0) + 2) > 0 == error - no instance of (+) for Bool \_________/ \ | \ Bool + Integer 

You can see that you cannot bend if you are trying to copy incompatible types.

Answer 2

The return type of the folding function (type (a -> b -> a) ) must be the same as the type of its first input. This is due to the fact that looking at (almost correct, with the exception of the last line, which should not have the foldl (+) score) that you gave, the result of the previous call to the folding function is passed as the first input for the next call, Thus, the types must match. in (a -> b -> c) types of the first argument and the result will correspond only if a ~ c (equality for types), but in this case, when a and c are equal, we can also call them as a. Given that the folding function returns something of type a, the result of the entire call to foldl will also be type a, since it simply returns the result of the last call to the folding function.