[Haskell-cafe] currying combinators

[wren ng thornton]

Lennart Augustsson wrote:
> So what would you consider a proof that there are no total Haskell
> functions of that type?
> Or, using Curry-Howard, a proof that the corresponding logical formula
> is unprovable in intuitionistic logic?


It depends on what kind of proof I'm looking for. If I'm looking for an 
informal proof to convince myself, then I'd probably trust Djinn. If I'm 
trying to convince others, am deeply skeptical, or want to understand 
the reasoning behind the result, then I'd be looking for a more rigorous 
proof. In general, that rigorous proof would require metatheory (as you 
say)--- either my own, or understanding the metatheory behind some tool 
I'm using to develop the proof. For example, I'd only trust Djinn for a 
rigorous proof after fully understanding the algorithms it's using and 
the metatheory used to prove its correctness (and a code inspection, if 
I didn't trust the developers).


> If Djinn correctly implements the decision procedure that have been
> proven to be total (using meta theory), then I would regard Djinn
> saying no as a proof that there is no function of that type.

So would I. However, that's adding prerequisites for trusting Djinn--- 
which was my original point: that Djinn says there isn't one is not 
sufficient justification for some folks, they'd also want justification 
for why we should believe Djinn actually does exhaust every possibility.

-- 
Live well,
~wren