Is there a universal identity or zero value for folding?

Question

I'm using Haskell notation for illustration, hopefully it is known widely enough for this to make sense.

In the following fold function the second argument is what I'm calling the identity:

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b

It is trivial to fold/reduce over a list of values with certain operations such as addition or multiplication. e.g.

mySum :: (Num a, Foldable t) => t a -> a
mySum = foldr (+) 0   --NB. Works because 0 is the additive identity

myProduct :: (Num a, Foldable t) => t a -> a
myProduct = foldr (*) 1  --NB. Works because 1 is the multiplicative identity

But not all operations have an obvious identity value.

My question is whether there is such thing as a universal identity value, or a function whereby you can find the identity value, or if you can contrive a scheme so that there now is one.

i.e. can you somehow define a z value such that:

foldrUniversal :: Foldable t => (a -> b -> b) -> t a -> b
foldrUniversal f = foldr f z

or could you have a function that determines it:

findIdentity :: (a -> b -> b) -> z  --is this possible?

foldrUniversal f = foldr f (findIdentity f)

or can you use some trick so that you always have an identity value even if you don't know what it should be?

(Note that I'm not stuck on a programming problem. I already know about foldr1 in Haskell, or using the head of the list as the identity and then the tail of the list as the list argument. I posted in cs.stackexchange instead of StackOverflow because I'm interested in the theoretical possibilities.)

Answer 1

There's no universal identity for folding. It it in fact visible from your examples with + and *: how could you infer that + needs 0 but * needs 1? In order to find this out, it is necessary to analyze + and * sufficiently to find how they differ. If the compiler has some knowledge of + and *, this might be doable. But if you generalize the example to any primitive function, or any function defined in Haskell but which the compiler isn't able to analyze, then the compiler won't be able to tell the difference between + and *, so there's no way it could come to different conclusions regarding the identity.

Another way to see that there's no universal identity is that sometimes, there is no identity. For example, if you had a type of positive integers (integers $\gt 0$) and the operation +, then there would be no identity. Another example that's perhaps more intuitive for a programmer: for string concatenation, the identity is the empty string "". But if you define an operation that concatenates with an explicit separator (e.g. cat x y = x + "," ++ y), that one has no identity.

It is possible however to force a universal identity, i.e. to pull an object out of thin air and declare that it will be an identity. (This use of the word force comes from mathematics.) The way to do this is to add a level of indirection — as every programmer knows, you can solve¹ any problem by adding a level of indirection. Instead of folding over values of the original type, you fold over a value that is either a value of the original type, or the identity. In other words, an option.

fold_with_identity :: Foldable t => (a -> b -> b) -> t a -> Maybe b
fold_with_identity f xf = fold_list (toList xf) where
                            fold_list [] = Nothing
                            fold_list x0:xs = Just (foldr f x0 xs)

There's no such thing as a free lunch, so obviously this doesn't actually solve the problem — it just moves it to the next level. You may get Nothing out of this and you have to know which value to convert it, if there's a value to convert it to.

¹ _{almost. Offer void where prohibited by law or by the type system. One per customer if using linear logic. Consult a PhD if the symptoms persist.}

Answer 2

Assume we can define

foldrUniversal :: Foldable t => (a -> b -> b) -> t a -> b

Then,

foo :: b
foo = foldrUniversal (\x y -> y) []

Is a way to form a value for any type b. If the type system is sane, this implies that foo does not terminate, as if we recursively defined foo = foo. Otherwise, all the types would be inhabited, making the logic associated to the type system to be inconsistent. A type system that allows this would be regarded as essentially "broken".

In real world languages, we do (grudgingly) allow some unwanted inhabitants. Non-terminating values ("bottom") are common ones, since they are mandatory in language with unconstrained recursion. null values are also used in many OOP based languages -- this is a so-called "billion dollar mistake", and should be avoided. Having a way to craft a "real" value of type b (say non-null, non-bottom) from nothing is too much.