1

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!

7
  • 1
    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. Feb 1 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?
    – J. Becker
    Feb 1 at 17:44
  • 1
    Parametric polymorphism implies that any polymorphic function between two functors is a natural transformation, including fst. Feb 1 at 18:04
  • 1
    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. Feb 1 at 18:12
  • 1
    @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. Feb 1 at 19:09

1 Answer 1

3

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.

3
  • 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. Feb 1 at 21:11
  • @JörgWMittag Yes, but undefined is a direct consequence of Haskell's type inference + laziness.
    – amon
    Feb 1 at 21:35
  • We generally say "up to bottom" and wave our hands a bit. Feb 1 at 23:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.