Logs: liberachat/#haskell
| 2026-01-08 21:30:05 | <EvanR> | fold being for the special case where all possible folds result in the same answer (a monoidal fold) |
| 2026-01-08 21:30:31 | → | mulk joins (~mulk@pd95143a6.dip0.t-ipconnect.de) |
| 2026-01-08 21:31:19 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 2026-01-08 21:32:15 | <EvanR> | considering how many utility functions other languages are sorely missing I am ok if haskell has 1 that is "useless", I'm arguing it's useful for pedagogical purposes |
| 2026-01-08 21:32:26 | <EvanR> | though* |
| 2026-01-08 21:32:58 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 21:33:30 | <jreicher> | I agree it's good to have a sandbox of some kind for programmers to experience the consequences of laziness and how they can sometimes be avoided. |
| 2026-01-08 21:34:01 | × | Milan_Vanca quits (~milan@user/Milan-Vanca:32634) (Quit: WeeChat 4.7.2) |
| 2026-01-08 21:34:48 | × | spew quits (~spew@user/spew) (Quit: nyaa~) |
| 2026-01-08 21:36:03 | <EvanR> | however the situation with sum |
| 2026-01-08 21:36:08 | <EvanR> | @src sum |
| 2026-01-08 21:36:08 | <lambdabot> | sum = foldl (+) 0 |
| 2026-01-08 21:36:25 | <EvanR> | this is probably dumb |
| 2026-01-08 21:36:26 | trickard_ | is now known as trickard |
| 2026-01-08 21:38:08 | <tomsmeding> | it is, but that was fixed; sum is now defined using foldl' |
| 2026-01-08 21:38:25 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-08 21:38:33 | <EvanR> | good |
| 2026-01-08 21:38:35 | <jreicher> | Oww. How did that happen in the first place? |
| 2026-01-08 21:39:09 | <tomsmeding> | that one was probably just an oversight |
| 2026-01-08 21:39:44 | <EvanR> | maybe, but there was a long thread on the mailing list defending the foldl version xD |
| 2026-01-08 21:40:04 | <EvanR> | a long time ago |
| 2026-01-08 21:40:09 | <tomsmeding> | there are probably contrived Num instances for which foldl' would be inappropriate |
| 2026-01-08 21:40:32 | <tomsmeding> | but contrary to Foldable, where [a] is merely a common instance, such contrived Num instances are really contrived, I'd guess |
| 2026-01-08 21:41:08 | <EvanR> | (curiously) Foldable ended up being more principled and based than Num |
| 2026-01-08 21:41:19 | <tomsmeding> | Num was never principled or based in any way |
| 2026-01-08 21:41:21 | <EvanR> | most things people try to write a Num instance for are contrived xD |
| 2026-01-08 21:41:23 | <tomsmeding> | so that's a low bar |
| 2026-01-08 21:41:43 | <tomsmeding> | I've ranted about Num before here |
| 2026-01-08 21:42:02 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-01-08 21:42:33 | <EvanR> | at some point you heard a lot of Foldable has no laws, Foldable is essentially a place to put your toList function |
| 2026-01-08 21:43:18 | <mauke> | comfortably Num |
| 2026-01-08 21:43:58 | <Leary> | `Foldable` just doesn't need laws, since the type of `foldMap` and parametricity say it all. |
| 2026-01-08 21:48:46 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 21:50:18 | <Leary> | Re `Num`, `abs` and `signum` should be moved to another class, and arguably `fromInteger` too (necessitating new `zero` and `one` methods). The rest could do to be split up or factored over `Monoid`, but it's otherwise fine and perfectly principled as a class for rings. |
| 2026-01-08 21:50:25 | <monochrom> | You need a law to outlaw me trying "foldMap _ _ = mempty". |
| 2026-01-08 21:50:51 | <Leary> | monochrom: But sometimes that's the correct implementation. :) |
| 2026-01-08 21:59:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-08 22:00:43 | Googulator82 | is now known as Googulator |
| 2026-01-08 22:00:58 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 2026-01-08 22:03:09 | × | malte quits (~malte@mal.tc) (Ping timeout: 250 seconds) |
| 2026-01-08 22:03:31 | <EvanR> | zero and one |
| 2026-01-08 22:03:39 | <EvanR> | and a law saying they must be different? xD |
| 2026-01-08 22:04:26 | <geekosaur> | they're allowed to be the same… if there's only one value in the set |
| 2026-01-08 22:04:32 | → | malte joins (~malte@mal.tc) |
| 2026-01-08 22:04:37 | <EvanR> | this whole time I was convinced that Num reflects a subcultural understanding of computer numbers and programmers are not usually thinking they're using a ring |
| 2026-01-08 22:04:37 | → | danza joins (~danza@user/danza) |
| 2026-01-08 22:05:21 | <monochrom> | I agree. |
| 2026-01-08 22:05:30 | <EvanR> | though we have good examples where they are, in crypto code |
| 2026-01-08 22:06:49 | × | danz94513 quits (~danza@user/danza) (Ping timeout: 246 seconds) |
| 2026-01-08 22:07:12 | <tomsmeding> | if 1 = 0 then by the ring axioms, 0 = 0 * a = 1 * a = a, so all elements are zero, so it's the trivial ring, but it's allowed |
| 2026-01-08 22:08:10 | <haskellbridge> | <loonycyborg> you can even divide by zero in this ring |
| 2026-01-08 22:11:19 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 22:11:33 | <tomsmeding> | (and 0 = a * 0 because: 0 = 1 + -1 = a * a^-1 + -1 = a * (0 + a^-1) + -1 = a * 0 + a * a^-1 + -1 = a * 0 + 1 + -1 = a * 0 + 0 = a * 0; there's probably a simpler derivation lol) |
| 2026-01-08 22:14:24 | → | xff0x_ joins (~xff0x@2405:6580:b080:900:cd9:802b:8b60:b254) |
| 2026-01-08 22:14:36 | <monochrom> | for all b, b*(a*0) = (b*a)*0 = 0. Then appeal to uniqueness of 0: "if forall b b*foo=0, then foo=0" |
| 2026-01-08 22:15:20 | tomsmeding | doesn't follow; doesn't that assume a*0 = 0 from the get go? |
| 2026-01-08 22:15:24 | <TMA> | tomsmeding: I have encountered ring definition containing the axiom 0!=1 as well |
| 2026-01-08 22:15:30 | jmcantrell_ | is now known as jmcantrell |
| 2026-01-08 22:16:10 | <monochrom> | 0 is axiomatized by "forall a, a*0 = 0". |
| 2026-01-08 22:16:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-08 22:16:26 | <monochrom> | To be sure I need a separate proof why it's unique. |
| 2026-01-08 22:16:27 | tomsmeding | is reading https://en.wikipedia.org/wiki/Ring_(mathematics) |
| 2026-01-08 22:16:32 | <geekosaur> | that was what I thought |
| 2026-01-08 22:16:34 | <tomsmeding> | this axiomatises 0 as the additive unit |
| 2026-01-08 22:16:39 | × | xff0x quits (~xff0x@2405:6580:b080:900:1a94:9136:5419:ce9c) (Ping timeout: 260 seconds) |
| 2026-01-08 22:16:49 | <geekosaur> | 0 is required to be an annihilating element in multiplication |
| 2026-01-08 22:16:51 | <monochrom> | Oh oops, sorry! Delete everything I said. |
| 2026-01-08 22:17:06 | <tomsmeding> | geekosaur: no, because you can prove it so it need not be an axiom :p |
| 2026-01-08 22:17:16 | <geekosaur> | but I think that's derived, not amxiom |
| 2026-01-08 22:17:44 | <tomsmeding> | right, I just proved it in a long-winded way (see 6 minutes ago), but surely there's a more direct way |
| 2026-01-08 22:18:47 | <ncf> | a * 0 = a * (1 - 1) = a - a = 0 ? |
| 2026-01-08 22:19:02 | <TMA> | 0*a = (x-x)*a = xa - xa = 0 for any x |
| 2026-01-08 22:19:32 | <tomsmeding> | ncf: thank you |
| 2026-01-08 22:19:38 | <tomsmeding> | oh also TMA :) |
| 2026-01-08 22:19:47 | <Leary> | That still relies on `a * -1 = -a`. |
| 2026-01-08 22:19:49 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-01-08 22:20:17 | <TMA> | the other order of operands need showing (-1)*a = a*(-1) |
| 2026-01-08 22:21:59 | <Leary> | a * -0 = a * (-0 + 0) = a * -0 + a * 0 ==> a * 0 = 0 (by cancellation) |
| 2026-01-08 22:22:53 | <ncf> | Leary++ |
| 2026-01-08 22:23:11 | <tomsmeding> | so fully: 0 = -(a * -0) + a * -0 = -(a * -0) + a * (-0 + 0) = -(a * -0) + a * -0 + a * 0 = 0 + a * 0 = a * 0 |
| 2026-01-08 22:24:16 | <Leary> | Actually the -0 could have been anything, should have just used 0. |
| 2026-01-08 22:24:29 | <monochrom> | :) |
| 2026-01-08 22:24:38 | → | AlexNoo joins (~AlexNoo@178.34.163.50) |
| 2026-01-08 22:25:38 | <ncf> | 0 = a * 0 - a * 0 = a * (0 + 0) - a * 0 = a * 0 + a * 0 - a * 0 = a * 0 |
| 2026-01-08 22:26:51 | <tomsmeding> | nice |
| 2026-01-08 22:26:52 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-08 22:27:34 | × | Digit quits (~user@user/digit) (Remote host closed the connection) |
| 2026-01-08 22:27:38 | <TMA> | Leary: ax = a(x+0) = ax + a0; now add -ax to both sides: -ax + ax = -ax + ax + a0 ==> 0 = 0 + a0 = a0, do I understand you correctly? |
| 2026-01-08 22:28:19 | <Leary> | Yes. |
| 2026-01-08 22:31:24 | × | carbolymer quits (~carbolyme@delirium.systems) (Read error: Connection reset by peer) |
| 2026-01-08 22:31:31 | × | ncf quits (~n@monade.li) (Ping timeout: 264 seconds) |
| 2026-01-08 22:31:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-08 22:31:59 | → | carbolymer joins (~carbolyme@delirium.systems) |
| 2026-01-08 22:33:08 | → | ncf joins (~n@monade.li) |
| 2026-01-08 22:36:47 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 252 seconds) |
| 2026-01-08 22:38:59 | → | Digit joins (~user@user/digit) |
| 2026-01-08 22:40:04 | × | carbolymer quits (~carbolyme@delirium.systems) () |
| 2026-01-08 22:40:14 | → | carbolymer joins (~carbolyme@delirium.systems) |
| 2026-01-08 22:40:38 | × | tromp quits (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-01-08 22:41:05 | × | carbolymer quits (~carbolyme@delirium.systems) (Client Quit) |
All times are in UTC.