CODEWITHSUNDEEP
haskell
Software Wisdom
Software Wisdom

Reputation: 105

Regarding Haskell's Parametricity concept

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?

Upvotes: 5

Views: 473

Answers (2)

Dave Sands
Dave Sands

Reputation: 1

There are five functions (up to observational equivalence in the pure expression (non-IO) part of Haskell) which have the most general type a -> a -> a.

f0 a b = f0 (f0 b a) (f0 a b) 

f1 a b = if True then a else b

f2 = flip f1

f3 a b = seq a (f2 a b)

f4 = flip f3

Upvotes: 0

dopamane
dopamane

Reputation: 1315

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.

Upvotes: 14

Related Questions