Newest at the top
| 2026-02-23 21:32:12 +0100 | <haskellbridge> | <loonycyborg> like if we add negative or positive zero to something then we'll get exactly the same number |
| 2026-02-23 21:31:26 +0100 | <EvanR> | in the case of float it's kind of murky, what's the number itself, what's the representation (relevant to this law, and are reals even supposed to be like standard reals). Which I guess is food for thought when thinking about any other situation we are implementing |
| 2026-02-23 21:31:08 +0100 | <haskellbridge> | <loonycyborg> at least as needed in practice |
| 2026-02-23 21:30:46 +0100 | <haskellbridge> | <loonycyborg> positive and negative zero have different representations but represent same number |
| 2026-02-23 21:30:00 +0100 | <haskellbridge> | <loonycyborg> the number itself and its representation are distinct things |
| 2026-02-23 21:28:22 +0100 | <tomsmeding> | I'll leave the proofs as an exercise to the reader though |
| 2026-02-23 21:28:03 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-02-23 21:28:02 +0100 | <tomsmeding> | I guess the conclusion is that we should prove more things |
| 2026-02-23 21:27:02 +0100 | <tomsmeding> | clearly isNegativeZero isn't |
| 2026-02-23 21:26:55 +0100 | <tomsmeding> | an Eq instance defines / ought to define an equivalence relation, but functions are not necessarily representative-independent |
| 2026-02-23 21:26:13 +0100 | <tomsmeding> | when I was studying maths, we continually had to prove stuff independent of the choice of representative, to make things work on equivalence classes |
| 2026-02-23 21:25:28 +0100 | mehbark | (~mehbark@user/mehbark) mehbark |
| 2026-02-23 21:25:28 +0100 | mehbark | (~mehbark@joey.luug.ece.vt.edu) (Changing host) |
| 2026-02-23 21:25:16 +0100 | <EvanR> | anyway let us be ridiculed by math |
| 2026-02-23 21:24:38 +0100 | <EvanR> | so it's like conflating a quotient with a thing being quotiented |
| 2026-02-23 21:23:49 +0100 | <EvanR> | than* |
| 2026-02-23 21:23:44 +0100 | <EvanR> | loonycyborg, well the slightly deeper issue that satisfying basic properties of equality is in this case... that otherwise sensible definition of (testable in this case) equality isn't universally obeyed. I.e. someone somewhere can observe a distinction between equals |
| 2026-02-23 21:22:39 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!) |
| 2026-02-23 21:22:04 +0100 | <EvanR> | so there's an equivalent of equivalences |
| 2026-02-23 21:21:16 +0100 | <EvanR> | lol |
| 2026-02-23 21:19:10 +0100 | <tomsmeding> | ≊ ALMOST EQUAL OR EQUAL TO is also suspicious -- surely if it's equal, it's also almost equal? |
| 2026-02-23 21:18:48 +0100 | <tomsmeding> | lol |
| 2026-02-23 21:18:41 +0100 | <int-e> | if you're undecided: ⪟ |
| 2026-02-23 21:18:35 +0100 | <EvanR> | almost equal to is a perennial favorite |
| 2026-02-23 21:17:50 +0100 | <tomsmeding> | choose your favourite https://tomsmeding.com/unicode#equal |
| 2026-02-23 21:17:46 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-02-23 21:17:34 +0100 | stef204 | (~stef204@user/stef204) stef204 |
| 2026-02-23 21:17:31 +0100 | <EvanR> | can we get a proper equal sign in here xD |
| 2026-02-23 21:17:10 +0100 | poscat0x04 | (~poscat@user/poscat) (Ping timeout: 255 seconds) |
| 2026-02-23 21:16:49 +0100 | tomsmeding | . o O ( reallyUnsafePointerEquality ) |
| 2026-02-23 21:15:57 +0100 | <EvanR> | which is something else again |
| 2026-02-23 21:15:57 +0100 | poscat | (~poscat@user/poscat) poscat |
| 2026-02-23 21:15:49 +0100 | <EvanR> | while same object speaks to me as same StableName |
| 2026-02-23 21:15:49 +0100 | <haskellbridge> | <loonycyborg> since we're free to implement == however we want, we can even violate basic properties of equality like reflexivity. |
| 2026-02-23 21:14:28 +0100 | <haskellbridge> | <loonycyborg> ah yes == isn't the same as it being same object |
| 2026-02-23 21:13:29 +0100 | <lambdabot> | (True,False) |
| 2026-02-23 21:13:28 +0100 | <EvanR> | > let f x y = (x == y, isNegativeZero x == isNegativeZero y) in f 0.0 (-1e-400) |
| 2026-02-23 21:12:34 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-02-23 21:09:35 +0100 | <EvanR> | good question |
| 2026-02-23 21:09:18 +0100 | Beowulf | (florian@sleipnir.bandrate.org) |
| 2026-02-23 21:09:12 +0100 | <haskellbridge> | <loonycyborg> wouldn't that violate referential trasparency? :P |
| 2026-02-23 21:08:08 +0100 | <EvanR> | the extent to which as programmers we run into or invent situations where x==y implying f(x)==f(y) doesn't hold |
| 2026-02-23 21:04:39 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 255 seconds) |
| 2026-02-23 21:03:44 +0100 | Beowulf | (florian@sleipnir.bandrate.org) (Quit: = "") |
| 2026-02-23 21:00:34 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-02-23 21:00:06 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-02-23 20:58:41 +0100 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Ping timeout: 268 seconds) |
| 2026-02-23 20:55:05 +0100 | GoldsteinQ | (~goldstein@goldstein.lol) |
| 2026-02-23 20:54:46 +0100 | attlin | (~user@user/attlin) attlin |
| 2026-02-23 20:52:05 +0100 | GoldsteinQ | (~goldstein@goldstein.lol) (Quit: ZNC 1.10.1 - https://znc.in) |