I was listening at the LambdaConf 2015 talk by Kris Nuttycombe titled Parametricity The Essence of Information Hiding. At 12:20, the speaker talks about why the definition of this function isn't map
, even though it shares the same type signature:
asdf :: forall a b. (a -> b) -> [a] -> [b]
Every value in the output is obtained by applying the function provided to a member of the input.
BUT List gives the implementer too much information, and thecaller too little.
asdf :: forall a b. (a -> b) -> [a] -> [b] asdf f [] = [] asdf f (x : _) = [f x]
Of course, the type signature is the same as map
; however, the result is a singleton list with f
applied to the head.
The speaker says that we should place a Functor
restriction. From that point, I couldn't understand why is that. Could someone give me any pointers?
CodePudding user response:
The speaker is arguing in favor of types. He wants to show the audience that types can under certain circumstances be used to limit possible implementations. When he gets at
asdf :: forall a b. (a -> b) -> [a] -> [b]
he explains that this would allow more than one implmentation but switching to a Functor
constraint would help with that.
asdf :: Functor f => (a -> b) -> f a -> f b
He also seems to split his talk into a first part where he ignores the finer points to get his main message across and a second part where he goes into some of the finer points. For what is worth I share your confusion of the speakers argument in the first part and I would consider it as fast and loose reasoning. I think you should not dig too deep as well.
On a final note, you probably will enjoy Edward Kmett's The free theorem for fmap which also lists the free theorem for fmap
and gives a link to Philip Wadler's Theorems for Free!.