Utterly Pointless Update

A quick update on my previous post, Utterly Pointless. I showed the same problem to my brother, who at first concluded the same thing that I did, but later raised the question as to why the first and third arguments have to be of the same type. His argument was that the polymorphic nature of the type parameters meant that they could take on different type signatures in different contexts. If we deconstruct the definition of f and uncurry it, we arrive at the equality

f(x,y,z) = const(y,f(z))

where const is a function that returns its first argument and ignores its second argument. Since we can call f with a first argument of type elephant, or a first argument of type giraffe, why do x and z have to both be elephants or both be giraffes?

While I am in no way an expert or by any means well-acquainted with Haskell's type inference system, my guess is that when Haskell is trying to construct a type for f from scratch, it assumes that f must be of a fixed type, and lets the polymorphism enter after it decides what relationship should exist between the various types in f's type signature.

>After my father lectured me for a brief while about category theory, and I was still unable to find a reason why the first and third arguments should have to be the same type, I decided to explicitly write out my brother's more general type for f, namely

f :: a -> b -> (c -> b)

Surprisingly, Haskell was completely okay with this type signature for the same definition, and allowed me to pass first and third arguments of different types, whereas it complained when I tried to do so without the custom signature. My theory is this: Haskell has no way of knowing that it might assume the more general type, so it starts out the same way that I did in my previous post. This more general signature is perfectly valid, and can be verified to be valid, but it cannot be constructed from scratch. If you give a mathematician an attempted proof of Goldbach's conjecture, they will probably be able to tell you whether it is a valid and complete proof, but no mathematician thus far has been able to construct a proof. I know that this analogy is getting the Curry-Howard isomorphism completely backwards, but I hope it at least gets my point across. 

If anyone has insight into what is happening here inside the type inference system and the type checking system, or about any aspect of this seeming paradox, please leave a comment. As usual, the comments section is also open to comments/criticisms/heckling.

EOF