[Haskell-cafe] currying combinators

[Lennart Augustsson]

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?
As I understand, in general this can only be proven using meta theory
rather than the logic itself (it could happen that the given formula
implies absurdity, and then we'd know it can't be proven, given that
the logic is consistent).
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.

   -- Lennart

On Thu, May 27, 2010 at 7:49 PM, wren ng thornton <wren at freegeek.org> wrote:
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>