How do you prove that a function is unique for its type?

Question

id is the only function of type a -> a, and fst the only function of type (a,b) -> a. In these simple cases, this is fairly straightforward to see. But in general, how would you go about proving this? What if there are multiple possible functions of the same type?

Alternatively, given a function's type, how do you derive the unique (if this is true) function of that type?

Edit: I'm particularly interested in what happens when we start adding constraints into the types.

Answer 1

The result you are looking for derives from Reynolds' parametricity, and was most famously shown by Wadler in theorems for free.

The most elegant way of proving basic parametricity results I have seen use the notion of a "Singleton Type". Essentially, given any ADT

data Nat = Zero | Succ Nat

there exists an indexed family (also known as a GADT)

data SNat n where
   SZero :: SNat Zero
   SSucc :: SNat n -> SNat (Succ n)

and we can give a semantics to our language by "erasing" all the types to an untyped language such that Nat and SNat erase to the same thing. Then, by the typing rules of the language

id (x :: SNat n) :: SNat n

SNat n has only one inhabitant (its singleton), since the semantics is given by erasure, functions can not use the type of their arguments, so the only value returnable from id on any Nat is the number you gave it. This basic argument can be extended to prove most of the parametricity results and was used by Karl Crary in A Simple Proof Technique for Parametricity Results although the presentation I have here is inspired by Stone and Harper