Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Any function with the same polymorphic type as fmap must be equal to fmap?

I'm reading the second edition of Programming in Haskell and I've came across this sentence:

... there is only one way to make any given parameterised type into a functor, and hence any function with the same polymorphic type as fmap must be equal to fmap.

This doesn't seem right to me, though. I can see that there is only one valid definition of fmap for each Functor type, but surely I could define any number of functions with the type (a -> b) -> f a -> f b which aren't equivalent to each other?

Why is this the case? Or, is it just a mistake by the author?

like image 987
Zac Avatar asked Dec 05 '22 10:12

Zac


2 Answers

You've misread what the author was saying.

...any function with the same polymorphic type as fmap...

This means, any function with the signature

Functor f => (a -> b) -> f a -> f b

must be equivalant to fmap. (Unless you permit bottom values, of course.)

That statement is true; it can be seen quite easily if you try to define such a function: because you know nothing about f except that it's a functor, the only way to obtain a non-⊥ f b value is by fmapping over the f a one.

What's a bit less clear cut is the logical implication in the quote:

there is only one way to make any given parameterised type into a functor, and hence any function with the same polymorphic type as fmap must be equal to fmap.

I think what the author means there is, because a Functor f => (a -> b) -> f a -> f b function must necessarily invoke fmap, and because fmap is always the only valid functor-mapping for a parameterised type, any Functor f => (a -> b) -> f a -> f b will indeed also in practice obey the functor laws, i.e. it will be the fmap.

I agree that the “hence” is a bit badly phrased, but in principle the quote is correct.

like image 174
leftaroundabout Avatar answered May 23 '23 07:05

leftaroundabout


I think that the quote refers to this scenario. Assume we define a parameterized type:

data F a = .... -- whatever

for which we can write not only one, but two fmap implementations

fmap1 :: (a -> b) -> F a -> F b
fmap2 :: (a -> b) -> F a -> F b

satisfying the functor laws

fmap1 id = id
fmap1 (f . g) = fmap1 f . fmap1 g
fmap2 id = id
fmap2 (f . g) = fmap2 f . fmap2 g

Under these assumptions, we have that fmap1 = fmap2.

This is a theoretical consequence of the "free theorem" associated to fmap's polymorphic type (see the comment under Lemma 1). Pragmatically, this ensures that the instance we obtain from deriving Functor is the only possible one.

like image 24
chi Avatar answered May 23 '23 08:05

chi