Djinn can't figure it out, and neither can I :P 2010/5/25 Günther Schmidt

Hi Yitz,

embarrassingly I was unable to deduce the implementation from the type signature, don't be tease man, show me what you got :)

Günther

Am 25.05.10 18:27, schrieb Yitzchak Gale:

Günther Schmidt wrote:

...

...

http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=25694 in which I attempt to develop a "currying combinator" library. I'm stuck at some point and would appreciate any help.

How about this:

keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b

so then

nameZip = keep (drop' . drop') names

Regards, Yitz

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I wrote:

...

keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b so then nameZip = keep (drop' . drop') names

Günther Schmidt wrote:

don't be tease man, show me what you got :)

Ivan Miljenovic wrote:

...

Methinks Yitzchak made a typo

Yes, sorry about that. Tested in ghci this time :). keep :: (forall c . (t -> c) -> u -> c) -> ((t1 -> t) -> b) -> (t1 -> u) -> b keep transform rec = \fn -> rec $ transform id . fn Regards, Yitz

There are no interesting (i.e. total) functions of that type. 2010/5/25 Yitzchak Gale :

Günther Schmidt wrote:

...

http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=25694 in which I attempt to develop a "currying combinator" library. I'm stuck at some point and would appreciate any help.

How about this:

keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b

so then

nameZip = keep (drop' . drop') names

Regards, Yitz _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

David Sankel wrote:

keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b

On Wed, May 26, 2010 at 12:49 PM, Lennart Augustsson

...

wrote:

...

There are no interesting (i.e. total) functions of that type.

I wonder how one would prove that to be the case. I tried and didn't come up with anything.

By parametricty, presumably. We must ultimately construct some value of type b, where b is universally quantified. Therefore, the only 'constructors' available for b are the ((t -> b) -> u -> b) and ((t1 -> t) -> b) arguments. However, since b is universally quantified, these arguments have no way of actually constructing some b, other than by returning bottom. Remember, if a language lacks typecase, (forall a. X -> a) is just another way of saying (X -> Void). -- Live well, ~wren

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

Dan Doel wrote:

On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote:

...

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.

How, exactly, is it non-constructive to encode the propositional calculus and its proofs as, say, types in intuitionistic type theory, write the algorithm djinn uses in the same (it was specially crafted to be provably terminating, after all), and prove the algorithm complete (again, hopefully in the type theory)? I realize this has not all been done, strictly speaking, but I see nowhere that it is necessarily non-constructive.

All I'm saying is that a proof of (\forall x. ~ P x) does not constitute a proof of (~ \exist x. P x) for some intuitionists. The issue is one of the range of quantification and whether \forall truly exhausts every possibility. The BHK interpretation says the two propositions are the same, but others say the latter is a stronger claim. If you believe that Djinn truly does exhaust the search space, then it's fine to convert Djinn's proof of (\forall x. ~ P x) into a proof of (~ \exist x. P x). However, that just pushes the question back to why you feel justified in believing that Djinn truly exhausts the search space. I'm not saying you shouldn't believe in Djinn, I'm saying that belief in Djinn is not justification for a theorem unless you have justification for believing in Djinn. -- Live well, ~wren

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

On 28 May 2010, at 08:47, Lennart Augustsson wrote:

Yes, of course you have to trust Djinn to believe its proof. That's no different from having to trust me if I had done the proof by hand. Our you would have to trust yourself if you did the proof.

BTW, Djinn does not do an exhaustive search, since there are infinitely many proofs. (Even if you just consider cut free proofs there's usually infinitely many.)

Just to flesh out the thought, let me sketch completeness (the result is due to Roy Dyckhoff). Fortunately, an exhaustive search is not necessary for completeness in this logic. Let's say that a "cycle" in a proof is where some atomic proposition P is derived by a proof tree which includes internal derivations of P ... ----- P ...... --------------------- P Of course, you can simplify such a proof by replacing the larger P-proof with the smaller. If a proposition has a proof, then it has a cycle-free proof. An exhaustive search of the cycle-free proofs is thus complete. But can we implement such a search? Given that an assumption can prove at most one atomic formula (an assumption which does not hold in *predicate* logic), you can be sure that any path in a proof tree which uses the same assumption twice creates a cycle. Correspondingly, you can be sure that in each branch of a proof, you can discard the assumptions you've already used. That's enough of a "resource bound" to ensure that an exhaustive search of the cycle-free proofs will terminate. (You can acquire new assumptions when you backchain on a higher-order assumptions, but the new assumptions are two orders lower than the assumption disposed of, so you can readily construct an order-based lexicographic termination scheme (shameless plug for my PAR2010 talk).) So, there's some reason to believe that there is a complete algorithm, which might even be the one Lennart implemented in Djinn. All the best Conor

On Fri, May 28, 2010 at 8:14 AM, wren ng thornton wrote:

...

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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

wren ng thornton wrote:

David Sankel wrote:

...

keep :: ((t -> b) -> u -> b) -> ((t1 -> t) -> b) -> (t1 -> u) -> b

Lennart Augustsson wrote:

...

There are no interesting (i.e. total) functions of that type.

I wonder how one would prove that to be the case. I tried and didn't come up with anything.

By parametricty, presumably.

We must ultimately construct some value of type b, where b is universally quantified. Therefore, the only 'constructors' available for b are the ((t -> b) -> u -> b) and ((t1 -> t) -> b) arguments. However, since b is universally quantified, these arguments have no way of actually constructing some b, other than by returning bottom.

Er, that's not quite right. That's only true if those arguments are rank-2 quantified. I'd had a longer (correct) explanation and tried shortening it. So here's the better proof: In order to produce a value of type b, keep must either use one of those two arguments or return bottom. If it uses the ((t -> b) -> u -> b) argument, then keep can only return non-bottom if that function [1] ignores its arguments and returns an arbitrary b, or [2] uses the (t -> b) argument to construct the b. If we assume #1 then keep is not total, because we have no way of proving that the assumption is valid. So we must expect #2; so in order for keep to be total it must be able to construct a total function (t -> b). In order to construct such a function it must use one of the original two arguments, so this is only possible if we can construct a b via ((t1 -> t) -> b). If it uses the ((t1 -> t) -> b) argument, then keep can only return non-bottom if that function [1] ignores its arguments, or [2] uses the (t1 -> t) argument. We can't assume #1 and be total, so we must expect #2. In order to construct (t1 -> t) we must construct a t. But, since t is universally quantified, keep knows of no total functions which return t. Thus, keep can only construct a function which returns bottom. Thus, keep can only return non-bottom under the assumption that the ((t -> b) -> u -> b) and ((t1 -> t) -> b) arguments ignore their arguments to return a constant b. -- Live well, ~wren