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,
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 = CP
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
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
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
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, Da
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
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 unl
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 unl
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 on
> 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
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 s
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,
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 lambd
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
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
_|_ 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 instanc
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
de
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
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 u
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
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
>
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 yet.
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 "p"s and "q"s and wont line up with
the outer type declaratio
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
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) (imp
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
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
A tutorial on the Curry-Howard Correspondence in Haskell:
http://www.thenewsh.com/%7Enewsham/formal/curryhoward/
Feedback appreciated.
Tim Newsham
http://www.thenewsh.com/~newsham/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.has
29 matches
Mail list logo