Polymorphic reasoning

Question

I am learning Haskell and in internet I've found is paper from Philip Wadler.
I read it and did not understand at all, but it somehow connects to polymorphic function.

For example:

polyfunc :: a -> a -> a

It is a polymorphic function of any type.

What is the free theorem in connection of the example polyfunc?

Answer 1

I feel like if I actually understood that paper then any code I wrote would be coauthored by God.

My best guess for this problem though is that all polyfunc can do is either always return the first argument or always return the second argument. So there are actually only two implementations of polyfunc,

polyfuncA a _ = a
polyfuncB _ b = b

The paper gives you a way to prove that claim.

This is a very important concept. For example, I've been involved in data quality research previously. This free theorem says that there is no function which can select the best data from two arbitrary pieces of data. We have to know something more. Its actually a no-brainer that I was surprised to find some people willing to overlook.