How do I show that a Haskell type is inhabited by one and only one function?

Question

In this answer, Gabriel Gonzalez shows how to show that id is the only inhabitant of forall a. a -> a. To do so (in the most formal iteration of the proof), he shows that the type is isomorphic to () using the Yoneda lemma, and since () has only one value in it, so must the type of id. Summarized, his proof is like this:

Yoneda says:

Functor f => (forall b . (a -> b) -> f b) ~ f a

If a = () and f = Identity, this becomes:

(forall b. (() -> b) -> b) ~ ()

And since trivially () -> b ~ b, the LHS is basically the type of id.

This feels like a bit of a "magic trick" that works well for id. I'm trying to do the same thing for a more complex function type:

(b -> a) -> (a -> b -> c) -> b -> c

but I have no idea where to start. I know it is inhabited by \f g x = g (f x) x, and if you ignore ugly ⊥/undefined stuff, I'm pretty sure there are no other functions of this type.

I don't think Gabriel's trick will immediately apply here whichever way I pick the types. Are there other approaches (that are equally formal!) with which I can show the isomorphism between this type and ()?

Answer 1

You can apply sequent calculus.

Short example, with type a -> a, we could construct term like: \x -> (\y -> y) x, but that still normalises to \x -> x which is id. In sequent calculus the system prohibites from constructing "reducable" proofs.

Your type is (b -> a) -> (a -> b -> c) -> b -> c, informally:

f: b -> a
g: a -> b -> c
x: b
--------------
Goal: c

And there aren't many ways to proceed:

apply g

f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0: a
Subgoal1: b


apply f

f: b -> a
g: a -> b -> c
x: b
---------------
Subgoal0': b
Subgoal1: b


-- For both
apply x

So in the end, seems that g (f x) x is the only inhabitant of that type.

---

Yoneda lemma approach, have to be careful to actually have forall x!

 (b -> a) -> (a -> b -> c) -> b -> c
 forall b a. (b -> a) -> b -> forall c. (a -> b -> c) -> c

Let concentrate on the end:

 (a -> b -> c) -> c ~ ((a,b) -> c) -> c

That is isomorphic to (a, b), so whole type reduces to

(b -> a) -> b -> (a, b)

Take f = Compose (Reader b) (,b)

(b -> a) -> f a ~ f b ~ b -> (b,b)

And that is unique by taking HP a = (a,a) functor:

b -> (b,b) ~ (() -> b) -> HP b ~ HP () ~ ()

---

EDIT the first approach feels a bit more hand-wavy, but feels somehow more direct: Given the restricted set of rules, how the proof can be constructed, how many proofs we can construct?