This is a question from book "Haskell Programming from First Principles".
I am reading the above mentioned book, On chapter 5, Number 2 of Exercises: Parametricity.
Copied from the book.
We can get a more comfortable appreciation of parametricity by looking at a -> a -> a. This hypothetical function a -> a -> a has two–and only two–implementations.
I do not understand "only two–implementations" part? can any one explain to me why only 2 implementations?
I think the word "implementations" can be a bit confusing at first glance.
Say we have only the function type
f :: a -> a -> a, and no other information; we're not allowed to peek inside
f. The function must return an
a and you only have 2 possible
a's as input. Therefore the function must return the first
a or the second
a; only 2 possible functions.
You cannot have
f x y = x + y because you do not know how to
a's just given that
f :: a -> a -> a. If you have, say
h :: Int -> Int -> Int, then
h x y = x + y would be a valid function, but you are not given that information for
Similarly, what if you have
f :: a -> a -> a and you claim
f x y = x + y is valid. Then I can break your claim by passing two
f Apple Orange = ???. Well
Apple + Orange is ambiguous and the code wont work. So keeping the type polymorphic "restricts" the possible functions to 2 possible "implementations":
f x y = x or
f x y = y.
This video helped me understand. I'd recommend the whole video but the link is to the relevant part. (31:28)
It demonstrates the power of type-level reasoning and parametricity. All the information for such reasoning is in the type.
Another example, say all you have is a function type
g :: b -> b. Well, the function must return a
b, and the only argument is a
b so it must return that
b. Thus, there is only one such function with type
b -> b.