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

Posted on 2015-09-15 by Oleg Grenrus

### 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

Site proudly generated by Hakyll