[Haskell-cafe] currying combinators

[wren ng thornton]

Lennart Augustsson wrote:
> Yes, of course you have to trust Djinn to believe its proof.
> That's no different from having to trust me if I had done the proof by hand.
> Our you would have to trust yourself if you did the proof.

True, though I think I didn't make my point clearly.


The question is, when can we consider a proof of (\forall x. ~ P x) as a 
valid *constructive* proof of (~ \exists x. P x)?

If you tell me you've checked every x and found none supporting P, and I 
believe you have the capability to have done so, and I believe things 
you say are true, then I may take your statement that (\forall x. ~ P x) 
and prove to myself that (~ \exists x. P x). However, my proof ---no 
matter how much I believe it--- is not the sort of thing I can pick up 
and hand to someone else. If they do not trust your diligence, then they 
have no reason to trust my proof. I haven't constructed a witness to the 
proposition, I've only convinced myself of it.

If, however, you construct a proof of (\forall x. ~ P x) which shows 
that all options have been exhausted, but does so in a finite way that's 
open to inspection and analysis, well then that's a different story. In 
this case, because we've actually constructed some mathematical object 
that we can poke and prod to understand what it is and how it works, we 
do have something that we can hand to a skeptic to convince them. We 
needn't argue from authority or put our faith in an elder or prophet, 
the proof stands on its own.

When someone says "prove it", it's not always clear whether they mean 
they want to be convinced it's true, or whether they mean they want 
concrete evidence that witnesses its truth. Exhaustive search may be 
convincing, but it's not constructive. When the OP was asking how we'd 
go about proving that no total function exists with a particular type, I 
was assuming they were seeking a witness rather than a convincing. For a 
witness, I'd think you'd have to reason from parametricity, understand 
the process that Djinn is automating, or similar; just running Djinn is 
merely convincing.

-- 
Live well,
~wren