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

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!

• Not 100% sure cause I lack the context, but here goes. If you were asked to supply (perhaps as a parameter to a higher order function) a function with the signature `(a,b) -> a`, you could find one that returns any value of type `a` (including a value that's different from the one in the tuple). But when it comes to implementing a function of that signature on the generic tuple type itself, since the types of the constituents are parameterized and unconstrained, you have no other way (in general) of producing a value of type `a`, other than taking the one you were supplied with. Commented Feb 1, 2022 at 17:38
• Ah, so that is probably where my misconception comes from. Mathematically speaking, there might be many such functions (at least if we believe in a sufficiently strong version of the axiom of choice and dont worry about running into inconsistencies with classes), but here the functions need to be implemented by one piece of code, so the typical "you can't write them down, but they still exist mathematically"-functions are not present? If I imagine actually having to implement such a function, then of course I dont know how to do it. How would one show the infeasibility, though? Commented Feb 1, 2022 at 17:44
• Parametric polymorphism implies that any polymorphic function between two functors is a natural transformation, including `fst`. Commented Feb 1, 2022 at 18:04
• I don't think you have to give that up; it's not the fact that you need to write them down that's in itself the problem. E.g. you can implement (write down) `(Int, Bool) -> Int` that always returns 0, and plug it somewhere where `(a, b) -> a` is required. It's just that when you have to implement a function that works on a completely generic, parameterized type such as "(a, b)" and returns an "a" that your options become limited. Now, I have a superficial understanding of Haskell, so I don't know if they become as limited as to justify the claim - maybe someone can chime in with more detail. Commented Feb 1, 2022 at 18:12
• @J.Becker `(, b)` and `Identity`, i.e. `fmap f (a, b) = (f a, b)` and `fmap = id`. Part 10 of Bartoz Milewski's Categories for Programmers discusses this in more detail. Commented Feb 1, 2022 at 19:09

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.

• Statements like the one in the question generally assume "no shenanigans", i.e. they assume totality, no side-effects, etc. In Haskell, that means no bottom, no `unsafePerformIO`, and friends. Commented Feb 1, 2022 at 21:11
• @JörgWMittag Yes, but `undefined` is a direct consequence of Haskell's type inference + laziness.
– amon
Commented Feb 1, 2022 at 21:35
• We generally say "up to bottom" and wave our hands a bit. Commented Feb 1, 2022 at 23:06