Regarding Haskell's Parametricity concept

3
votes

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?

1
haskell
I'm not sure I can explain formally, but just try to think up ways you could implement a function that, given two elements of the same type, produces a single one of that type - for every conceivable type. The two possible implementations are rather obvious, and (speaking informally) there is "nothing else you can do" because you can't assume anything about the values the function takes, as you don't know anything about their type. - Robin Zigmond
\nf x y = x f x y = y f x y = x + y\n,so i have defined 3 functions - Software Wisdom
the last one doesn't have type a -> a -> a but Num a => a -> a -> a. - Li-yao Xia
Suppose I give you two boxes, and I tell you that the things in these boxes are the same type of thing, but I don’t tell you what they are. Now I ask you to give me back something of that same type, deterministically (no using IO to flip a coin) and “honestly” (no breaking open a box to see what’s inside, no lying to me about what you gave me, no running away with the boxes and never returning). Since you know nothing about what’s in the boxes, you can’t just make something of that type—you must give me back one of the boxes I gave you, and you only have two possible choices. - Jon Purdy
@JonPurdy, that explanation is pretty good, thanks - Software Wisdom

1 Answers

13
votes

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 Fruits 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.