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-06-24 – hashable arch native
• 2024-05-28 – cabal fields
• 2024-04-21 – A note about coercions
• 2024-04-18 – What makes a good compiler warning?
• 2024-04-12 – Core Inspection

twitter github email linkedin stackoverflow