• A+
Category：Languages

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 `+` two `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 `f`.

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 `Fruit`s to `f`: `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`.