[Haskell-cafe] currying combinators

[Dan Doel]

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.

-- Dan

[*] http://www.cs.st-andrews.ac.uk/~rd/publications/jsl57.pdf