[Haskell-cafe] currying combinators

[wren ng thornton]

Dan Doel wrote:
> On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote:
>> By parametricty, presumably.
> 
> Actually, I imagine the way he proved it was to use djinn, which uses a 
> complete decision procedure for intuitionistic propositional logic. The proofs 
> of theorems for that logic correspond to total functions for the analogous 
> type. Since djinn is complete, it will either find a total function with the 
> right type, or not, in which case there is no such function.
> 
> At that point, all you have left to do is show that djinn is in fact complete. 
> For that, you can probably look to the paper it's based on: Contraction-Free 
> Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy 
> Dyckhoff.

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.


(Sorry, just finished writing a philosophy paper on intuitionism :)

-- 
Live well,
~wren