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

### The Question

We know that forall a. a -> a has only one element: id = \x -> x. How to show it for more complicated type, like: (b -> a) -> (a -> b -> c) -> b -> c

### The answer

• You can apply sequent calculus
• Or you can use Yoneda lemma -approach with smart choices of functors.

Read rest the rest on StackOverflow

• 2024-04-18 – What makes a good compiler warning?
• 2024-04-12 – Core Inspection
• 2024-04-01 – Implicit arguments
• 2024-03-17 – ST with an early exit
• 2024-02-27 – More QualifiedDo examples

twitter github email linkedin stackoverflow