In what sense are functions like fst and snd determined uniquely by their type signature in Haskell?

Question

I have recently given Haskell another go, mostly because I heard about the book Haskell from first principles and so far I'm having a blast. My background is that of a mathematician mostly working in Algebra, so I usually understand the categorical aspects decently, but I could not quite grasp the following specific claim. On p.163 of Haskell from first principles, it is claimed that the functions

fst :: (a,b) -> a
snd :: (a,b) -> b

are uniquely determined by their type signature.

Now, I feel like this is not true without some further naturality, compatibility or universality requirements that uniquely determine the explicit realisations of fst and snd given bindings of a and b to explicit types.

So my question is: What properties are fst and snd assumed to possess that indeed determine them uniquely?

I feel like I got a rough handwavy understanding of what is meant. If we want fst and snd to somehow "behave the same way" no matter which types we choose for a and b, then it feels like we indeed have no other choice but given an inhabitant of (a,b) return its constituents. However, I don't know what precisely is meant here.

At first glance, it might remind one of the categorical product in the category of sets, but the product already comes together with its two projection maps. Now of course we could say "fst and snd are already uniquely determined if we want the triple ( (a,b), fst, snd) ) to satisfy an analogon of the universal property of the categorical product", but that is a rather weak claim and certainly not what is said in the book.

Another idea is that maybe we want fst and snd to be compatible with maps in the sense that if f :: a -> b is any function, then we might want something like f a = fst.(f -*- id ) (a,undefined) to hold. (Or maybe undefined instead of id as well, but that shouldnt matter since we discard it anyway).

Any help is appreciated!

Answer 1

As a simpler example, we can consider the function id :: a -> a. For any type a, this function takes an a value and returns an a value. However, a is not constrained by any typeclasses – meaning we can't do anything with that type. We can't even create new values. So the only way for id to evaluate to a value of type a is to return the value that was given.

id x = x

Technically, there is another way because there is undefined :: a – an expression that has any type. Thus, undefined servers as a kind of “bottom instance” in Haskell. However, undefined never actually evaluates to a value, and trying to evaluate it will lead to an error. An undefined expression can be defined via the tautology undefined = undefined. So technically, we could alternatively define id _ = undefined. Such a function could also inhabit a type a -> b, though it could never be evaluated successfully.

By the same argument that id :: a -> a is defined uniquely (leaving aside degenerate cases like those involving undefined), it must be the case that a function fst :: (a,b) -> a only has one unique definition. It can't create a new a value and can't use the b value in place of a, so it must evaluate to the first tuple element. In contrast, fst :: (a,a) -> a would not have an unique definition because the implementation has a choice of using either the first or the second tuple element.