Newest at the top
| 2026-02-23 21:46:47 +0100 | peutri | (~peutri@bobo.desast.re) peutri |
| 2026-02-23 21:46:12 +0100 | LUCKY_NOOB | (~LUCKY_NOO@user/LUCKY-NOOB:44374) LUCKY_NOOB |
| 2026-02-23 21:45:53 +0100 | LUCKY_NOOB | (~LUCKY_NOO@user/LUCKY-NOOB:44374) (Quit: leaving) |
| 2026-02-23 21:45:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-02-23 21:45:08 +0100 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2026-02-23 21:44:52 +0100 | peutri | (~peutri@bobo.desast.re) (Ping timeout: 246 seconds) |
| 2026-02-23 21:44:46 +0100 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 2026-02-23 21:43:41 +0100 | <EvanR> | so annoying |
| 2026-02-23 21:43:31 +0100 | <EvanR> | also anybody get the feeling NaN comes up much more often than infinity for some reason |
| 2026-02-23 21:42:54 +0100 | machined1od | (~machinedg@d172-219-48-230.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 2026-02-23 21:41:35 +0100 | <humasect> | div by zero feels more like inifnity |
| 2026-02-23 21:41:31 +0100 | <EvanR> | infinite == -infinite ok but infinite == zero might require some more coffee |
| 2026-02-23 21:41:17 +0100 | <haskellbridge> | <loonycyborg> in most cases infinity leads to exception |
| 2026-02-23 21:41:03 +0100 | <humasect> | ah well ... i would put infinity and zero in the same place. negative... |
| 2026-02-23 21:40:58 +0100 | <haskellbridge> | <loonycyborg> the answer is moo :P |
| 2026-02-23 21:40:20 +0100 | <haskellbridge> | <ijouw> infinity == -infinity ? |
| 2026-02-23 21:39:44 +0100 | <haskellbridge> | <loonycyborg> ye but it's still infinity |
| 2026-02-23 21:38:23 +0100 | <lambdabot> | (Infinity,-Infinity) |
| 2026-02-23 21:38:21 +0100 | <EvanR> | > (1 / tan 0.0, 1 / tan (-0.0)) |
| 2026-02-23 21:38:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-02-23 21:35:30 +0100 | <lambdabot> | Variable not in scope: cot :: t0 -> t1 -> t |
| 2026-02-23 21:35:28 +0100 | <EvanR> | > cot 0.0 (-1e-400) -- or even normal trig |
| 2026-02-23 21:34:46 +0100 | <EvanR> | and weeds upon weeds, the inverse trig functions care about the negative zero I think |
| 2026-02-23 21:33:37 +0100 | <EvanR> | it doesn't complain if everything ends up equal |
| 2026-02-23 21:33:16 +0100 | <EvanR> | that behavior wouldn't be problematic for x==y => f(x)==f(y) |
| 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 |