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.
True, though I think I didn't make my point clearly.
The question is,
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 searc
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 jus
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 fo
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
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
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
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
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.
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 function
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
wit
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.
David
--
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.
>
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
n
Hi all,
I've posted some code on hpaste
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.
Günther
___
Haskell-Cafe mailing l
15 matches
Mail list logo