Can someone explain to me, given that (a) I'm not particularly expert
at maths, (b) I'm not particularly expert at Haskell, and (c) I'm a
bit fuzzybrained of late:
Given that _|_ represents in some sense any computation not
representable in and/or not consistent with Haskell, why/how is
On Jan 23, 2007, at 2:09 PM, Brandon S. Allbery KF8NH wrote:
Can someone explain to me, given that (a) I'm not particularly
expert at maths, (b) I'm not particularly expert at Haskell, and
(c) I'm a bit fuzzybrained of late:
Given that _|_ represents in some sense any computation not
Brandon S. Allbery KF8NH wrote:
Can someone explain to me, given that (a) I'm not particularly expert
at maths, (b) I'm not particularly expert at Haskell, and (c) I'm a bit
fuzzybrained of late:
Me too...
Given that _|_ represents in some sense any computation not
representable in
On Jan 23, 2007, at 14:48 , Robert Dockins wrote:
Its possible, however, that I don't understand your question. The
formula (p^~p)-q (AKA, proof by contradiction) is valid most
classical and constructive logics that I know of, so I'm not quite
sure what you're getting at.
I'm not
On Jan 23, 2007, at 14:58 , Seth Gordon wrote:
The only catch I see to that POV is that the way `seq` is defined,
undefined `seq` 42 *must* return an error. If this were
analogous to
(p^~p)-q, then undefined `seq` 42 would be allowed to return any
value whatsoever.
That's not quite what
Hi
That's not quite what I was trying to say. (p^~p)-q is equivalent
to _|_ in the sense that once you derive/compute (respectively) it,
the world in which it exists breaks.
I think thats a bit overly harsh view of _|_ to take. The world does
not break once you compute _|_ - a _|_ value
On Jan 23, 2007, at 15:34 , Neil Mitchell wrote:
prove/compute anything you couldn't before. While removing _|_ from
the language does make some things nicer to reason about, there aren't
many corners where _|_ really gets in the way that much - seq being
one of those few corners.
But that
Hi
prove/compute anything you couldn't before. While removing _|_ from
the language does make some things nicer to reason about, there aren't
many corners where _|_ really gets in the way that much - seq being
one of those few corners.
But that is exactly the problem: `seq` forces _|_ to
Brandon S. Allbery KF8NH wrote:
That's not quite what I was trying to say. (p^~p)-q is equivalent
to _|_ in the sense that once you derive/compute (respectively) it,
the world in which it exists breaks. (I don't think formal logic
can have a Haskell-like _|_, but deriving (p^~p)-q is
On Jan 23, 2007, at 15:50 , Neil Mitchell wrote:
prove/compute anything you couldn't before. While removing _|_ from
the language does make some things nicer to reason about, there
aren't
many corners where _|_ really gets in the way that much - seq being
one of those few corners.
But
10 matches
Mail list logo
