Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→ 1,798,409 events total
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.