Logs: liberachat/#haskell
| 2026-02-23 20:25:16 | <EvanR> | anyway let us be ridiculed by math |
| 2026-02-23 20:25:28 | × | mehbark quits (~mehbark@joey.luug.ece.vt.edu) (Changing host) |
| 2026-02-23 20:25:28 | → | mehbark joins (~mehbark@user/mehbark) |
| 2026-02-23 20:26:13 | <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 20:26:55 | <tomsmeding> | an Eq instance defines / ought to define an equivalence relation, but functions are not necessarily representative-independent |
| 2026-02-23 20:27:02 | <tomsmeding> | clearly isNegativeZero isn't |
| 2026-02-23 20:28:02 | <tomsmeding> | I guess the conclusion is that we should prove more things |
| 2026-02-23 20:28:03 | → | Anarchos joins (~Anarchos@91-161-254-16.subs.proxad.net) |
| 2026-02-23 20:28:22 | <tomsmeding> | I'll leave the proofs as an exercise to the reader though |
| 2026-02-23 20:30:00 | <haskellbridge> | <loonycyborg> the number itself and its representation are distinct things |
| 2026-02-23 20:30:46 | <haskellbridge> | <loonycyborg> positive and negative zero have different representations but represent same number |
| 2026-02-23 20:31:08 | <haskellbridge> | <loonycyborg> at least as needed in practice |
| 2026-02-23 20:31:26 | <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 20:32:12 | <haskellbridge> | <loonycyborg> like if we add negative or positive zero to something then we'll get exactly the same number |
| 2026-02-23 20:33:16 | <EvanR> | that behavior wouldn't be problematic for x==y => f(x)==f(y) |
| 2026-02-23 20:33:37 | <EvanR> | it doesn't complain if everything ends up equal |
| 2026-02-23 20:34:46 | <EvanR> | and weeds upon weeds, the inverse trig functions care about the negative zero I think |
| 2026-02-23 20:35:28 | <EvanR> | > cot 0.0 (-1e-400) -- or even normal trig |
| 2026-02-23 20:35:30 | <lambdabot> | Variable not in scope: cot :: t0 -> t1 -> t |
| 2026-02-23 20:38:13 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-23 20:38:21 | <EvanR> | > (1 / tan 0.0, 1 / tan (-0.0)) |
| 2026-02-23 20:38:23 | <lambdabot> | (Infinity,-Infinity) |
| 2026-02-23 20:39:44 | <haskellbridge> | <loonycyborg> ye but it's still infinity |
| 2026-02-23 20:40:20 | <haskellbridge> | <ijouw> infinity == -infinity ? |
| 2026-02-23 20:40:58 | <haskellbridge> | <loonycyborg> the answer is moo :P |
| 2026-02-23 20:41:03 | <humasect> | ah well ... i would put infinity and zero in the same place. negative... |
| 2026-02-23 20:41:17 | <haskellbridge> | <loonycyborg> in most cases infinity leads to exception |
| 2026-02-23 20:41:31 | <EvanR> | infinite == -infinite ok but infinite == zero might require some more coffee |
| 2026-02-23 20:41:35 | <humasect> | div by zero feels more like inifnity |
| 2026-02-23 20:42:54 | × | machined1od quits (~machinedg@d172-219-48-230.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 2026-02-23 20:43:31 | <EvanR> | also anybody get the feeling NaN comes up much more often than infinity for some reason |
| 2026-02-23 20:43:41 | <EvanR> | so annoying |
| 2026-02-23 20:44:46 | × | marinelli quits (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 2026-02-23 20:44:52 | × | peutri quits (~peutri@bobo.desast.re) (Ping timeout: 246 seconds) |
| 2026-02-23 20:45:08 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2026-02-23 20:45:09 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-02-23 20:45:53 | × | LUCKY_NOOB quits (~LUCKY_NOO@user/LUCKY-NOOB:44374) (Quit: leaving) |
| 2026-02-23 20:46:12 | → | LUCKY_NOOB joins (~LUCKY_NOO@user/LUCKY-NOOB:44374) |
| 2026-02-23 20:46:47 | → | peutri joins (~peutri@bobo.desast.re) |
| 2026-02-23 20:49:23 | <haskellbridge> | <ijouw> I don't remember where it comes up and a value is more reasonable |
| 2026-02-23 20:49:23 | <tomsmeding> | infinity actually behaves kind of okay under certain floating point operations |
| 2026-02-23 20:49:35 | <haskellbridge> | <ijouw> atan (1/0) |
| 2026-02-23 20:49:43 | <tomsmeding> | > atan (1 / 0) |
| 2026-02-23 20:49:44 | <lambdabot> | 1.5707963267948966 |
| 2026-02-23 20:50:07 | <tomsmeding> | > (1 / 0) * 2 > 3 |
| 2026-02-23 20:50:09 | <lambdabot> | True |
| 2026-02-23 20:50:28 | <EvanR> | I approve |
| 2026-02-23 20:50:32 | <tomsmeding> | NaN, however, breaks everything it touches; EvanR perhaps this influences what you observe |
| 2026-02-23 20:51:02 | <tomsmeding> | > (1 / 0) + (-1 / 0) |
| 2026-02-23 20:51:04 | <lambdabot> | NaN |
| 2026-02-23 20:51:11 | <EvanR> | I have to preface everything I say about floats with "assuming no NaNs" |
| 2026-02-23 20:51:31 | <EvanR> | another case of math beating us, by defining 1 to be not a prime |
| 2026-02-23 20:51:32 | <tomsmeding> | "assuming these are all numbers" |
| 2026-02-23 20:51:42 | <humasect> | > (1 / 0) |
| 2026-02-23 20:51:44 | <lambdabot> | Infinity |
| 2026-02-23 20:52:33 | <EvanR> | so you don't have to preface everything you say about primes with "assuming no 1s" |
| 2026-02-23 20:52:49 | <tomsmeding> | there's plenty of math that assumes odd primes |
| 2026-02-23 20:53:11 | <EvanR> | given an odd non-1 prime... |
| 2026-02-23 20:53:18 | <tomsmeding> | which I always find a funny phrasing, almost certainly chosen because it's the shortest way to express the intended set |
| 2026-02-23 20:53:23 | <EvanR> | oh wait |
| 2026-02-23 20:53:35 | <EvanR> | I get you |
| 2026-02-23 20:54:14 | <tomsmeding> | "an odd prime p" is not even really shorter than "a prime p ≥ 3" |
| 2026-02-23 20:54:17 | <[exa]> | I once called these "degenerate" primes in front of both abstract&linear algebra folks at once |
| 2026-02-23 20:54:26 | <[exa]> | man I got hated |
| 2026-02-23 20:54:30 | <tomsmeding> | what, 1 and 2? |
| 2026-02-23 20:54:41 | <[exa]> | yes |
| 2026-02-23 20:54:44 | <tomsmeding> | nice! |
| 2026-02-23 20:55:11 | <tomsmeding> | that's a good way to annoy mathematicians |
| 2026-02-23 20:56:16 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-23 20:57:01 | <EvanR> | bottom, NaN, and prime 1 walk into a bar |
| 2026-02-23 20:57:38 | <tomsmeding> | and the story yielded an infinite stream of indivisible batman? |
| 2026-02-23 20:57:55 | <newmind> | EvanR: is the punchline segfault or illegal operation? |
| 2026-02-23 20:57:58 | <EvanR> | ha |
| 2026-02-23 20:58:56 | → | petrichor joins (~jez@user/petrichor) |
| 2026-02-23 20:59:12 | <tomsmeding> | (for the unenlightened: the "batman" is a reference to https://www.destroyallsoftware.com/talks/wat 3:24) |
| 2026-02-23 20:59:28 | <[exa]> | I like how 3:24 looks like a bible reference |
| 2026-02-23 20:59:43 | <tomsmeding> | the imagery in the video is appropriate |
| 2026-02-23 21:00:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-02-23 21:02:38 | × | AlexZenon quits (~alzenon@178.34.151.130) (Ping timeout: 256 seconds) |
| 2026-02-23 21:04:06 | × | constxd quits (~constxd@user/constxd) (Server closed connection) |
| 2026-02-23 21:05:29 | <EvanR> | I was unenlightened but now I'm unenlightened minus that bit of enlightenment |
| 2026-02-23 21:05:49 | <EvanR> | which might still be unenlightened dependent on precision |
| 2026-02-23 21:05:57 | × | distopico quits (~cerdolibr@2001:4b98:dc2:41:216:3eff:fe6c:52a1) (Server closed connection) |
| 2026-02-23 21:05:58 | → | constxd joins (~constxd@user/constxd) |
| 2026-02-23 21:06:12 | → | distopico joins (~cerdolibr@xvm-111-150.dc2.ghst.net) |
| 2026-02-23 21:06:32 | → | AlexZenon joins (~alzenon@178.34.151.130) |
| 2026-02-23 21:11:17 | × | petrichor quits (~jez@user/petrichor) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-02-23 21:11:38 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-02-23 21:12:58 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2026-02-23 21:14:56 | → | sp1ff joins (~user@2601:1c2:4701:7850::8cd) |
| 2026-02-23 21:16:11 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-02-23 21:19:31 | × | target_i quits (~target_i@user/target-i/x-6023099) (Ping timeout: 264 seconds) |
| 2026-02-23 21:21:10 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2026-02-23 21:21:57 | × | mmaruseacph2 quits (~mihai@mihai.page) (Server closed connection) |
| 2026-02-23 21:22:12 | → | mmaruseacph2 joins (~mihai@mihai.page) |
| 2026-02-23 21:25:24 | <tomsmeding> | EvanR: how does it feel |
| 2026-02-23 21:26:14 | → | tromp joins (~textual@2001:1c00:3487:1b00:1a7:fa86:12e2:7e3d) |
| 2026-02-23 21:28:04 | <EvanR> | I was hoping he was going to show some haskell wats |
| 2026-02-23 21:28:06 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 268 seconds) |
| 2026-02-23 21:29:28 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
All times are in UTC.