What is the formalism to prove statements about uniqueness of functions with certain signatures

Question

Suppose I want a function like

f: ((A, B) -> C) -> A -> B -> C

A statement I've often seen made is that f has just one implementation, namely the 'curry function', i.e. g => a => b => g(a, b)

Taken at face value this doesn't seem to actually be true, I can always define f as acting differently from this in special cases, e.g. I can say it is g => a => b => g(a, b) except when A = B and then I define it as g => a => b => g(b, a).

Nonetheless, it's intuitively clear enough what is meant by 'has just one implementation'.

I would like to know the correct formalism in which statements like the above can be proven.

At a guess I would suspect it is category theory? The above feels a bit like the notion of a natural transformation, but I don't really see the details.

Answer 1

I'm sure there is a connection to category theory, but you can actually do it with (what I consider to be ) a simpler tool: parametricity.

They basic idea is that, when a language has the property that polymorphic types do the exact same thing for each type they're instantiated to (i.e. there's no typecase construct), we can prove very powerful properties about the language, in the form of a logical relation.

This prevents exactly the "special case" implementation that you describe in your question. It's also worth mentioning that these implementations are all extensionally equal: they might look different but produce equal results for equal inputs. e.g. you can replace any term $t$ with $(\lambda x \ldotp x) t $ and get an equivalent function.

The statements about functions only from their type are generally called free theorem, named after the paper that introduced the idea: Theorems for Free by Phil Wadler. If you're interested in this area, I highly recommend the paper, since it's a good introduction to the subject.

The idea behind this actually goes much further back than that paper, to John Reynolds work with System F and the "abstraction theorem" but it took a while before the idea became popular.

You can actually generate free theorems at http://free-theorems.nomeata.de/, although it might take a bit of massaging to get useful information from the theorems they give there.

If you're interested in parametricity used to prove things other than free theorems, like type safe, then Amal Ahmed's thesis is the best introduction I've seen. She really does a good job of describing semantic types: the type of a program is actually a property of how it runs and what it produces, and what we call "types" are a syntactic approximation of these more general semantic types.