[Haskell-cafe] currying combinators

[Dan Doel]

On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote:
> Sure, that's another option. But the failure of exhaustive search isn't
> a constructive/intuitionistic technique, so not everyone would accept
> the proof. Djinn is essentially an implementation of reasoning by
> parametricity, IIRC, so it comes down to the same first principles.

How, exactly, is it non-constructive to encode the propositional calculus and 
its proofs as, say, types in intuitionistic type theory, write the algorithm 
djinn uses in the same (it was specially crafted to be provably terminating, 
after all), and prove the algorithm complete (again, hopefully in the type 
theory)? I realize this has not all been done, strictly speaking, but I see 
nowhere that it is necessarily non-constructive.

If you point is that the result you get is:

  ¬ ⊢ (...)

instead of 

  ⊢ ¬ (...)

then this is true, but the former is what was originally claimed (there are no 
total functions of that type ==> that proposition is not a theorem). In fact, 
if one can prove the second, then we're in trouble, because the proposition is 
a classical theorem, and djinn provides a result for

  ⊢ ¬ ¬ (...)

which contradicts the second statement above.

-- Dan