[Haskell-cafe] currying combinators
wren ng thornton
wren at freegeek.org
Fri May 28 02:14:20 EDT 2010
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
More information about the Haskell-Cafe
mailing list