Regarding Haskell's Parametricity concept

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

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: