On Fri, 2007-10-19 at 00:02 +0200, [EMAIL PROTECTED]
wrote:
Dan Weston writes:
... now I am totally flummoxed:
thm1 :: (a - a) - a
thm1 f = let x = f x in x
thm1 (const 1)
1
I *thought* that the theorem ((a = a) = a) is not derivable (after all,
0^(0^0) = 0^1 = 0),
Derek and Lennart,
Thank you both for your clarifications. Tutorials (and blogs) of the C-H
correspondence and the naive (i.e. set-theoretic) categorical
descriptions of Haskell are so eager to get to the insights you mention
that they gloss too easily over the important role of _|_, a term I
I must confess that I find choosing
type Prop = CProp ()
to be slightly dangerous, since now
CProp (const ()) :: Prop p
and there is nothing in that expression that suggests non-termination (~
invalid proof).
I would rather choose a type admitting only _|_ as its value:
type Prop =
On Wed, 2007-10-17 at 15:06 -0700, Dan Weston wrote:
That is a great tutorial. Thanks! But in the last two sentences of the
introduction you say:
We just need to find any program with the given type.
The existence of a program for the type will be a proof
of the corresponding
There's nothing wrong with Haskell types. It's the terms that make Haskell
types an inconsistent logic.
But that doesn't mean that the C-H correspondence doesn't have any insight
to offer.
-- Lennart
On 10/21/07, Derek Elkins [EMAIL PROTECTED] wrote:
On Wed, 2007-10-17 at 15:06 -0700, Dan
Hello,
On 10/17/07, Lennart Augustsson [EMAIL PROTECTED] wrote:
Check Wikipedia. Peirce law, law of excluded middle, double negation, ...
they are all equivalent and it can be instructive to see how one can derive
one from the other.
Apparently these axioms are not all equivalent (I was
On Mon, 2007-10-22 at 01:12 +0100, Lennart Augustsson wrote:
There's nothing wrong with Haskell types. It's the terms that make
Haskell types an inconsistent logic.
Logics are what are consistent or not, so saying the logic Haskell's
type system corresponds to is inconsistent is all that can
Thank you for that clarification, and I hope you will have patience for
a follow-up question. I am really eager to fully understand this
correspondence and appreciate any help.
Your strong normalization induction does deconstruct function
application but seemingly not constructor application,
I'm fairly new to this and struggling to follow along so I might
be a little off base here...
I assume you mean then that it is a valid proof because it halts for *some*
argument? Suppose I have:
thm1 :: (a - a) - a
thm1 f = let x = f x in x
There is no f for which (thm1 f) halts (for the
The function needs to be total. You seem to be using Haskell to execute
a function to see if it terminates as a proof of totality. Is that
fair? This approach might work for some simple examples, but if the
function doesn't terminate immediately then what? I would assume that
proof of
Tim Newsham quotes somebody /I didn't follow this thread!/:
I assume you mean then that it is a valid proof because it halts for
*some* argument? Suppose I have:
thm1 :: (a - a) - a
thm1 f = let x = f x in x
There is no f for which (thm1 f) halts (for the simple reason that _|_ is
the
It was I that he quoted, and now I am totally flummoxed:
thm1 :: (a - a) - a
thm1 f = let x = f x in x
thm1 (const 1)
1
I *thought* that the theorem ((a = a) = a) is not derivable (after
all, 0^(0^0) = 0^1 = 0), but it appears somehow that thm1 is a proof of
its type.
Help, I just
Dan Weston writes:
... now I am totally flummoxed:
thm1 :: (a - a) - a
thm1 f = let x = f x in x
thm1 (const 1)
1
I *thought* that the theorem ((a = a) = a) is not derivable (after all,
0^(0^0) = 0^1 = 0), but it appears somehow that thm1 is a proof of its
type.
Help, I just
On Tue, Oct 16, 2007 at 08:03:52PM -1000, Tim Newsham wrote:
A tutorial on the Curry-Howard Correspondence in Haskell:
http://www.thenewsh.com/%7Enewsham/formal/curryhoward/
Feedback appreciated.
Very clear and useful for me. Thank you for sharing it.
Andrea
Tim Newsham wrote:
A tutorial on the Curry-Howard Correspondence in Haskell:
http://www.thenewsh.com/%7Enewsham/formal/curryhoward/
Nice!
Perhaps you should add a link to this on the wiki:
http://haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence
Thanks,
Yitz
Tim,
I have also enjoyed the article, it's well written and easy enough to
follow (at least for me).
Slightly offtopic - I am curious about the use of forall in some type
signatures:
subsume :: forall p q r. Prop (p := q) - Prop ((p :/\ q) :== p)
subsume pIMPq = equivInj (impInj pq2p) (impInj
Very clear tutorial indeed. But why isn't propCC shown as Pierce's
Law? And Excluded middle is proven on such basis.
Vitaliy.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Slightly offtopic - I am curious about the use of forall in some type
signatures:
If you specify the forall p q at the top level then the types
used internally will use the same p and q. Otherwise the
internal types will be new ps and qs and wont line up with
the outer type declaration.
Very clear tutorial indeed. But why isn't propCC shown as Pierce's
Law? And Excluded middle is proven on such basis.
Simply because I don't know that much about pierce's law. I've
seen it mentioned a few times, but I'm not that familiar with it
yet and I haven't read a good treatment of it
Check Wikipedia. Peirce law, law of excluded middle, double negation, ...
they are all equivalent and it can be instructive to see how one can derive
one from the other.
On 10/17/07, Tim Newsham [EMAIL PROTECTED] wrote:
Very clear tutorial indeed. But why isn't propCC shown as Pierce's
Law?
That is a great tutorial. Thanks! But in the last two sentences of the
introduction you say:
We just need to find any program with the given type.
The existence of a program for the type will be a proof
of the corresponding proposition!
Maybe you should make explicit that
1) the type is
Also, I was wondering if the constructor and/or function arguments
should be marked strict.
Otherwise, types can be inhabited by defined arguments. Since Prop is
not strict in its argument, we could have the (false) theorem
andAlwaysTrue :: forall p q . p :/\ q
andAlwaysTrue p q = And (Prop
Tim Newsham writes:
A tutorial on the Curry-Howard Correspondence in Haskell:
http://www.thenewsh.com/%7Enewsham/formal/curryhoward/
Feedback appreciated.
Did I miss it (then I apologize), or that tutorial doesn't even mention
Djinn (in which case the Author should).
Jerzy Karczmarczuk
On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote:
2) the function must halt for all defined arguments
fix :: forall p . (p - p) - p
fix f = let x = f x in x
consider:
foo :: ((a - a) - a) - a
foo x = x id
foo is a valid proof of a true theorem, but does not halt for the
defined
_|_ does not provide a witness to a theorem in any consistent logic
(otherwise everything could be proved from it), yet it inhabits every
type in Haskell. If the only invalid type instance is _|_, then a
necessary and sufficient test for the C-H correspondence be the
existence of a type
It would seem that this induction on SN requires strictness at every
stage. Or am I missing something?
Stefan O'Rear wrote:
On Wed, Oct 17, 2007 at 03:06:33PM -0700, Dan Weston wrote:
2) the function must halt for all defined arguments
fix :: forall p . (p - p) - p
fix f = let x = f x in x
On Wed, Oct 17, 2007 at 06:45:04PM -0700, Dan Weston wrote:
_|_ does not provide a witness to a theorem in any consistent logic
(otherwise everything could be proved from it), yet it inhabits every type
in Haskell. If the only invalid type instance is _|_, then a necessary and
sufficient
On Wed, Oct 17, 2007 at 06:49:24PM -0700, Dan Weston wrote:
It would seem that this induction on SN requires strictness at every stage.
Or am I missing something?
Yes you are missing something. Whether it exists in my message is less
certain.
First, note that the elements of SN[a] are
28 matches
Mail list logo
