Logs on 2026-01-08 (liberachat/#haskell)
| 00:03:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 00:06:33 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds) |
| 00:11:45 | <monochrom> | As an individual citizen of #haskell I say that I'm not interested in a Claude program but that's just me. As a moderator I say that "fuck off" is uncalled for. |
| 00:13:46 | <geekosaur> | +1 |
| 00:14:15 | <newmind> | it's perfectly fine, i fully get that it might be a charged topic, i was just wondering if i might have expressed myself in a way that's generally offensive >.> |
| 00:15:05 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 00:15:14 | <monochrom> | I think you're doing fine. You just asked "anyone interested?" so it's fair game. |
| 00:19:47 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 00:25:43 | → | Googulator14 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 00:25:43 | × | Googulator quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 00:27:49 | <newmind> | besides, the assessment seemed to be, at the very least, factually accurate :) |
| 00:30:53 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 00:31:26 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 00:31:28 | × | annamalai quits (~annamalai@2409:4042:eb8:bd50::9eca:160e) (Ping timeout: 246 seconds) |
| 00:31:39 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 00:36:01 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 00:36:37 | × | shr\ke quits (~shrike@user/shrke:31298) (Ping timeout: 264 seconds) |
| 00:36:55 | trickard_ | is now known as trickard |
| 00:37:47 | → | shr\ke joins (~shrike@user/paxhumana) |
| 00:37:47 | × | shr\ke quits (~shrike@user/paxhumana) (Changing host) |
| 00:37:47 | → | shr\ke joins (~shrike@user/shrke:31298) |
| 00:40:21 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 00:42:14 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 00:46:42 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 00:49:16 | → | raincomplex joins (~rain@user/raincomplex) |
| 00:51:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 00:52:16 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 00:55:04 | <EvanR> | in the sense that a program is a proof of some theorem, if I can get a computer to give me the correct program that's great. But that's not what we're doing right now with AI |
| 00:55:48 | <EvanR> | it's more like mass copywrite infringement search |
| 00:56:35 | <jreicher> | Even correct programs aren't proofs of theorems. "In retrospect it seems to be doing the right thing." |
| 00:56:38 | <EvanR> | of code that is hardly a proof of anything |
| 00:56:39 | → | ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com) |
| 00:57:22 | <EvanR> | jreicher, correct in the sense that I explicitly specified the theorem |
| 00:57:36 | <EvanR> | not "write me an MMO in haskell" |
| 00:58:01 | <newmind> | that would be the dream, yeah: provide a spec, and it spits out a program that fulfills that (and while we're at it, also does proofably terminate and run in limited space).. but current AI agents are doing the exact opposite, little more than running in yolo mode and just executing whatever comes to mind.. what i'm proposing is a middle ground: at |
| 00:58:02 | <newmind> | least run code that's checked by a compiler and can't do anything completely nuts |
| 00:58:48 | <jreicher> | Even if AI could do it, I think the bigger problem is motivating humans to write specs in the first place. That's been possible for half a century and still almost nobody doesit. |
| 00:58:49 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 00:59:15 | <EvanR> | that part is beyond my paygrade xD |
| 00:59:30 | <newmind> | in the meantime, for _a lot_ of real world software problems, it's a lot more grey: people can specify "what they want" only in very loose terms |
| 01:00:03 | <EvanR> | people with mathematical or engineering maturity are better at specifying what they want or what they have |
| 01:00:55 | <EvanR> | hopefully that bleeds onto programming at some point |
| 01:00:56 | <jreicher> | Never thought about this before, but maybe there's a market for AI /only/ because of informal specification. If the spec was formal non-AI program generation might be possible? |
| 01:01:26 | <geekosaur> | that was the theory behind UML, I think? |
| 01:01:30 | <ncf> | take it to #haskell-offtopic please, this is not the place to discuss LLMs |
| 01:02:08 | <EvanR> | yeah I don't see the connection to haskell specifically |
| 01:02:58 | <jreicher> | Fair |
| 01:03:10 | → | omidmash5 joins (~omidmash@user/omidmash) |
| 01:03:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 01:03:39 | <haskellbridge> | <sm> it means that if you come into a space and talk about the ai thing you're building, you need to be ready for all kinds of response |
| 01:03:41 | <haskellbridge> | <sm> (I'm not excusing rudeness, but I understand it) |
| 01:05:09 | × | xff0x quits (~xff0x@2405:6580:b080:900:4b0b:90a:cd82:2bd2) (Ping timeout: 244 seconds) |
| 01:05:09 | × | omidmash quits (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 01:05:09 | omidmash5 | is now known as omidmash |
| 01:06:27 | <newmind> | the connection would be that haskell (or strongly typed languages in particular) provide guardrails and constraints to LLM generated code that does not exist in other languages, including that generated haskell code is safer (not absolutely safe) to generate and run than in most other languages (especially with the Safe extension enabled). but i |
| 01:06:28 | <newmind> | take your point, i was just generally looking for feedback, viewpoints and ideas |
| 01:08:00 | × | prite quits (~pritam@user/pritambaral) (Quit: Konversation terminated!) |
| 01:08:55 | <int-e> | discover new ways in which well-typed programs go wrong |
| 01:09:40 | <EvanR> | some of those premises about haskell don't add up ... |
| 01:10:05 | <int-e> | You'd need {-# LANGUAGE AdditivePromises #-} for that. |
| 01:10:13 | <EvanR> | executing "untrusted" code is still a horrible idea in haskell |
| 01:10:21 | <EvanR> | and not sure why that's even required |
| 01:10:34 | <int-e> | > text "why oh why indeed" |
| 01:10:35 | <lambdabot> | why oh why indeed |
| 01:11:16 | <EvanR> | the amount of infrastructure required for lambdabot xD |
| 01:11:34 | <EvanR> | he's running in the equivalent of that underwater prison in avengers |
| 01:12:27 | <int-e> | huh |
| 01:13:42 | <newmind> | obviously, yes. and i'd never advocate for blindly running untrusted code either. but it's a lot easier to reason about a function with a type signature than just executing a bash script blindly. it's not meant as a airtight sandbox that holds up against adverserial attacks, but it is another layer. and it is quite a bit more than what current |
| 01:13:43 | <newmind> | agents are doing |
| 01:14:36 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 01:15:52 | <int-e> | EvanR: I'm kind of curious what evoked that picture. |
| 01:17:55 | <EvanR> | haskell itself isn't making code inherently safe, you have whatever layers of stuff and planning for something like an eval bot |
| 01:18:36 | <EvanR> | in any language |
| 01:19:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 01:22:03 | <jreicher> | My understanding of type checking has always been that it's only checking whether the programmer has contradicted themselves. The programmer writes the type assertions, and the programmer writes the code. Type checker checks if that set of assertions is inconsistent according to the type inference rules. |
| 01:22:22 | <jreicher> | Nothing in that guarantees safety. |
| 01:22:52 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 01:23:15 | → | bggd joins (~bgg@user/bggd) |
| 01:23:20 | <newmind> | exactly, the language itself has nothing to do with the inherent safety, that was never my claim. but what it has is a type system that does let you reason where and how IO actually happens. if you need _safety_ you still need sandboxing, vms and whatever else you would use for any other binary |
| 01:24:48 | × | divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 01:24:52 | → | divlamir_ joins (~divlamir@user/divlamir) |
| 01:25:44 | divlamir_ | is now known as divlamir |
| 01:30:24 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 01:36:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 01:42:00 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 01:42:13 | × | Googulator14 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 01:42:30 | → | Googulator14 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 01:45:07 | × | lbseale quits (~quassel@user/ep1ctetus) (Client Quit) |
| 01:45:50 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 01:48:27 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 01:53:24 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 02:00:54 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 02:00:56 | → | omidmash1 joins (~omidmash@user/omidmash) |
| 02:02:30 | × | omidmash quits (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 02:02:30 | omidmash1 | is now known as omidmash |
| 02:04:09 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 02:04:14 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 02:09:07 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 02:09:09 | → | libertyprime joins (~libertypr@121.74.62.77) |
| 02:09:22 | <monochrom> | You can extend that argument to all correctness proofs. The proof only checks that the program doesn't contradict the claim. Nothing says the claim guarantees safety in the first place. |
| 02:10:39 | <geekosaur> | (or anything else, for that matter) |
| 02:10:52 | <monochrom> | But the apologetic is that if you make you say the same thing in two ways, once as the program and once more as the claim, and if they are consistent, that's heightened confidence that you have made fewer mistakes. |
| 02:11:08 | <monochrom> | err, s/if you make you/if I make you/ |
| 02:12:47 | <EvanR> | I write my program from scratch several times so there's less chance of a bug |
| 02:12:51 | <monochrom> | Extra credit if you also provide test cases. (That's like saying the same thing the third way.) |
| 02:13:20 | <EvanR> | 99% times 99% times 99% correct equals |
| 02:13:29 | <EvanR> | 999999% correct |
| 02:14:06 | × | libertyprime quits (~libertypr@121.74.62.77) (Quit: leaving) |
| 02:14:14 | <monochrom> | (In fact when I pose a programming homework question when teaching, I provide examples and sample test cases. It's good old reliability by redundancy.) |
| 02:20:01 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 02:23:08 | × | rainbyte quits (~rainbyte@186.22.19.214) (Read error: Connection reset by peer) |
| 02:24:42 | → | rainbyte joins (~rainbyte@186.22.19.214) |
| 02:24:52 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 02:26:52 | <EvanR> | now I ran into a funny... in some cases repeating a test causes your confidence to go from 95% to 99% to 99.99999%, in other cases repeated trials causes chance of success to go from 95% 30% 2% xD |
| 02:27:19 | × | rekahsoft quits (~rekahsoft@70.51.99.245) (Ping timeout: 246 seconds) |
| 02:27:42 | <EvanR> | probability is so subjective |
| 02:29:39 | <monochrom> | Just rebrand, akak move the goalpost. If the chance of success drops, then speak of the chance of reproducing a heisenbug. >:) |
| 02:31:08 | <newmind> | or if you have 499 testcases that pass, and one that fails, guess which one is the interesting one? |
| 02:31:33 | <monochrom> | I guess moving the goalpost to the opposite side entirely is not what people think when they move the goalpost. >:) |
| 02:32:25 | <monochrom> | The 501st test case. :) |
| 02:32:58 | <monochrom> | "Forwarding thinking" |
| 02:35:47 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 02:40:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 02:46:30 | × | acidjnk quits (~acidjnk@p200300d6e7171923580d90e1926e8255.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 02:51:36 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 02:53:43 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 02:57:01 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 03:04:11 | → | mange joins (~mange@user/mange) |
| 03:07:24 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 03:11:15 | × | machinedgod quits (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 03:13:52 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 03:24:31 | → | annamalai joins (~annamalai@157.33.204.61) |
| 03:25:57 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 03:30:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 03:41:20 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 03:45:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 03:53:07 | × | haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 03:56:00 | × | omidmash quits (~omidmash@user/omidmash) (Quit: The Lounge - https://thelounge.chat) |
| 03:57:10 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 04:00:31 | → | omidmash joins (~omidmash@user/omidmash) |
| 04:01:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 04:01:56 | × | img quits (~img@user/img) (Quit: ZNC 1.10.1 - https://znc.in) |
| 04:03:09 | → | img joins (~img@user/img) |
| 04:06:28 | × | vidak quits (~vidak@2407:e400:7800:2c01:d0be:76f8:cc84:bd4a) (Quit: Konversation terminated!) |
| 04:12:55 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 04:16:25 | × | ryanbooker quits (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 04:17:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 04:28:19 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 04:32:31 | → | vidak joins (~vidak@180-150-95-190.b4965f.per.static.aussiebb.net) |
| 04:32:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 04:35:15 | trickard_ | is now known as trickard |
| 04:44:07 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 04:50:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 04:58:15 | → | takuan joins (~takuan@d8D86B9E9.access.telenet.be) |
| 05:02:10 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 05:06:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 05:08:06 | → | torn joins (~torn@91-133-90-252.dyn.cablelink.at) |
| 05:17:56 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 05:22:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 05:25:03 | × | Googulator14 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 05:25:25 | → | Googulator14 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 05:33:43 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 05:41:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 05:43:48 | → | michalz joins (~michalz@185.246.207.221) |
| 05:53:02 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 05:57:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 06:08:25 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 06:12:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 06:13:53 | → | karenw joins (~karenw@user/karenw) |
| 06:16:07 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 240 seconds) |
| 06:16:45 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 06:19:31 | × | karenw quits (~karenw@user/karenw) (Quit: Deep into that darkness peering...) |
| 06:19:45 | → | karenw joins (~karenw@user/karenw) |
| 06:21:23 | → | libertyprime joins (~libertypr@121.74.62.77) |
| 06:23:49 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 06:28:37 | × | jreicher quits (~joelr@user/jreicher) (Quit: bbs) |
| 06:28:58 | × | vidak quits (~vidak@180-150-95-190.b4965f.per.static.aussiebb.net) (Quit: Konversation terminated!) |
| 06:29:35 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 06:30:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 06:37:13 | × | mange quits (~mange@user/mange) (Remote host closed the connection) |
| 06:41:52 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 06:43:11 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 06:46:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 06:46:35 | → | jreicher joins (~joelr@user/jreicher) |
| 06:47:30 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 06:57:27 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 07:01:31 | × | AlexZenon quits (~alzenon@178.34.150.138) (Ping timeout: 265 seconds) |
| 07:02:34 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 07:05:34 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds) |
| 07:06:25 | × | libertyprime quits (~libertypr@121.74.62.77) (Quit: leaving) |
| 07:07:12 | → | AlexZenon joins (~alzenon@178.34.163.50) |
| 07:12:39 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 07:13:14 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 07:18:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 07:20:46 | → | vidak joins (~vidak@2407:e400:7800:2c01:d0be:76f8:cc84:bd4a) |
| 07:22:09 | × | annamalai quits (~annamalai@157.33.204.61) (Ping timeout: 252 seconds) |
| 07:26:04 | → | tromp joins (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) |
| 07:29:03 | → | merijn joins (~merijn@62.45.136.136) |
| 07:33:05 | → | halloy7365 joins (~halloy736@2407:7000:af54:9000:2d67:a726:905c:972e) |
| 07:33:49 | × | halloy7365 quits (~halloy736@2407:7000:af54:9000:2d67:a726:905c:972e) (Client Quit) |
| 07:34:07 | × | merijn quits (~merijn@62.45.136.136) (Ping timeout: 240 seconds) |
| 07:38:14 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 07:43:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 07:44:10 | × | housemate quits (~housemate@202.7.247.224) (Quit: https://ineedsomeacidtocalmmedown.space/) |
| 07:48:16 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 246 seconds) |
| 07:53:25 | × | stefan-_ quits (~cri@42dots.de) (Ping timeout: 264 seconds) |
| 07:54:02 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 07:54:18 | → | stefan-_ joins (~cri@42dots.de) |
| 07:55:14 | → | annamalai joins (~annamalai@157.33.203.8) |
| 07:55:31 | × | duckworld quits (~duckworld@user/duckworld) (Ping timeout: 240 seconds) |
| 07:58:42 | → | housemate joins (~housemate@202.7.247.224) |
| 07:58:46 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 08:09:48 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 08:09:51 | → | danza joins (~danza@user/danza) |
| 08:10:06 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:10:45 | → | duckworld joins (~duckworld@user/duckworld) |
| 08:13:34 | × | notzmv quits (~umar@user/notzmv) (Ping timeout: 244 seconds) |
| 08:15:01 | × | Square3 quits (~Square@user/square) (Ping timeout: 244 seconds) |
| 08:16:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 08:17:59 | × | synchromesh quits (~john@2406:5a00:2412:2c00:4db3:269e:6459:c957) (Read error: Connection reset by peer) |
| 08:18:59 | → | synchromesh joins (~john@2406:5a00:2412:2c00:d907:3b01:3c28:cb58) |
| 08:19:49 | × | lortabac quits (~lortabac@mx1.fracta.dev) (Ping timeout: 264 seconds) |
| 08:21:03 | → | lortabac joins (~lortabac@mx1.fracta.dev) |
| 08:30:11 | → | chele joins (~chele@user/chele) |
| 08:39:28 | → | orcus- joins (~orcus@user/brprice) |
| 08:39:37 | × | orcus quits (~orcus@user/brprice) (Ping timeout: 264 seconds) |
| 08:42:52 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 08:43:37 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Remote host closed the connection) |
| 08:46:15 | → | acidjnk joins (~acidjnk@p200300d6e7171973ed8816f9e416ce0a.dip0.t-ipconnect.de) |
| 08:49:35 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 08:56:55 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds) |
| 08:58:07 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 255 seconds) |
| 08:58:47 | → | merijn joins (~merijn@77.242.116.146) |
| 08:59:48 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 09:00:10 | <dutchie> | question about coerce: I have a newtype of NonEmpty (Map Text Value), and I want to write something like `modify (coerce $ NonEmpty.cons Map.empty)` but it doesn't typecheck |
| 09:00:16 | <dutchie> | (in a state monad) |
| 09:00:35 | <dutchie> | should coerce be able to do this? or am I missing what's going on |
| 09:00:45 | → | kuribas joins (~user@2a02-1810-2825-6000-e123-c17a-ed17-774f.ip6.access.telenet.be) |
| 09:01:02 | <dutchie> | the error is "Couldn't match representation of type ‘a0’ with that of ‘Value’` |
| 09:01:08 | <dutchie> | s/`/"/ |
| 09:03:08 | <danza> | :t cons |
| 09:03:10 | <lambdabot> | Cons s s a a => a -> s -> s |
| 09:04:47 | <danza> | cons is partially applied, so you are applying coerce to a function |
| 09:07:49 | Googulator14 | is now known as Googulator |
| 09:08:04 | <dutchie> | right, does that not work? I want to coerce `NonEmpty (Map) -> NonEmpty (Map)` to a function on my newtype |
| 09:08:26 | <dutchie> | so do I have to do `coerce . cons . coerce`? feels like I might as well explicitly unwrap/wrap then |
| 09:09:14 | <int-e> | presumably you need a type signature like (Map.empty :: Map Text Value) so that the inner type is actually fully known. |
| 09:09:43 | <merijn> | Map's key type is not coercible, afaik |
| 09:09:47 | <merijn> | At least, it shouldn't be |
| 09:09:55 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 240 seconds) |
| 09:10:03 | <dutchie> | ah explicit annotation on Map.empty does it |
| 09:10:12 | <int-e> | merijn: yeah but it's complaining about the Value type |
| 09:10:45 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 09:10:51 | <int-e> | and specifying the key type is less of a hassle than figuring out whether we have partial type signatures :P |
| 09:11:51 | × | tromp quits (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:12:16 | <danza> | what is the point of having a newtype if then you use coerce |
| 09:15:59 | <int-e> | dutchie: Btw there's an error message reading exercise here: it complains that it doesn't know that some `a0` and `Value` have the same representation. It's easy to guess where the `Value` comes from, but GHC should also tell you what it introduced `a0` for. |
| 09:21:15 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 09:22:48 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 09:25:52 | → | merijn joins (~merijn@77.242.116.146) |
| 09:30:55 | × | GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 240 seconds) |
| 09:31:42 | → | fp joins (~Thunderbi@2001-14ba-6e24-3000--198.rev.dnainternet.fi) |
| 09:32:30 | × | danza quits (~danza@user/danza) (Remote host closed the connection) |
| 09:32:58 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 09:33:26 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 09:34:44 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Quit: xff0x) |
| 09:40:02 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Read error: Connection reset by peer) |
| 09:40:11 | <dutchie> | it didn't mention the a0 or I probably would have figured it out :( |
| 09:40:12 | → | danza joins (~danza@user/danza) |
| 09:40:37 | <dutchie> | danza: I'm using the newtype to hide details outside the module but this is an internal function |
| 09:40:59 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 09:41:20 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 09:41:23 | ← | kuribas parts (~user@2a02-1810-2825-6000-e123-c17a-ed17-774f.ip6.access.telenet.be) (ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3)) |
| 09:45:23 | <danza> | i see, makes sense |
| 09:51:35 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 09:53:35 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 09:56:46 | × | jreicher quits (~joelr@user/jreicher) (Quit: brb) |
| 09:57:04 | × | karenw quits (~karenw@user/karenw) (Ping timeout: 246 seconds) |
| 10:03:51 | → | danz98640 joins (~danza@user/danza) |
| 10:05:07 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 252 seconds) |
| 10:05:26 | → | merijn joins (~merijn@77.242.116.146) |
| 10:05:55 | × | danza quits (~danza@user/danza) (Ping timeout: 240 seconds) |
| 10:06:27 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 10:10:01 | × | fp quits (~Thunderbi@2001-14ba-6e24-3000--198.rev.dnainternet.fi) (Ping timeout: 265 seconds) |
| 10:10:55 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 10:19:05 | → | gmg joins (~user@user/gehmehgeh) |
| 10:20:31 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 246 seconds) |
| 10:22:20 | × | bggd quits (~bgg@user/bggd) (Remote host closed the connection) |
| 10:22:49 | × | Vq quits (~vq@user/vq) (Ping timeout: 264 seconds) |
| 10:22:54 | → | merijn joins (~merijn@77.242.116.146) |
| 10:24:11 | → | Vq joins (~vq@user/vq) |
| 10:24:41 | → | notzmv joins (~umar@user/notzmv) |
| 10:25:27 | × | torn quits (~torn@91-133-90-252.dyn.cablelink.at) (Quit: Client closed) |
| 10:28:11 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 10:33:07 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 246 seconds) |
| 10:37:08 | → | tromp joins (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) |
| 10:40:44 | → | Tuplanolla joins (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) |
| 10:43:55 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 10:55:25 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 10:59:57 | → | fp joins (~Thunderbi@130.233.70.102) |
| 11:17:03 | → | xff0x joins (~xff0x@2405:6580:b080:900:1a94:9136:5419:ce9c) |
| 11:20:55 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 11:30:46 | → | jreicher joins (~joelr@user/jreicher) |
| 11:31:40 | × | Inline quits (~Inline@cgn-195-14-217-102.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/) |
| 11:34:52 | → | merijn joins (~merijn@77.242.116.146) |
| 11:38:12 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 11:38:42 | → | Inline joins (~Inline@cgn-195-14-217-102.nc.de) |
| 11:39:16 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 11:41:47 | → | gmg joins (~user@user/gehmehgeh) |
| 11:45:09 | → | weary-traveler joins (~user@user/user363627) |
| 11:52:13 | × | _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 256 seconds) |
| 11:52:30 | → | merijn joins (~merijn@77.242.116.146) |
| 11:55:41 | → | _d0t joins (~{-d0t-}@user/-d0t-/x-7915216) |
| 11:57:48 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Remote host closed the connection) |
| 11:58:04 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 12:02:05 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 252 seconds) |
| 12:05:19 | → | __monty__ joins (~toonn@user/toonn) |
| 12:11:01 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 12:12:55 | → | gmg joins (~user@user/gehmehgeh) |
| 12:23:46 | × | dequbed quits (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 255 seconds) |
| 12:32:24 | → | nadja joins (~dequbed@banana-new.kilobyte22.de) |
| 12:32:44 | × | nadja quits (~dequbed@banana-new.kilobyte22.de) (Client Quit) |
| 12:33:20 | × | Inline quits (~Inline@cgn-195-14-217-102.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/) |
| 12:33:43 | → | machinedgod joins (~machinedg@d75-159-126-101.abhsia.telus.net) |
| 12:34:55 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 12:37:23 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 12:38:20 | → | merijn joins (~merijn@77.242.116.146) |
| 12:41:37 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 12:41:50 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 12:43:39 | → | gmg joins (~user@user/gehmehgeh) |
| 12:43:55 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 12:48:10 | → | merijn joins (~merijn@77.242.116.146) |
| 12:52:30 | → | nadja joins (~dequbed@banana-new.kilobyte22.de) |
| 12:53:43 | × | s4msung quits (sdqoRqmCHs@user/s4msung) (Quit: s4msung) |
| 12:53:43 | × | yushyin quits (C2iywkXWw5@mail.karif.server-speed.net) (Quit: WeeChat 4.7.1) |
| 12:53:43 | × | noctuks quits (6ytiZUtHp5@user/noctux) (Quit: WeeChat 4.7.1) |
| 12:53:46 | → | Inline joins (~Inline@cgn-195-14-217-102.nc.de) |
| 12:54:19 | → | noctuks joins (rYHDFdD8sa@user/noctux) |
| 12:54:21 | → | yushyin joins (2oGK0f75bd@mail.karif.server-speed.net) |
| 12:54:24 | → | s4msung joins (zozxDe14NI@user/s4msung) |
| 13:01:08 | × | qqq quits (~qqq@185.54.21.105) (Quit: Lost terminal) |
| 13:10:23 | → | itaipu joins (~itaipu@168.121.99.54) |
| 13:13:55 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 13:15:01 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 13:15:59 | → | Typer_of_Terms joins (~Typer_of_@85.62.22.209) |
| 13:24:32 | × | hakutaku quits (~textual@chen.yukari.eu.org) (Remote host closed the connection) |
| 13:24:49 | → | hakutaku joins (~textual@chen.yukari.eu.org) |
| 13:27:00 | × | DetourNetworkUK quits (~DetourNet@user/DetourNetworkUK) (Read error: Connection reset by peer) |
| 13:28:18 | → | DetourNetworkUK joins (~DetourNet@user/DetourNetworkUK) |
| 13:29:18 | × | bliminse quits (~bliminse@user/bliminse) (Quit: leaving) |
| 13:33:04 | → | bliminse joins (~bliminse@user/bliminse) |
| 13:35:18 | trickard_ | is now known as trickard |
| 13:38:15 | → | poscat joins (~poscat@user/poscat) |
| 13:40:00 | × | poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 252 seconds) |
| 13:45:20 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 13:46:29 | × | newmind quits (~newmind@91-133-90-252.dyn.cablelink.at) (Quit: Client closed) |
| 13:47:11 | → | newmind joins (~newmind@91-133-90-252.dyn.cablelink.at) |
| 13:47:50 | × | Googulator quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 13:48:04 | → | Googulator joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 13:49:34 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 13:49:49 | × | Vq quits (~vq@user/vq) (Ping timeout: 264 seconds) |
| 13:49:54 | → | merijn joins (~merijn@77.242.116.146) |
| 13:51:32 | → | Vq joins (~vq@user/vq) |
| 14:03:46 | → | timide joins (~timide@user/timide) |
| 14:04:38 | → | danza joins (~danza@user/danza) |
| 14:07:13 | × | danz98640 quits (~danza@user/danza) (Ping timeout: 264 seconds) |
| 14:15:35 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 14:22:28 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 14:28:35 | × | pabs3 quits (~pabs3@user/pabs3) (Ping timeout: 240 seconds) |
| 14:31:04 | × | synchromesh quits (~john@2406:5a00:2412:2c00:d907:3b01:3c28:cb58) (Read error: Connection reset by peer) |
| 14:32:14 | → | pabs3 joins (~pabs3@user/pabs3) |
| 14:32:40 | → | synchromesh joins (~john@2406:5a00:2412:2c00:d907:3b01:3c28:cb58) |
| 14:34:02 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 14:34:16 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 14:39:18 | → | thenightmail joins (~thenightm@user/thenightmail) |
| 14:39:31 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 14:42:39 | → | merijn joins (~merijn@77.242.116.146) |
| 14:45:45 | trickard_ | is now known as trickard |
| 14:45:49 | × | danza quits (~danza@user/danza) (Remote host closed the connection) |
| 14:45:52 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 14:45:55 | × | duckworld quits (~duckworld@user/duckworld) (Ping timeout: 240 seconds) |
| 15:00:30 | → | duckworld joins (~duckworld@user/duckworld) |
| 15:04:39 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 15:08:21 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 15:16:50 | × | Googulator quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 15:17:07 | → | Googulator joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 15:17:28 | → | spew joins (~spew@user/spew) |
| 15:32:35 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 15:32:47 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 15:33:00 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 15:33:41 | jmcantrell_ | is now known as jmcantrell |
| 15:34:42 | → | Enrico63 joins (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) |
| 15:41:10 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 15:41:35 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 240 seconds) |
| 15:45:23 | × | tromp quits (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:49:10 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 246 seconds) |
| 16:01:23 | trickard_ | is now known as trickard |
| 16:04:31 | → | tromp joins (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) |
| 16:05:22 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 16:07:11 | → | danza joins (~danza@user/danza) |
| 16:09:22 | → | Lycurgus joins (~juan@user/Lycurgus) |
| 16:13:06 | → | comerijn joins (~merijn@77.242.116.146) |
| 16:15:35 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 16:15:42 | × | Googulator quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 16:15:48 | → | Googulator3 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 16:16:58 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 16:17:31 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 16:20:55 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 240 seconds) |
| 16:27:57 | × | newmind quits (~newmind@91-133-90-252.dyn.cablelink.at) (Quit: Client closed) |
| 16:34:04 | ← | Typer_of_Terms parts (~Typer_of_@85.62.22.209) () |
| 16:36:47 | → | newmind joins (~newmind@91-133-90-252.dyn.cablelink.at) |
| 16:40:59 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 16:45:04 | × | m_a_r_k quits (~m_a_r_k@archlinux/support/mark) (Ping timeout: 244 seconds) |
| 16:45:50 | → | Googulator46 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 16:46:16 | × | Googulator3 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 16:50:51 | → | m_a_r_k joins (~m_a_r_k@archlinux/support/mark) |
| 16:51:19 | × | fp quits (~Thunderbi@130.233.70.102) (Ping timeout: 240 seconds) |
| 16:57:01 | × | mulk quits (~mulk@pd95143a6.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 16:57:37 | → | mulk joins (~mulk@pd95143a6.dip0.t-ipconnect.de) |
| 16:59:29 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 17:00:46 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 17:01:00 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 17:03:40 | × | Enrico63 quits (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) (Quit: Client closed) |
| 17:03:57 | → | Enrico63 joins (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) |
| 17:13:06 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 17:13:15 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 17:16:09 | × | m_a_r_k quits (~m_a_r_k@archlinux/support/mark) (Remote host closed the connection) |
| 17:26:21 | → | m_a_r_k joins (~m_a_r_k@archlinux/support/mark) |
| 17:33:14 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 17:35:26 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:37:48 | × | tcard quits (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 17:38:06 | → | tcard joins (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 17:38:22 | × | Googulator46 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 17:38:41 | → | Googulator46 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 17:40:08 | → | comerijn joins (~merijn@77.242.116.146) |
| 17:40:09 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Read error: Connection reset by peer) |
| 17:42:44 | × | itaipu quits (~itaipu@168.121.99.54) (Read error: Connection timed out) |
| 17:48:05 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 17:48:48 | → | gmg joins (~user@user/gehmehgeh) |
| 17:51:51 | × | Enrico63 quits (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) (Ping timeout: 272 seconds) |
| 17:53:22 | → | chromoblob joins (~chromoblo@user/chromob1ot1c) |
| 18:00:46 | → | itaipu joins (~itaipu@168.121.99.54) |
| 18:03:09 | → | Enrico63 joins (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) |
| 18:03:56 | → | danz94513 joins (~danza@user/danza) |
| 18:04:27 | × | newmind quits (~newmind@91-133-90-252.dyn.cablelink.at) (Quit: Client closed) |
| 18:05:03 | × | danza quits (~danza@user/danza) (Read error: Connection reset by peer) |
| 18:09:53 | → | Square3 joins (~Square@user/square) |
| 18:12:39 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 18:15:49 | → | Googulator82 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 18:17:50 | × | Googulator46 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 18:18:01 | × | tromp quits (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:19:13 | × | mulk quits (~mulk@pd95143a6.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 18:19:20 | → | Milan_Vanca joins (~milan@user/Milan-Vanca:32634) |
| 18:20:10 | → | mulk joins (~mulk@pd95143a6.dip0.t-ipconnect.de) |
| 18:25:52 | → | newmind joins (~newmind@91-133-90-252.dyn.cablelink.at) |
| 18:27:24 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 18:28:53 | → | euphores joins (~SASL_euph@user/euphores) |
| 18:29:08 | → | tromp joins (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) |
| 18:37:13 | × | itaipu quits (~itaipu@168.121.99.54) (Ping timeout: 264 seconds) |
| 18:40:36 | × | synchromesh quits (~john@2406:5a00:2412:2c00:d907:3b01:3c28:cb58) (Read error: Connection reset by peer) |
| 18:40:51 | × | Leary quits (~Leary@user/Leary/x-0910699) (Remote host closed the connection) |
| 18:41:06 | → | Leary joins (~Leary@user/Leary/x-0910699) |
| 18:41:41 | → | synchromesh joins (~john@2406:5a00:2412:2c00:d907:3b01:3c28:cb58) |
| 18:45:10 | × | Everything quits (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving) |
| 18:56:14 | × | tromp quits (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:57:28 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 18:59:39 | → | itaipu joins (~itaipu@168.121.99.54) |
| 19:02:54 | → | tromp joins (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) |
| 19:03:47 | trickard_ | is now known as trickard |
| 19:03:49 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 19:05:36 | → | bggd joins (~bgg@user/bggd) |
| 19:06:49 | × | shr\ke quits (~shrike@user/shrke:31298) (Remote host closed the connection) |
| 19:17:15 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 240 seconds) |
| 19:20:04 | × | jreicher quits (~joelr@user/jreicher) (Quit: In transit) |
| 19:24:34 | × | Googulator82 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 19:24:50 | → | Googulator82 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 19:31:30 | → | Guest94 joins (~Guest94@2402:a00:402:648b:9145:dcf0:d0e8:6860) |
| 19:32:23 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 19:37:43 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 19:37:53 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 19:39:13 | Lord_of_Life_ | is now known as Lord_of_Life |
| 19:40:59 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 19:43:07 | × | ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Ping timeout: 256 seconds) |
| 19:43:35 | × | comerijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 19:46:17 | → | Guest63 joins (~Guest22@ip-005-147-245-066.um06.pools.vodafone-ip.de) |
| 19:50:30 | × | Guest63 quits (~Guest22@ip-005-147-245-066.um06.pools.vodafone-ip.de) (Client Quit) |
| 19:52:22 | → | comerijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 19:53:13 | <tomsmeding> | Everyone knows how foldl should never be used and you should use foldl' instead. Few people know that mapAccumL has _exactly_ the same issue, and there is no mapAccumL' in base |
| 19:53:27 | × | newmind quits (~newmind@91-133-90-252.dyn.cablelink.at) (Ping timeout: 272 seconds) |
| 19:54:22 | × | Guest94 quits (~Guest94@2402:a00:402:648b:9145:dcf0:d0e8:6860) (Quit: Client closed) |
| 19:54:50 | <larsivi> | fwiw, for a newbie coming from languages without use of weird little markers here and there, the little ' at the end there is not particularly easy to pick up :) |
| 19:54:57 | <monochrom> | mapAccumL is kind of going out of style because you can use the State monad instead, and you have multiple strictness options there. |
| 19:55:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 19:55:13 | × | itaipu quits (~itaipu@168.121.99.54) (Ping timeout: 264 seconds) |
| 19:55:20 | <tomsmeding> | in fact, mapAccumL is defined in terms of traverse with a lazy state monad |
| 19:56:10 | <tomsmeding> | monochrom: you could use a state monad, but you should be careful with moving away from plain list functions because you might miss out on fusion RULEs that can cost integer factors in performance |
| 19:56:15 | <haskellbridge> | <sm> yikes.. I am using that |
| 19:56:42 | <tomsmeding> | sm: if the list is not that long it's not that bad of a problem :) |
| 19:56:48 | <monochrom> | Ah. |
| 19:57:14 | <c_wraith> | yeah, mapAccumL is like the worst possible strictness behavior. |
| 19:57:15 | <tomsmeding> | (my post was inspired by optimising an application that, indirectly, applies these list functions to lists millions of elements long) |
| 19:57:23 | <larsivi> | Is there a list of all such things that are improved and shouldn't be used? Preferably with some explanations. |
| 19:57:25 | <dolio> | > foldl (\_ e -> e) (error "last: empty list") [1,2,3] |
| 19:57:26 | <lambdabot> | 3 |
| 19:57:32 | <dolio> | > foldl' (\_ e -> e) (error "last: empty list") [1,2,3] |
| 19:57:33 | <lambdabot> | *Exception: last: empty list |
| 19:57:33 | <lambdabot> | CallStack (from HasCallStack): |
| 19:57:33 | <lambdabot> | error, called at <interactive>:3:21 in interactive:Ghci1 |
| 19:57:55 | <monochrom> | As usual, a stricter mapAccumL is always welcome, but as usual again, we all vote that someone else should do it. |
| 19:58:00 | <tomsmeding> | dolio: ah nice, so that's the one counterexample :) |
| 19:58:02 | <haskellbridge> | <sm> https://hackage-content.haskell.org/package/infinite-list-0.1.3/docs/Data-List-Infinite.html#v:mapAccumL-39- seems to be the strict version |
| 19:58:28 | <c_wraith> | note that mapAccumL *does* have a way to sneak strictness in, and it's the worst possible way |
| 19:58:58 | <c_wraith> | you link evaluation of the state to evaluation of the map result, and force each map result sequentially before examining the final state |
| 19:59:14 | <Leary> | tomsmeding: The other countexample is on any traversable that isn't right-biased. |
| 19:59:34 | <tomsmeding> | I'm interested in lists only in this case, but yes :p |
| 19:59:34 | <monochrom> | Worst is a monad. pure :: a -> Worst a; join :: Worst (Worst a) -> Worst a. >:) |
| 19:59:38 | <c_wraith> | reverse is an example of something where foldl vs foldl' just doesn't matter |
| 20:00:09 | <dolio> | Yeah. It might make some microscopic difference, but not much. |
| 20:00:27 | <c_wraith> | if it does, the optimizer should be working harder. :) |
| 20:15:04 | → | newmind joins (~newmind@91-133-90-252.dyn.cablelink.at) |
| 20:15:36 | × | Googulator82 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 20:15:44 | → | Googulator82 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 20:21:24 | × | tromp quits (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:21:45 | <Leary> | @where dangerous |
| 20:21:45 | <lambdabot> | https://github.com/NorfairKing/haskell-dangerous-functions |
| 20:21:48 | <Leary> | larsivi: ^ |
| 20:22:11 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 250 seconds) |
| 20:22:26 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Quit: peterbecich) |
| 20:22:30 | → | tromp joins (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) |
| 20:23:53 | <EvanR> | yes foldl and foldl' are strictly (no pun intended) different beasts and not simply one is a more optimized version of the other |
| 20:24:03 | <EvanR> | which might be why we still have them |
| 20:25:11 | <EvanR> | larsivi, and foldl' was one of the first things covered in "tutorials" way back when. Once you see this, "primed" versions of other functions start to raise enough eyebrows to not be surprising |
| 20:25:50 | → | merijn joins (~merijn@77.242.116.146) |
| 20:25:56 | × | comerijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Read error: Connection reset by peer) |
| 20:28:11 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 20:30:29 | × | Googulator82 quits (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) (Quit: Client closed) |
| 20:30:52 | → | Googulator82 joins (~Googulato@2a01-036d-0106-4994-68db-cf64-05de-a70a.pool6.digikabel.hu) |
| 20:30:55 | × | yin quits (~zero@user/zero) (Ping timeout: 246 seconds) |
| 20:31:15 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 240 seconds) |
| 20:32:04 | → | haritz joins (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) |
| 20:32:05 | × | haritz quits (~hrtz@2a01:4b00:bc2e:7000:d5af:a266:ca31:5ef8) (Changing host) |
| 20:32:05 | → | haritz joins (~hrtz@user/haritz) |
| 20:33:55 | → | yin joins (~zero@user/zero) |
| 20:36:56 | → | pavonia joins (~user@user/siracusa) |
| 20:39:06 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 20:42:42 | → | jreicher joins (~joelr@user/jreicher) |
| 20:43:40 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 20:50:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 20:52:45 | <jreicher> | tomsmeding: I've sometimes wondered why foldl exists at all. |
| 20:53:30 | × | Enrico63 quits (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) (Quit: Client closed) |
| 20:54:27 | <monochrom> | It came from an old time when people did not notice or did not mind the space growth in e.g. foldl (+) |
| 20:55:43 | <monochrom> | and also when they just copied the standard libraries of other functional languages (and those languages are not lazy). |
| 20:56:16 | <tomsmeding> | jreicher: on lists, foldl is almost useless (`last` notwithstanding), but on general Foldables, foldl is just the mirror image of foldr |
| 20:56:51 | <jreicher> | monochrom: but why not "replace" foldl with foldl'? Even if you're copying the standard libraries from other languages, you don't need to keep the same implementation. |
| 20:56:54 | <tomsmeding> | so monochrom's explanation is historically correct (because foldl started out as a plain-list function), but these days, there is a reason for hvaing foldl |
| 20:56:56 | × | michalz quits (~michalz@185.246.207.221) (Remote host closed the connection) |
| 20:57:01 | <jreicher> | tomsmeding: yes, that's my point. if foldl is useless, why keep it? |
| 20:57:15 | <tomsmeding> | % :t foldl |
| 20:57:15 | <yahb2> | foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b |
| 20:57:51 | <tomsmeding> | jreicher: I just explained how foldl is not useless any more on certain types that are not [a] |
| 20:58:08 | <monochrom> | This community is too polite to delete things in the stdlib or on the wiki. :) |
| 20:58:51 | <monochrom> | I mean :( even >:( but it's a good day let's just :) |
| 20:58:53 | <tomsmeding> | in particular, if you have `data RevList a = Nil | Snoc (RevList a) a deriving (Foldable)`, then foldr will have the useless behaviour and foldl will be as useful as foldr is on [a] |
| 20:59:36 | <tomsmeding> | granted, [a] is much more common than RevList, but still, removing it now would be a bit brash |
| 20:59:41 | → | Enrico63 joins (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) |
| 20:59:56 | <monochrom> | OK yeah Foldable should have all 4 combinations and then you choose the best one for the actual use case. |
| 20:59:57 | → | itaipu joins (~itaipu@168.121.99.54) |
| 21:00:40 | <tomsmeding> | (and indeed, Foldable does have foldr' since GHC 7.6 :p) |
| 21:01:19 | <jreicher> | I can't shake the feeling that it shouldn't be necessary to have four instead of two, but I can't assemble a coherent argument just at the moment. |
| 21:01:23 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 21:01:50 | <monochrom> | > foldr (&&) False (False : undefined) |
| 21:01:51 | <lambdabot> | False |
| 21:01:58 | <monochrom> | I don't want your foldr' for that. |
| 21:02:15 | <tomsmeding> | jreicher: you can reduce it to two: foldMap and foldMap' |
| 21:02:16 | <monochrom> | But I would want your foldr' for some other data structure. |
| 21:02:25 | × | ridcully quits (~ridcully@pd951fc06.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 21:02:43 | → | ridcully joins (~ridcully@pd951f83e.dip0.t-ipconnect.de) |
| 21:03:10 | <monochrom> | My point is that I want to be allowed to choose between foldr and foldr' and you don't know a priori which one is best for me. |
| 21:04:15 | <dolio> | Yes, the only question is which one gets which name. |
| 21:04:44 | <tomsmeding> | a prime for a strict version is so entrenched at this point that doing it the other way round would be a crime. :) |
| 21:04:56 | <ncf> | if we had better identifiers we could have foldl! for the strict version |
| 21:05:17 | <tomsmeding> | (that always makes me think of Ruby's chop!) |
| 21:05:19 | <monochrom> | Oh haha that inspires me. foldr' and foldr_ to make it more confusing. :) |
| 21:05:55 | <monochrom> | What is Ruby's chop? Is it similar to Prolog's cut? |
| 21:05:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 21:06:04 | <tomsmeding> | no, it just sounds funny with the ! |
| 21:06:12 | <dolio> | It's in-place trimming or something. |
| 21:06:35 | × | Enrico63 quits (~Enrico63@host-95-251-99-143.retail.telecomitalia.it) (Quit: Client closed) |
| 21:06:45 | <dolio> | Exclamation points indicate mutation, I think. |
| 21:07:02 | monochrom | invents Prolog's dice, which means "if random() > 0.5 then cut else nop", so literally dice in two senses. >:) |
| 21:07:23 | <monochrom> | Oh, like Perl's chop. |
| 21:07:27 | <dolio> | Yeah. |
| 21:07:39 | <monochrom> | @stab monochrom |
| 21:07:39 | lambdabot | throws some pointy lambdas at monochrom |
| 21:07:40 | × | trickard quits (~trickard@cpe-50-98-47-163.wireline.com.au) (Ping timeout: 246 seconds) |
| 21:07:42 | <monochrom> | @stab monochrom |
| 21:07:42 | lambdabot | pulls monochrom through the Evil Mangler |
| 21:07:45 | <monochrom> | @stab monochrom |
| 21:07:45 | lambdabot | moulds monochrom into a delicous cookie, and places it in her oven |
| 21:08:06 | → | trickard_ joins (~trickard@cpe-50-98-47-163.wireline.com.au) |
| 21:08:14 | <monochrom> | There is one that says "chop ... into pieces" or something like that. |
| 21:09:40 | <monochrom> | Oh haha there is also a Banach-Tarski one. :) |
| 21:10:05 | <darkling> | monochrommonochrom. An anagram. :) |
| 21:10:30 | <monochrom> | haha |
| 21:11:17 | <monochrom> | I think the mathematicians also have a joke along the line of "what's the anagram of Banach-Tarski" |
| 21:11:36 | <darkling> | That's the joke I was thinking of. |
| 21:11:51 | <monochrom> | hehe |
| 21:17:11 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 21:18:08 | Square3 | is now known as Square |
| 21:21:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 21:24:12 | × | Vizious quits (~bes@user/Vizious) (Quit: WeeChat 4.8.1) |
| 21:24:23 | <EvanR> | we spend a lot of time hating on foldl because we think we understand it and think it's completely useless. But if we didn't dwell on foldl so much, we might miss all the other things in the standard library which potentially blow up in your face and don't have real answers |
| 21:25:01 | <EvanR> | we'd have like 10 different other foldl situations and the conversion would get kind of confusing |
| 21:25:23 | <EvanR> | the whole drama stems from haskell's laziness, which you can't really escape |
| 21:25:27 | <EvanR> | you have to understand it |
| 21:26:41 | <EvanR> | I'm thinking of the various Writer monads |
| 21:29:18 | <EvanR> | jreicher, on the subject of how many folds you need in Foldable... there's a huge number of other folding strategies other than left fold and right fold, just for a tree-like DS |
| 21:30:01 | × | mulk quits (~mulk@pd95143a6.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 21:30:04 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 246 seconds) |
| 21:30:05 | <EvanR> | fold being for the special case where all possible folds result in the same answer (a monoidal fold) |
| 21:30:31 | → | mulk joins (~mulk@pd95143a6.dip0.t-ipconnect.de) |
| 21:31:19 | → | jmcantrell_ joins (~weechat@user/jmcantrell) |
| 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 |
| 21:32:26 | <EvanR> | though* |
| 21:32:58 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 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. |
| 21:34:01 | × | Milan_Vanca quits (~milan@user/Milan-Vanca:32634) (Quit: WeeChat 4.7.2) |
| 21:34:48 | × | spew quits (~spew@user/spew) (Quit: nyaa~) |
| 21:36:03 | <EvanR> | however the situation with sum |
| 21:36:08 | <EvanR> | @src sum |
| 21:36:08 | <lambdabot> | sum = foldl (+) 0 |
| 21:36:25 | <EvanR> | this is probably dumb |
| 21:36:26 | trickard_ | is now known as trickard |
| 21:38:08 | <tomsmeding> | it is, but that was fixed; sum is now defined using foldl' |
| 21:38:25 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 21:38:33 | <EvanR> | good |
| 21:38:35 | <jreicher> | Oww. How did that happen in the first place? |
| 21:39:09 | <tomsmeding> | that one was probably just an oversight |
| 21:39:44 | <EvanR> | maybe, but there was a long thread on the mailing list defending the foldl version xD |
| 21:40:04 | <EvanR> | a long time ago |
| 21:40:09 | <tomsmeding> | there are probably contrived Num instances for which foldl' would be inappropriate |
| 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 |
| 21:41:08 | <EvanR> | (curiously) Foldable ended up being more principled and based than Num |
| 21:41:19 | <tomsmeding> | Num was never principled or based in any way |
| 21:41:21 | <EvanR> | most things people try to write a Num instance for are contrived xD |
| 21:41:23 | <tomsmeding> | so that's a low bar |
| 21:41:43 | <tomsmeding> | I've ranted about Num before here |
| 21:42:02 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 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 |
| 21:43:18 | <mauke> | comfortably Num |
| 21:43:58 | <Leary> | `Foldable` just doesn't need laws, since the type of `foldMap` and parametricity say it all. |
| 21:48:46 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 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. |
| 21:50:25 | <monochrom> | You need a law to outlaw me trying "foldMap _ _ = mempty". |
| 21:50:51 | <Leary> | monochrom: But sometimes that's the correct implementation. :) |
| 21:59:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 22:00:43 | Googulator82 | is now known as Googulator |
| 22:00:58 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 22:03:09 | × | malte quits (~malte@mal.tc) (Ping timeout: 250 seconds) |
| 22:03:31 | <EvanR> | zero and one |
| 22:03:39 | <EvanR> | and a law saying they must be different? xD |
| 22:04:26 | <geekosaur> | they're allowed to be the same… if there's only one value in the set |
| 22:04:32 | → | malte joins (~malte@mal.tc) |
| 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 |
| 22:04:37 | → | danza joins (~danza@user/danza) |
| 22:05:21 | <monochrom> | I agree. |
| 22:05:30 | <EvanR> | though we have good examples where they are, in crypto code |
| 22:06:49 | × | danz94513 quits (~danza@user/danza) (Ping timeout: 246 seconds) |
| 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 |
| 22:08:10 | <haskellbridge> | <loonycyborg> you can even divide by zero in this ring |
| 22:11:19 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 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) |
| 22:14:24 | → | xff0x_ joins (~xff0x@2405:6580:b080:900:cd9:802b:8b60:b254) |
| 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" |
| 22:15:20 | tomsmeding | doesn't follow; doesn't that assume a*0 = 0 from the get go? |
| 22:15:24 | <TMA> | tomsmeding: I have encountered ring definition containing the axiom 0!=1 as well |
| 22:15:30 | jmcantrell_ | is now known as jmcantrell |
| 22:16:10 | <monochrom> | 0 is axiomatized by "forall a, a*0 = 0". |
| 22:16:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 22:16:26 | <monochrom> | To be sure I need a separate proof why it's unique. |
| 22:16:27 | tomsmeding | is reading https://en.wikipedia.org/wiki/Ring_(mathematics) |
| 22:16:32 | <geekosaur> | that was what I thought |
| 22:16:34 | <tomsmeding> | this axiomatises 0 as the additive unit |
| 22:16:39 | × | xff0x quits (~xff0x@2405:6580:b080:900:1a94:9136:5419:ce9c) (Ping timeout: 260 seconds) |
| 22:16:49 | <geekosaur> | 0 is required to be an annihilating element in multiplication |
| 22:16:51 | <monochrom> | Oh oops, sorry! Delete everything I said. |
| 22:17:06 | <tomsmeding> | geekosaur: no, because you can prove it so it need not be an axiom :p |
| 22:17:16 | <geekosaur> | but I think that's derived, not amxiom |
| 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 |
| 22:18:47 | <ncf> | a * 0 = a * (1 - 1) = a - a = 0 ? |
| 22:19:02 | <TMA> | 0*a = (x-x)*a = xa - xa = 0 for any x |
| 22:19:32 | <tomsmeding> | ncf: thank you |
| 22:19:38 | <tomsmeding> | oh also TMA :) |
| 22:19:47 | <Leary> | That still relies on `a * -1 = -a`. |
| 22:19:49 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 22:20:17 | <TMA> | the other order of operands need showing (-1)*a = a*(-1) |
| 22:21:59 | <Leary> | a * -0 = a * (-0 + 0) = a * -0 + a * 0 ==> a * 0 = 0 (by cancellation) |
| 22:22:53 | <ncf> | Leary++ |
| 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 |
| 22:24:16 | <Leary> | Actually the -0 could have been anything, should have just used 0. |
| 22:24:29 | <monochrom> | :) |
| 22:24:38 | → | AlexNoo joins (~AlexNoo@178.34.163.50) |
| 22:25:38 | <ncf> | 0 = a * 0 - a * 0 = a * (0 + 0) - a * 0 = a * 0 + a * 0 - a * 0 = a * 0 |
| 22:26:51 | <tomsmeding> | nice |
| 22:26:52 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 22:27:34 | × | Digit quits (~user@user/digit) (Remote host closed the connection) |
| 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? |
| 22:28:19 | <Leary> | Yes. |
| 22:31:24 | × | carbolymer quits (~carbolyme@delirium.systems) (Read error: Connection reset by peer) |
| 22:31:31 | × | ncf quits (~n@monade.li) (Ping timeout: 264 seconds) |
| 22:31:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 22:31:59 | → | carbolymer joins (~carbolyme@delirium.systems) |
| 22:33:08 | → | ncf joins (~n@monade.li) |
| 22:36:47 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 252 seconds) |
| 22:38:59 | → | Digit joins (~user@user/digit) |
| 22:40:04 | × | carbolymer quits (~carbolyme@delirium.systems) () |
| 22:40:14 | → | carbolymer joins (~carbolyme@delirium.systems) |
| 22:40:38 | × | tromp quits (~textual@2001:1c00:3487:1b00:a460:d351:8685:d1f0) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:41:05 | × | carbolymer quits (~carbolyme@delirium.systems) (Client Quit) |
| 22:41:33 | → | carbolymer joins (carbolymer@delirium.systems) |
| 22:42:38 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 22:43:49 | → | gmg joins (~user@user/gehmehgeh) |
| 22:45:15 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 22:46:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 22:47:15 | × | ncf quits (~n@monade.li) (Ping timeout: 244 seconds) |
| 22:47:55 | × | carbolymer quits (carbolymer@delirium.systems) (Ping timeout: 240 seconds) |
| 22:52:36 | → | ncf joins (~n@monade.li) |
| 22:53:57 | → | carbolymer joins (~carbolyme@delirium.systems) |
| 22:58:05 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 23:02:39 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 252 seconds) |
| 23:02:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 23:04:30 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 23:05:01 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 252 seconds) |
| 23:09:03 | × | gehmehgeh quits (~user@user/gehmehgeh) (Ping timeout: 252 seconds) |
| 23:13:52 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 23:16:33 | → | gmg joins (~user@user/gehmehgeh) |
| 23:21:01 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 23:26:31 | × | jmcantrell quits (~weechat@user/jmcantrell) (Ping timeout: 240 seconds) |
| 23:27:44 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:31:55 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 23:36:35 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 23:46:51 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 23:47:42 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 23:51:28 | × | rainbyte quits (~rainbyte@186.22.19.214) (Quit: rainbyte) |
| 23:52:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 23:56:16 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
All times are in UTC on 2026-01-08.