My first thought when I read this title was that there should be a site like Hoogle for mathematical proofs, where one could search by type signature for existing proofs. I'm not sure if people often think of proofs in terms of their type signature, but by Curry-Howard it would be doable.