| 2026-06-23 00:01:36 +0000 | dtman34 | (~dtman34@2601:447:d17d:eaf2:8123:c1ff:6dae:d26b) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2026-06-23 00:01:43 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-23 00:01:59 +0000 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) dtman34 |
| 2026-06-23 00:12:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 00:17:45 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-23 00:28:15 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 00:33:03 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-23 00:35:17 +0000 | xff0x | (~xff0x@2405:6580:b080:900:df45:9308:76fe:d30b) (Quit: xff0x) |
| 2026-06-23 00:36:49 +0000 | xff0x | (~xff0x@2405:6580:b080:900:a40e:e1eb:bacb:147b) |
| 2026-06-23 00:37:46 +0000 | czan | (~czan@user/mange) czan |
| 2026-06-23 00:41:35 +0000 | CloneOfNone | (~CloneOfNo@user/CloneOfNone) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-06-23 00:43:37 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 00:48:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 00:48:28 +0000 | CloneOfNone | (~CloneOfNo@user/CloneOfNone) CloneOfNone |
| 2026-06-23 00:50:06 +0000 | xff0x | (~xff0x@2405:6580:b080:900:a40e:e1eb:bacb:147b) (Ping timeout: 252 seconds) |
| 2026-06-23 00:50:09 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) (Ping timeout: 246 seconds) |
| 2026-06-23 00:56:01 +0000 | divya- | (divya@140.238.251.170) divya |
| 2026-06-23 00:57:43 +0000 | divya- | divya |
| 2026-06-23 00:58:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 01:02:58 +0000 | tremon | (~tremon@83-80-159-219.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in) |
| 2026-06-23 01:03:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-06-23 01:03:41 +0000 | Enigmagic | (~Enigmagic@user/Enigmagic) Enigmagic |
| 2026-06-23 01:13:51 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 271 seconds) |
| 2026-06-23 01:14:22 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 01:19:20 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-06-23 01:24:17 +0000 | bdkl | (~bdkl@user/bdkl) bdkl |
| 2026-06-23 01:29:55 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 01:34:31 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-23 01:35:46 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-23 01:39:36 +0000 | bdkl | (~bdkl@user/bdkl) (Quit: bdkl) |
| 2026-06-23 01:45:20 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-23 01:45:38 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-23 01:49:29 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 245 seconds) |
| 2026-06-23 01:58:07 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-06-23 02:00:39 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 02:06:02 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) (Ping timeout: 248 seconds) |
| 2026-06-23 02:07:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-06-23 02:11:29 +0000 | td_ | (~td@i53870915.versanet.de) (Ping timeout: 256 seconds) |
| 2026-06-23 02:13:14 +0000 | td_ | (~td@i53870934.versanet.de) |
| 2026-06-23 02:16:00 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 02:22:36 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-06-23 02:28:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 02:36:08 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 02:36:12 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 256 seconds) |
| 2026-06-23 02:43:28 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 02:45:36 +0000 | yin | (~zero@user/zero) (Ping timeout: 252 seconds) |
| 2026-06-23 02:46:06 +0000 | emilym | (~Thunderbi@user/emilym) emilym |
| 2026-06-23 02:48:16 +0000 | statusbot8 | (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) statusbot |
| 2026-06-23 02:48:18 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-06-23 02:48:58 +0000 | AlexNoo_ | (~AlexNoo@178.34.150.149) |
| 2026-06-23 02:50:19 +0000 | emilym | (~Thunderbi@user/emilym) (Ping timeout: 245 seconds) |
| 2026-06-23 02:51:09 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 245 seconds) |
| 2026-06-23 02:51:59 +0000 | AlexNoo | (~AlexNoo@178.34.150.149) (Ping timeout: 245 seconds) |
| 2026-06-23 02:51:59 +0000 | statusbot | (~statusbot@ec2-34-198-122-184.compute-1.amazonaws.com) (Ping timeout: 245 seconds) |
| 2026-06-23 02:55:23 +0000 | yin | (~zero@user/zero) zero |
| 2026-06-23 02:58:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 03:03:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 03:03:14 +0000 | mulk | (~mulk@p5b112c49.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-06-23 03:05:19 +0000 | siraben | (~siraben@user/siraben) (Ping timeout: 245 seconds) |
| 2026-06-23 03:06:13 +0000 | mulk | (~mulk@p5b112c49.dip0.t-ipconnect.de) mulk |
| 2026-06-23 03:06:34 +0000 | czan | (~czan@user/mange) (Ping timeout: 245 seconds) |
| 2026-06-23 03:08:40 +0000 | siraben | (~siraben@user/siraben) siraben |
| 2026-06-23 03:09:04 +0000 | foul_owl | (~kerry@94.156.149.95) (Ping timeout: 245 seconds) |
| 2026-06-23 03:09:08 +0000 | mesaoptimizer | (~user@user/PapuaHardyNet) (Remote host closed the connection) |
| 2026-06-23 03:09:09 +0000 | rekahsoft | (~rekahsoft@70.51.99.119) (Remote host closed the connection) |
| 2026-06-23 03:11:23 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-06-23 03:13:46 +0000 | foul_owl | (~kerry@94.156.149.95) foul_owl |
| 2026-06-23 03:14:11 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 03:19:28 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-06-23 03:29:40 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-23 03:34:08 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 252 seconds) |
| 2026-06-23 03:44:56 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 03:49:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-06-23 04:00:18 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 04:06:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 04:12:25 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) (Ping timeout: 248 seconds) |
| 2026-06-23 04:18:15 +0000 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2026-06-23 04:18:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 04:22:53 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2026-06-23 04:25:43 +0000 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-06-23 04:29:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 04:33:45 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-23 04:35:30 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2026-06-23 04:35:45 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2026-06-23 04:43:09 +0000 | michalz | (~michalz@185.246.207.221) |
| 2026-06-23 04:44:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 04:49:34 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-06-23 04:59:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 05:00:30 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 268 seconds) |
| 2026-06-23 05:01:59 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-06-23 05:04:15 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-06-23 05:13:56 +0000 | ft | (~ft@p508db6b1.dip0.t-ipconnect.de) (Quit: leaving) |
| 2026-06-23 05:15:11 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 05:19:25 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 243 seconds) |
| 2026-06-23 05:29:01 +0000 | acidjnk | (~acidjnk@p200300d6e700e5277500ddb9aa62921b.dip0.t-ipconnect.de) acidjnk |
| 2026-06-23 05:29:12 +0000 | acidjnk_new3 | (~acidjnk@p200300d6e700e5277500ddb9aa62921b.dip0.t-ipconnect.de) |
| 2026-06-23 05:30:05 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 05:34:42 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-23 05:38:50 +0000 | puke | (~puke@user/puke) (Quit: puke) |
| 2026-06-23 05:45:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 05:51:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 05:57:57 +0000 | traxex | (traxex@user/traxex) traxex |
| 2026-06-23 06:03:30 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 06:07:57 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-06-23 06:18:49 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 06:21:34 +0000 | <gentauro> | lately, I've been given these suggestions in my IDE (emacs) -> `✲ Name: Infinite: ghc-internal/length`. Is there a way to use a `[]` with the built-in logic and not getting those? |
| 2026-06-23 06:23:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 261 seconds) |
| 2026-06-23 06:30:21 +0000 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) (Ping timeout: 246 seconds) |
| 2026-06-23 06:31:04 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 06:35:18 +0000 | jle` | (~jle`@23.240.67.73) (Quit: WeeChat 4.8.1) |
| 2026-06-23 06:35:57 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-06-23 06:38:22 +0000 | jle` | (~jle`@2603:8001:3b00:11:181d:91a8:37ba:ce0c) jle` |
| 2026-06-23 06:43:22 +0000 | karenw_ | (~karenw@user/karenw) karenw |
| 2026-06-23 06:47:01 +0000 | picnoir | (~picnoir@about/aquilenet/vodoo/NinjaTrappeur) NinjaTrappeur |
| 2026-06-23 06:48:09 +0000 | <pavonia> | What is that message even saying? |
| 2026-06-23 06:52:36 +0000 | <gentauro> | pavonia: I'm just using `length` on a standard list. |
| 2026-06-23 06:52:39 +0000 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-06-23 06:53:23 +0000 | <gentauro> | I'm guessing that (which is correct) that calling `length` on an infinete list could be problematic. But, we don't have dependent types in Haskell right? (Idris comes to mind) |
| 2026-06-23 06:55:22 +0000 | <gentauro> | I really appreciate the messages when using `head` as that could make an application crash on empty list (correct way would be doing pattern-matching). But on `length`? What's the alternative to that? |
| 2026-06-23 06:56:36 +0000 | <pavonia> | No idea, tbh. You can't really check whether a list is infinite |
| 2026-06-23 06:58:57 +0000 | dextaa | (~DV@user/dextaa) (Ping timeout: 271 seconds) |
| 2026-06-23 07:00:59 +0000 | <probie> | I think both are equally valid warnings. `head` is a partial function and `length` is not a productive function |
| 2026-06-23 07:01:56 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-23 07:03:17 +0000 | <pavonia> | How would you check the length of a list in a productive way then? |
| 2026-06-23 07:03:54 +0000 | <probie> | `data N = Z | S N`, `length = foldr (const S) Z` |
| 2026-06-23 07:04:04 +0000 | <gentauro> | hmmm, perhaps that now that I have push access to Hackage. Maybe I should invest time to add my `Data.Array.Log{32|64|128|256}` -> https://blog.stermon.org/articles/2020/05/22/haskell-data-array-log256-safe-idiomatic-and-bottom.h… |
| 2026-06-23 07:06:34 +0000 | <gentauro> | `length (A l _) = l` 👍 |
| 2026-06-23 07:06:58 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 276 seconds) |
| 2026-06-23 07:08:57 +0000 | <pavonia> | probie: But isn't that just deferring the problem to other functions? If you want to do comparisons with the length of the list you could run into the same issue |
| 2026-06-23 07:09:20 +0000 | <probie> | You can compare an `Int` against the length of a list |
| 2026-06-23 07:09:59 +0000 | <probie> | What you can't do is compare the length of two lists or treat the length as an Int |
| 2026-06-23 07:10:03 +0000 | chele | (~chele@user/chele) chele |
| 2026-06-23 07:10:13 +0000 | <probie> | (if you still want your code to be total) |
| 2026-06-23 07:11:36 +0000 | <pavonia> | Right. To me this seems like a too restrictive check |
| 2026-06-23 07:14:06 +0000 | <probie> | > let n `compareWithLength` xs = foldr (\x k acc -> if acc <= 0 then LT else k $! (acc - 1)) (\acc -> if acc == 0 then EQ else GT) xs n in (42 `compareWithLength` [1..5], 42 `compareWithLength` [1..42], 42 `compareWithLength` [1..]) |
| 2026-06-23 07:14:07 +0000 | <lambdabot> | (GT,EQ,LT) |
| 2026-06-23 07:15:50 +0000 | <probie> | If you want to make `length` total, just stick `take n` (for some large n) in front of the list you're calling `length` on |
| 2026-06-23 07:16:34 +0000 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2026-06-23 07:19:30 +0000 | <probie> | To clarify, I think it's a silly rule to raise a warning about, but not that much more silly than the one for `head` |
| 2026-06-23 07:20:11 +0000 | <gentauro> | probie: tbh, `head` shouldn't even exists in the first place … |
| 2026-06-23 07:20:31 +0000 | <gentauro> | pattern-matching SHOULD be the way |
| 2026-06-23 07:21:41 +0000 | <probie> | We're allowed to diverge right, so you're happy with `head xs = case xs of { x:_ -> x; [] -> let x = x in x }` since it's as "total" as `length` |
| 2026-06-23 07:23:32 +0000 | fp1 | (~Thunderbi@130.233.70.229) fp |
| 2026-06-23 07:23:34 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) |
| 2026-06-23 07:23:43 +0000 | <mauke> | :t length . take maxBound |
| 2026-06-23 07:23:44 +0000 | <lambdabot> | [a] -> Int |
| 2026-06-23 07:24:50 +0000 | merijn | (~merijn@2a02:a420:22df:d034:8458:927c:ac6e:3896) merijn |
| 2026-06-23 07:25:54 +0000 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-06-23 07:34:57 +0000 | <gentauro> | mauke: `length . take maxBound` -> `✲ Name: Infinite: ghc-internal/length` |
| 2026-06-23 07:37:18 +0000 | <mauke> | > (length . take maxBound) [0 ..] |
| 2026-06-23 07:37:25 +0000 | <lambdabot> | *Exception: <<timeout>> |
| 2026-06-23 07:37:41 +0000 | <humasect> | ah i miss haskell . |
| 2026-06-23 07:39:51 +0000 | <gentauro> | > (length . take maxBound) [0 :: Int16 ..] |
| 2026-06-23 07:39:52 +0000 | <lambdabot> | 32768 |
| 2026-06-23 07:40:15 +0000 | karenw_ | (~karenw@user/karenw) (Quit: Deep into that darkness peering...) |
| 2026-06-23 07:42:14 +0000 | terrorjack | (~terrorjac@2a01:4f8:271:2d98::2) (Quit: The Lounge - https://thelounge.chat) |
| 2026-06-23 07:46:41 +0000 | terrorjack | (~terrorjac@2a01:4f8:271:2d98::2) terrorjack |
| 2026-06-23 07:52:09 +0000 | merijn | (~merijn@2a02:a420:22df:d034:8458:927c:ac6e:3896) (Ping timeout: 248 seconds) |
| 2026-06-23 07:56:06 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 245 seconds) |
| 2026-06-23 07:56:06 +0000 | yanmaani | (~yanmaani@gateway/tor-sasl/yanmaani) (Ping timeout: 245 seconds) |
| 2026-06-23 07:56:13 +0000 | califax_ | (~califax@user/califx) califx |
| 2026-06-23 07:56:31 +0000 | califax | (~califax@user/califx) (Ping timeout: 245 seconds) |
| 2026-06-23 07:56:31 +0000 | gmg | (~user@user/gehmehgeh) (Ping timeout: 245 seconds) |
| 2026-06-23 07:56:31 +0000 | tusko | (~uwu@user/tusko) (Ping timeout: 245 seconds) |
| 2026-06-23 07:56:53 +0000 | yanmaani | (~yanmaani@gateway/tor-sasl/yanmaani) yanmaani |
| 2026-06-23 07:56:59 +0000 | tusko | (~uwu@user/tusko) tusko |
| 2026-06-23 07:57:05 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2026-06-23 07:57:27 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-06-23 07:57:27 +0000 | califax_ | califax |
| 2026-06-23 08:04:38 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-23 08:12:24 +0000 | mesaoptimizer | (~user@user/PapuaHardyNet) PapuaHardyNet |
| 2026-06-23 08:12:42 +0000 | mesaoptimizer | (~user@user/PapuaHardyNet) (Client Quit) |
| 2026-06-23 08:13:31 +0000 | mesaoptimizer | (~user@user/PapuaHardyNet) PapuaHardyNet |
| 2026-06-23 08:13:32 +0000 | acidjnk_new | (~acidjnk@p200300d6e700e585726eb65abab086aa.dip0.t-ipconnect.de) |
| 2026-06-23 08:16:49 +0000 | acidjnk_new3 | (~acidjnk@p200300d6e700e5277500ddb9aa62921b.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2026-06-23 08:16:50 +0000 | acidjnk | (~acidjnk@p200300d6e700e5277500ddb9aa62921b.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2026-06-23 08:17:46 +0000 | acidjnk | (~acidjnk@p200300d6e700e585726eb65abab086aa.dip0.t-ipconnect.de) acidjnk |
| 2026-06-23 08:23:37 +0000 | olivial | (~benjaminl@user/benjaminl) (Ping timeout: 248 seconds) |
| 2026-06-23 08:25:52 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-23 08:27:42 +0000 | CiaoSen | (~Jura@2a02:3100:6065:ab00:4e50:ddff:fe9b:8922) CiaoSen |
| 2026-06-23 08:28:44 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 08:30:36 +0000 | danza | (~danza@user/danza) danza |
| 2026-06-23 08:32:59 +0000 | olivial | (~benjaminl@user/benjaminl) benjaminl |
| 2026-06-23 08:38:59 +0000 | bggd__ | (~bgg@2a01:e0a:fd5:f510:8e31:1731:15f3:2843) |
| 2026-06-23 08:40:35 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2026-06-23 08:40:35 +0000 | m_a_r_k | (~m_a_r_k@archlinux/support/mark) (Ping timeout: 245 seconds) |
| 2026-06-23 08:42:00 +0000 | bggd_ | (~bgg@2a01:e0a:fd5:f510:8949:3630:d504:97ee) (Ping timeout: 252 seconds) |
| 2026-06-23 08:43:30 +0000 | m_a_r_k | (~m_a_r_k@archlinux/support/mark) m_a_r_k |
| 2026-06-23 08:45:18 +0000 | CiaoSen | (~Jura@2a02:3100:6065:ab00:4e50:ddff:fe9b:8922) (Ping timeout: 252 seconds) |
| 2026-06-23 08:45:36 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 08:49:16 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-06-23 08:50:56 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 268 seconds) |
| 2026-06-23 08:52:06 +0000 | ThePenguin | (~ThePengui@83-233-229-100.cust.bredband2.com) (Ping timeout: 246 seconds) |
| 2026-06-23 08:53:06 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 08:54:57 +0000 | ThePenguin | (~ThePengui@83-233-229-100.cust.bredband2.com) ThePenguin |
| 2026-06-23 09:03:55 +0000 | fp1 | (~Thunderbi@130.233.70.229) (Ping timeout: 245 seconds) |
| 2026-06-23 09:05:44 +0000 | foul_owl | (~kerry@94.156.149.95) (Ping timeout: 245 seconds) |
| 2026-06-23 09:06:04 +0000 | schuelermine | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-06-23 09:07:44 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) |
| 2026-06-23 09:20:14 +0000 | foul_owl | (~kerry@94.156.149.95) foul_owl |
| 2026-06-23 09:21:52 +0000 | prdak1 | (~Thunderbi@user/prdak) prdak |
| 2026-06-23 09:23:43 +0000 | prdak | (~Thunderbi@user/prdak) (Ping timeout: 264 seconds) |
| 2026-06-23 09:23:43 +0000 | prdak1 | prdak |
| 2026-06-23 09:27:43 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-23 09:32:00 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) Inline |
| 2026-06-23 09:40:09 +0000 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) lisbeths |
| 2026-06-23 09:40:56 +0000 | karenw_ | (~karenw@user/karenw) karenw |
| 2026-06-23 09:49:29 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2026-06-23 09:54:49 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 272 seconds) |
| 2026-06-23 10:01:58 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 10:02:50 +0000 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-06-23 10:06:49 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2026-06-23 10:07:58 +0000 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Quit: xff0x) |
| 2026-06-23 10:18:40 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 10:23:14 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2026-06-23 10:24:11 +0000 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-06-23 10:34:56 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 10:36:43 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Ping timeout: 243 seconds) |
| 2026-06-23 10:40:10 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 256 seconds) |
| 2026-06-23 10:50:00 +0000 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2026-06-23 10:50:21 +0000 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) dtman34 |
| 2026-06-23 10:51:13 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 10:55:46 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 257 seconds) |
| 2026-06-23 11:02:04 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-23 11:02:26 +0000 | karenw_ | karenw |
| 2026-06-23 11:03:26 +0000 | haritz | (~hrtz@140.228.70.141) |
| 2026-06-23 11:03:26 +0000 | haritz | (~hrtz@140.228.70.141) (Changing host) |
| 2026-06-23 11:03:26 +0000 | haritz | (~hrtz@user/haritz) haritz |
| 2026-06-23 11:08:14 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 11:22:19 +0000 | fernando-basso | (~fernando-@2a01:4f9:c012:63d3::1) (Quit: WeeChat 3.8) |
| 2026-06-23 11:23:44 +0000 | xff0x | (~xff0x@2405:6580:b080:900:e63a:b024:3b2a:a5eb) |
| 2026-06-23 11:24:34 +0000 | rekahsoft | (~rekahsoft@70.51.99.119) rekahsoft |
| 2026-06-23 11:25:01 +0000 | schuelermine | (~Thunderbi@user/schuelermine) (Quit: schuelermine) |
| 2026-06-23 11:30:19 +0000 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2026-06-23 11:30:41 +0000 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 244 seconds) |
| 2026-06-23 11:31:23 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2026-06-23 11:33:11 +0000 | Lord_of_Life_ | Lord_of_Life |
| 2026-06-23 11:34:00 +0000 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2026-06-23 11:41:43 +0000 | traxex | (traxex@user/traxex) (Ping timeout: 264 seconds) |
| 2026-06-23 11:50:21 +0000 | czan | (~czan@user/mange) czan |
| 2026-06-23 11:50:46 +0000 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-06-23 11:51:06 +0000 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-06-23 11:52:06 +0000 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-06-23 11:55:35 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2026-06-23 11:55:45 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-06-23 12:05:58 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 12:07:05 +0000 | rabbull72 | (~rabbull@xdsl-31-164-93-219.adslplus.ch) (Quit: Ping timeout (120 seconds)) |
| 2026-06-23 12:07:15 +0000 | rabbull72 | (~rabbull@xdsl-31-164-93-219.adslplus.ch) |
| 2026-06-23 12:15:57 +0000 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2026-06-23 12:19:31 +0000 | DragonMaus | (~DragonMau@user/dragonmaus) (Ping timeout: 264 seconds) |
| 2026-06-23 12:24:07 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-06-23 12:29:26 +0000 | lisbeths | (uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2026-06-23 12:32:17 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) |
| 2026-06-23 12:37:31 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-06-23 12:44:52 +0000 | confusedalex | (~confuseda@user/confusedalex) (Remote host closed the connection) |
| 2026-06-23 12:45:47 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-06-23 12:53:31 +0000 | CiaoSen | (~Jura@2a02:3100:6065:ab00:4e50:ddff:fe9b:8922) CiaoSen |
| 2026-06-23 12:53:39 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-23 13:11:55 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) (Quit: KVIrc 5.2.8 Quasar http://www.kvirc.net/) |
| 2026-06-23 13:21:23 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-06-23 13:21:50 +0000 | mrvdb- | (~mrvdb@2001:19f0:5000:8582:5400:ff:fe07:3df5) (Quit: ZNC 1.10.1 - https://znc.in) |
| 2026-06-23 13:22:59 +0000 | mrvdb | (~mrvdb@2001:19f0:5000:8582:5400:ff:fe07:3df5) mrvdb |
| 2026-06-23 13:29:07 +0000 | confusedalex | (~confuseda@user/confusedalex) confusedalex |
| 2026-06-23 13:29:46 +0000 | czan | (~czan@user/mange) (Quit: Zzz...) |
| 2026-06-23 13:36:19 +0000 | karenw | (~karenw@user/karenw) (Ping timeout: 276 seconds) |
| 2026-06-23 13:39:13 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) Anarchos |
| 2026-06-23 13:40:30 +0000 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) (Ping timeout: 246 seconds) |
| 2026-06-23 13:46:59 +0000 | comonad | (~comonad@p200300d02734bf007432065c333bdb0c.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-06-23 13:48:10 +0000 | comonad | (~comonad@p200300d02734bf007432065c333bdb0c.dip0.t-ipconnect.de) |
| 2026-06-23 13:52:57 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-23 13:56:03 +0000 | traxex | (traxex@user/traxex) traxex |
| 2026-06-23 14:02:54 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) |
| 2026-06-23 14:06:07 +0000 | dtman34 | (~dtman34@c-73-242-68-179.hsd1.mn.comcast.net) dtman34 |
| 2026-06-23 14:11:38 +0000 | Anarchos | (~Anarchos@91-161-254-16.subs.proxad.net) (Quit: Vision[]: i've been blurred!) |
| 2026-06-23 14:13:39 +0000 | CiaoSen | (~Jura@2a02:3100:6065:ab00:4e50:ddff:fe9b:8922) (Ping timeout: 245 seconds) |
| 2026-06-23 14:16:50 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 248 seconds) |
| 2026-06-23 14:17:49 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-23 14:19:49 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2026-06-23 14:24:41 +0000 | karenw | (~karenw@user/karenw) karenw |
| 2026-06-23 14:26:21 +0000 | foul_owl | (~kerry@94.156.149.95) (Ping timeout: 246 seconds) |
| 2026-06-23 14:27:40 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Read error: Connection reset by peer) |
| 2026-06-23 14:27:58 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-23 14:28:56 +0000 | DragonMaus | (~DragonMau@user/dragonmaus) DragonMaus |
| 2026-06-23 14:32:35 +0000 | merijn | (~merijn@77.242.116.146) merijn |
| 2026-06-23 14:43:29 +0000 | Guest66 | (~Guest66@240f:6e:f6f0:1:c42e:e17d:4fe1:287b) |
| 2026-06-23 14:43:36 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-23 14:44:36 +0000 | Guest66 | (~Guest66@240f:6e:f6f0:1:c42e:e17d:4fe1:287b) (Client Quit) |
| 2026-06-23 14:48:18 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 252 seconds) |
| 2026-06-23 14:54:03 +0000 | AlexNoo_ | AlexNoo |
| 2026-06-23 14:58:36 +0000 | schuelermine | (~Thunderbi@user/schuelermine) schuelermine |
| 2026-06-23 14:59:06 +0000 | nyc | (~nyc@user/nyc) nyc |
| 2026-06-23 15:04:29 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 245 seconds) |
| 2026-06-23 15:04:46 +0000 | machinedgod | (~machinedg@d108-173-95-19.abhsia.telus.net) machinedgod |
| 2026-06-23 15:08:05 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-06-23 15:09:56 +0000 | <jaror> | gentauro: an alternative to length was added recently to base, let me look it up |
| 2026-06-23 15:10:48 +0000 | <int-e> | :t genericLength |
| 2026-06-23 15:10:49 +0000 | <lambdabot> | Num i => [a] -> i |
| 2026-06-23 15:11:20 +0000 | <jaror> | compareLength |
| 2026-06-23 15:11:27 +0000 | <jaror> | https://github.com/haskell/core-libraries-committee/issues/257 |
| 2026-06-23 15:11:52 +0000 | <schuelermine> | int-e: hasn't genericLength existed for ages |
| 2026-06-23 15:12:12 +0000 | <int-e> | schuelermine: time is relative ;) |
| 2026-06-23 15:12:24 +0000 | <schuelermine> | sure |
| 2026-06-23 15:12:38 +0000 | <schuelermine> | it feels like 10 years |
| 2026-06-23 15:12:56 +0000 | <schuelermine> | unfortunately there isn't a "since" in the docs |
| 2026-06-23 15:15:25 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) |
| 2026-06-23 15:16:18 +0000 | <schuelermine> | surprised I don’t have a GHC clone already |
| 2026-06-23 15:17:21 +0000 | <geekosaur> | someone would have to dig pretty far back, genericLength was already in 6.0.1 |
| 2026-06-23 15:17:29 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2026-06-23 15:20:14 +0000 | <int-e> | Yeah in a sense it's always been there: https://gitlab.haskell.org/ghc/ghc/-/blob/4fb94ae5e5d632748fa2e6c35e259eccc5a1a3f4/libraries/base/… |
| 2026-06-23 15:20:28 +0000 | <schuelermine> | im going through the git blame and I'm at a commit in 2001 rn |
| 2026-06-23 15:20:44 +0000 | <schuelermine> | oh you already got further |
| 2026-06-23 15:22:01 +0000 | <int-e> | https://www.haskell.org/definition/haskell98-bugs.html lists it as a December 2001 addition to the report |
| 2026-06-23 15:22:20 +0000 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2026-06-23 15:23:23 +0000 | califax | (~califax@user/califx) califx |
| 2026-06-23 15:28:39 +0000 | <schuelermine> | I think we can all agree that’s pretty recent |
| 2026-06-23 15:28:53 +0000 | <schuelermine> | practically yesterday |
| 2026-06-23 15:32:56 +0000 | <schuelermine> | jaror: I wonder if you could formulate a theoretical language with a sort of ultra-laziness where "length (repeat ()) >= 10" just doesn't diverge even with the current definitions of length and repeat and >= |
| 2026-06-23 15:33:41 +0000 | <schuelermine> | wait isn't that what would happen if you used an inductively defined Nat type |
| 2026-06-23 15:33:57 +0000 | <dutchie> | yeah i was about to say you just need data Nat = Z | S Nat |
| 2026-06-23 15:36:30 +0000 | <jaror> | https://youtu.be/jFk1qpr1ytk |
| 2026-06-23 15:36:59 +0000 | <Leary> | % genericLength @Nat (repeat ()) >= 10 |
| 2026-06-23 15:36:59 +0000 | <yahb2> | True |
| 2026-06-23 15:37:47 +0000 | <jaror> | One problem is that the language has no guardrails, so you have to think very hard all the time |
| 2026-06-23 15:41:09 +0000 | <jaror> | Not necessarily harder than making sure normal strict programs terminate, but that's bad too |
| 2026-06-23 15:44:04 +0000 | absence | (torgeihe@hildring.pvv.ntnu.no) (Ping timeout: 256 seconds) |
| 2026-06-23 15:45:28 +0000 | absence | (torgeihe@hildring.pvv.ntnu.no) |
| 2026-06-23 16:01:49 +0000 | danza | (~danza@user/danza) (Remote host closed the connection) |
| 2026-06-23 16:07:42 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-06-23 16:09:56 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-23 16:11:47 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Read error: Connection reset by peer) |
| 2026-06-23 16:12:12 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-23 16:16:48 +0000 | aka_dude | (~aka_dude@192.71.166.120) (Quit: Gateway shutdown) |
| 2026-06-23 16:17:39 +0000 | aka_dude | (~aka_dude@2a03:f80:30:f490::1) |
| 2026-06-23 16:18:26 +0000 | xintron | (~xintron@user/xintron) (Quit: Lurker 1.0.3 (the truth is out there) https://lurker.chat) |
| 2026-06-23 16:18:39 +0000 | xintron | (~xintron@user/xintron) xintron |
| 2026-06-23 16:20:21 +0000 | ystael | (~ystael@user/ystael) ystael |
| 2026-06-23 16:21:35 +0000 | jreicher | Guest9452 |
| 2026-06-23 16:21:35 +0000 | Guest9452 | (~joelr@user/jreicher) (Killed (niobium.libera.chat (Nickname regained by services))) |
| 2026-06-23 16:22:01 +0000 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-06-23 16:23:37 +0000 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2026-06-23 16:23:51 +0000 | karenw | (~karenw@user/karenw) (Quit: Deep into that darkness peering...) |
| 2026-06-23 16:51:00 +0000 | m | (~travltux@user/travltux) (Quit: WeeChat 4.7.2) |
| 2026-06-23 16:53:25 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 257 seconds) |
| 2026-06-23 16:53:35 +0000 | m2 | (~travltux@user/travltux) travltux |
| 2026-06-23 16:53:43 +0000 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2026-06-23 16:54:06 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-23 16:54:44 +0000 | califax | (~califax@user/califx) califx |
| 2026-06-23 16:56:48 +0000 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2026-06-23 16:57:49 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) (Read error: Connection reset by peer) |
| 2026-06-23 16:58:12 +0000 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-06-23 16:58:46 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 244 seconds) |
| 2026-06-23 17:02:49 +0000 | nyc | (~nyc@user/nyc) (Ping timeout: 245 seconds) |
| 2026-06-23 17:03:07 +0000 | nyc | (~nyc@user/nyc) nyc |
| 2026-06-23 17:05:58 +0000 | emilym | (~Thunderbi@user/emilym) emilym |
| 2026-06-23 17:07:45 +0000 | <monochrom> | (Belated) After being candid and s/productive/coinductive/, even s/productive/anamorphism/, you see why it is counterproductive to insist on "productive" --- catamorphisms are important too. |
| 2026-06-23 17:09:01 +0000 | <jaror> | inductive functions need to terminate, coinductive functions need to be productive |
| 2026-06-23 17:09:09 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2026-06-23 17:09:31 +0000 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2026-06-23 17:09:43 +0000 | <jaror> | Haskell doesn't make it easy to enforce that difference |
| 2026-06-23 17:10:49 +0000 | emilym | (~Thunderbi@user/emilym) (Ping timeout: 276 seconds) |
| 2026-06-23 17:15:16 +0000 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2026-06-23 17:16:16 +0000 | califax | (~califax@user/califx) califx |
| 2026-06-23 17:19:15 +0000 | acidsys | (~crameleon@openSUSE/member/crameleon) (Ping timeout: 246 seconds) |
| 2026-06-23 17:19:16 +0000 | Fijxu | (~Fijxu@user/fijxu) (Ping timeout: 276 seconds) |
| 2026-06-23 17:19:34 +0000 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2026-06-23 17:19:50 +0000 | califax | (~califax@user/califx) califx |
| 2026-06-23 17:21:13 +0000 | nyc | (~nyc@user/nyc) (Ping timeout: 276 seconds) |
| 2026-06-23 17:21:29 +0000 | nyc | (~nyc@user/nyc) nyc |
| 2026-06-23 17:28:05 +0000 | rabbull72 | (~rabbull@xdsl-31-164-93-219.adslplus.ch) (Read error: Connection reset by peer) |
| 2026-06-23 17:28:25 +0000 | rabbull72 | (~rabbull@xdsl-31-164-93-219.adslplus.ch) |
| 2026-06-23 17:32:50 +0000 | nyc | (~nyc@user/nyc) (Read error: Connection reset by peer) |
| 2026-06-23 17:33:10 +0000 | nyc | (~nyc@user/nyc) nyc |
| 2026-06-23 17:33:30 +0000 | ft | (~ft@p508db6b1.dip0.t-ipconnect.de) ft |
| 2026-06-23 17:35:27 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-23 17:39:40 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-06-23 17:40:43 +0000 | nyc | (~nyc@user/nyc) (Ping timeout: 276 seconds) |
| 2026-06-23 17:40:58 +0000 | nyc | (~nyc@user/nyc) nyc |
| 2026-06-23 17:42:13 +0000 | acidsys | (~crameleon@openSUSE/member/crameleon) crameleon |
| 2026-06-23 17:42:57 +0000 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2026-06-23 17:44:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 17:49:20 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 17:53:55 +0000 | nyc | (~nyc@user/nyc) (Read error: Connection reset by peer) |
| 2026-06-23 17:54:10 +0000 | nyc | (~nyc@user/nyc) nyc |
| 2026-06-23 18:00:26 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 18:03:07 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) |
| 2026-06-23 18:04:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 18:06:11 +0000 | olivial | (~benjaminl@user/benjaminl) (Read error: Connection reset by peer) |
| 2026-06-23 18:06:28 +0000 | olivial | (~benjaminl@user/benjaminl) benjaminl |
| 2026-06-23 18:07:46 +0000 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2026-06-23 18:13:37 +0000 | foul_owl | (~kerry@94.156.149.95) foul_owl |
| 2026-06-23 18:15:47 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 18:16:15 +0000 | <monochrom> | GHC2021 seems to have GADTs power even though it only has GADTSyntax. I tried "data Z a where Nil :: Z ()" and it's accepted. (Tried both 9.6 and 9.14.) Have you noticed it too? How did full GADTs sneaked in? |
| 2026-06-23 18:16:25 +0000 | schuelermine | (~Thunderbi@user/schuelermine) (Ping timeout: 272 seconds) |
| 2026-06-23 18:16:42 +0000 | <jaror> | Yeah, it's a known bug |
| 2026-06-23 18:16:52 +0000 | <monochrom> | OK thanks. |
| 2026-06-23 18:17:16 +0000 | <monochrom> | I don't mind the accidental bonus. Just nerding it out heh. |
| 2026-06-23 18:17:18 +0000 | <jaror> | the combination of GADTSyntax and ExistentialQuantification allows you to write any GADT |
| 2026-06-23 18:17:48 +0000 | <jaror> | Though it doesn't enable MonoLocalBinds, so you'll probably get warnings about that |
| 2026-06-23 18:20:10 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-23 18:21:21 +0000 | <EvanR> | ghc2021, you're too powerful |
| 2026-06-23 18:21:43 +0000 | <EvanR> | we recommend you step down and resign from office |
| 2026-06-23 18:23:43 +0000 | <jaror> | What about GHC2024 then? |
| 2026-06-23 18:25:00 +0000 | tromp | (~textual@2001:1c00:340e:2700:f85c:5d3d:452:a65a) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-06-23 18:28:50 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 265 seconds) |
| 2026-06-23 18:33:20 +0000 | dextaa | (~DV@user/dextaa) dextaa |
| 2026-06-23 18:36:15 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 18:36:15 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-23 18:37:13 +0000 | <geekosaur> | unless they removed one of those extensions it'll have it too |
| 2026-06-23 18:37:38 +0000 | <jaror> | It explicitly added GADTs and MonoLocalBinds |
| 2026-06-23 18:37:46 +0000 | <jaror> | For that reason |
| 2026-06-23 18:39:07 +0000 | <monochrom> | haha "It's a feature not a bug" |
| 2026-06-23 18:40:50 +0000 | <geekosaur> | that seems like a hack to me; if I didn't ask specifically for GADTs, I shouldn't getthem just because ExistentialQqantification was also enabled |
| 2026-06-23 18:41:06 +0000 | <geekosaur> | well, a mask, not really a hack |
| 2026-06-23 18:41:10 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2026-06-23 18:42:16 +0000 | <monochrom> | I can understand if it is too difficult to fix. The inference algorithm is already a mess... |
| 2026-06-23 18:43:11 +0000 | <jaror> | also, do we want yet another breaking change to fix this minor thing? |
| 2026-06-23 18:43:51 +0000 | <jaror> | Are there really that many people who want ExistentialQuantification but no GADTs? |
| 2026-06-23 18:45:45 +0000 | <geekosaur> | there are certainly people who turn on GADTSyntax just because they prefer that syntax for all declarations; I could see them being surprised if some of those became existentials without warning |
| 2026-06-23 18:46:41 +0000 | <jaror> | That won't happen unless you enable ExistentialQuantification |
| 2026-06-23 18:47:10 +0000 | <jaror> | The thing is that if you do that, you can also define data types that are not just existentially quantified |
| 2026-06-23 18:47:23 +0000 | <jaror> | Like monochrom's example above |
| 2026-06-23 18:49:15 +0000 | <monochrom> | I think MonoLocalBinds is more divisive one. |
| 2026-06-23 18:49:18 +0000 | <Leary> | You can already write any GADT with ExistentialQuantification alone; GADTSyntax is just, well, better syntax. |
| 2026-06-23 18:51:12 +0000 | <monochrom> | Wait, how do I write "data Z a where Nil :: Z()" with ExistentialQuantification? |
| 2026-06-23 18:51:19 +0000 | <geekosaur> | right, but I can stillimagine people being surprised by it |
| 2026-06-23 18:51:22 +0000 | <Leary> | `data Z a = a ~ () => Nil` |
| 2026-06-23 18:51:32 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 18:51:39 +0000 | <monochrom> | yikes haha |
| 2026-06-23 18:58:26 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-06-23 19:01:31 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 264 seconds) |
| 2026-06-23 19:09:38 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-23 19:11:18 +0000 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2026-06-23 19:13:30 +0000 | itaipu | (~itaipu@168.121.98.63) (Ping timeout: 245 seconds) |
| 2026-06-23 19:14:05 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 258 seconds) |
| 2026-06-23 19:16:41 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-06-23 19:19:07 +0000 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-06-23 19:22:02 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 19:26:23 +0000 | itaipu | (~itaipu@168.121.99.135) itaipu |
| 2026-06-23 19:26:36 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-23 19:29:24 +0000 | itaipu | (~itaipu@168.121.99.135) (Read error: Connection reset by peer) |
| 2026-06-23 19:31:20 +0000 | Googulator | (~Googulato@212-40-94-63.pool.digikabel.hu) (Quit: Client closed) |
| 2026-06-23 19:31:35 +0000 | Googulator | (~Googulato@212-40-94-63.pool.digikabel.hu) |
| 2026-06-23 19:32:51 +0000 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-06-23 19:34:48 +0000 | koraynilay | (~koraynila@user/koraynilay) (Ping timeout: 244 seconds) |
| 2026-06-23 19:34:57 +0000 | exarkun_ | (~exarkun@user/exarkun) exarkun |
| 2026-06-23 19:35:19 +0000 | jonnie | (~jonnie@user/jonnie) (Ping timeout: 244 seconds) |
| 2026-06-23 19:35:43 +0000 | jonnie | (~jonnie@user/jonnie) jonnie |
| 2026-06-23 19:35:52 +0000 | dextaa | (~DV@user/dextaa) (Quit: Leaving) |
| 2026-06-23 19:35:58 +0000 | exarkun | (~exarkun@user/exarkun) (Ping timeout: 268 seconds) |
| 2026-06-23 19:37:02 +0000 | koraynilay | (~koraynila@user/koraynilay) koraynilay |
| 2026-06-23 19:37:03 +0000 | dextaa | (~DV@user/dextaa) dextaa |
| 2026-06-23 19:37:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 19:41:50 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 19:44:49 +0000 | karenw | (~karenw@user/karenw) karenw |
| 2026-06-23 19:46:31 +0000 | itaipu | (~itaipu@168.121.99.135) itaipu |
| 2026-06-23 19:51:00 +0000 | acidjnk | (~acidjnk@p200300d6e700e585726eb65abab086aa.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2026-06-23 19:51:29 +0000 | acidjnk_new | (~acidjnk@p200300d6e700e585726eb65abab086aa.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2026-06-23 19:52:46 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 19:55:33 +0000 | acidjnk | (~acidjnk@p200300d6e70242376685ebb53532e457.dip0.t-ipconnect.de) acidjnk |
| 2026-06-23 19:55:35 +0000 | acidjnk_new | (~acidjnk@p200300d6e70242376685ebb53532e457.dip0.t-ipconnect.de) acidjnk |
| 2026-06-23 19:57:22 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-06-23 20:07:20 +0000 | <gentauro> | jaror: and int-e `genericLength`? |
| 2026-06-23 20:07:51 +0000 | <jaror> | what's the question? |
| 2026-06-23 20:08:07 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 20:09:12 +0000 | <gentauro> | jaror: gives the same warning (LSP + IED) -> ` ✲ Name: Infinite: ghc-internal/genericLength` |
| 2026-06-23 20:09:19 +0000 | <int-e> | gentauro: it's an equivalent to length ;) |
| 2026-06-23 20:09:19 +0000 | <gentauro> | we are in the same boat :) |
| 2026-06-23 20:09:36 +0000 | <jaror> | Yeah, I suggested Data.List.compareLength, not genericLength |
| 2026-06-23 20:09:47 +0000 | <gentauro> | jaror: ahhh |
| 2026-06-23 20:10:52 +0000 | <gentauro> | > :t compareLength |
| 2026-06-23 20:10:53 +0000 | <lambdabot> | <hint>:1:1: error: parse error on input `:' |
| 2026-06-23 20:10:58 +0000 | <gentauro> | % :t compareLength |
| 2026-06-23 20:10:58 +0000 | <yahb2> | <interactive>:1:1: error: [GHC-88464] ; Variable not in scope: compareLength |
| 2026-06-23 20:11:05 +0000 | <int-e> | gentauro: whereas I did the thing where I didn't read context |
| 2026-06-23 20:11:10 +0000 | <gentauro> | % :t Data.ListcompareLength |
| 2026-06-23 20:11:10 +0000 | <yahb2> | <interactive>:1:1: error: [GHC-76037] ; • Not in scope: data constructor ‘Data.ListcompareLength’ ; • Note: No module named ‘Data’ is imported. |
| 2026-06-23 20:11:14 +0000 | <gentauro> | % :t Data.List.compareLength |
| 2026-06-23 20:11:14 +0000 | <yahb2> | Data.List.compareLength :: [a] -> Int -> Ordering |
| 2026-06-23 20:11:52 +0000 | <gentauro> | int-e: fair enough :) |
| 2026-06-23 20:12:47 +0000 | <gentauro> | jaror: but to use `compareLength` you need to have some static value and you get an order (LT,EQ,GT). I want a number xD |
| 2026-06-23 20:12:48 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-23 20:13:06 +0000 | <gentauro> | I guess I just have to live with the warnings. |
| 2026-06-23 20:14:02 +0000 | <jaror> | If you know your lists are finite, can't you use another type like an array or Seq? |
| 2026-06-23 20:14:30 +0000 | <jaror> | They also have much faster length fuctions |
| 2026-06-23 20:16:03 +0000 | <int-e> | > let s = iterate (\x -> x <> x) (Seq.singleton ()) !! 63 in Seq.length s |
| 2026-06-23 20:16:05 +0000 | <lambdabot> | -9223372036854775808 |
| 2026-06-23 20:17:03 +0000 | <jaror> | very fast |
| 2026-06-23 20:22:44 +0000 | <gentauro> | jaror: I think I could. But for my usage, standard list should do the job (and yes, I know they aren't inf) |
| 2026-06-23 20:23:02 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 20:26:10 +0000 | <jaror> | Arrays and Seq are also pretty standard. I think they should be used more. |
| 2026-06-23 20:27:55 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-23 20:30:34 +0000 | <jaror> | (Not actually the Array type from the array package) |
| 2026-06-23 20:33:20 +0000 | tromp | (~textual@2001:1c00:340e:2700:e1be:7d8f:de85:da97) |
| 2026-06-23 20:38:35 +0000 | merijn | (~merijn@62.45.136.136) merijn |
| 2026-06-23 20:38:43 +0000 | <c_wraith> | Seq is... Seq is not great. Like it's fine as a quick proof of concept. But nearly every use people have for it can be done better by something more focused |
| 2026-06-23 20:39:15 +0000 | <jaror> | It's better than lists for most things |
| 2026-06-23 20:39:45 +0000 | <c_wraith> | I guess that's true for the universe of possible things |
| 2026-06-23 20:39:54 +0000 | <c_wraith> | But it's significantly worse than list for iterating in order |
| 2026-06-23 20:40:00 +0000 | <c_wraith> | Which is the main thing lists are used for |
| 2026-06-23 20:43:03 +0000 | merijn | (~merijn@62.45.136.136) (Ping timeout: 252 seconds) |
| 2026-06-23 20:44:17 +0000 | <monochrom> | IMO you should just tell your LSP+IED to shut up. Those warnings are getting silly. |
| 2026-06-23 20:44:50 +0000 | <monochrom> | Or even better, don't use it, use a plain editor. |
| 2026-06-23 20:44:57 +0000 | <jaror> | those warnings are from Stan by the way which you should be able to disable separately |
| 2026-06-23 20:45:12 +0000 | <jaror> | and I think recent versions of HLS don't enable it by default |
| 2026-06-23 20:45:20 +0000 | <jaror> | at least in vscodium |
| 2026-06-23 20:45:27 +0000 | <monochrom> | Like, GHC -Wall already gives you more than enough silly warnings, you don't need another warner. |
| 2026-06-23 20:45:44 +0000 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-06-23 20:46:47 +0000 | <monochrom> | Those who care so much about totality can please switch over to Lean and leave Haskell alone. I chose Haskell because I want its compromises, not because I have totality OCD. |
| 2026-06-23 20:47:27 +0000 | <monochrom> | I only have a mild case of static typing OCD. |
| 2026-06-23 20:48:02 +0000 | <geekosaur> | yeh, HLS disabled Stan by default a couple versions ago IIRC |
| 2026-06-23 20:50:09 +0000 | <jaror> | c_wraith, so a better alternative would be a list of arrays that double in length? Maybe someone should write a library for that. |
| 2026-06-23 20:51:07 +0000 | <jaror> | That way you still have O(1) access to the first element and fast iteration, but you also have fast length and fast indexing |
| 2026-06-23 20:51:31 +0000 | <jaror> | (amortized) |
| 2026-06-23 20:52:16 +0000 | <jaror> | Is there any way that is worse than finite lists? |
| 2026-06-23 20:52:28 +0000 | acidjnk_new | (~acidjnk@p200300d6e70242376685ebb53532e457.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2026-06-23 20:52:28 +0000 | acidjnk | (~acidjnk@p200300d6e70242376685ebb53532e457.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2026-06-23 20:52:36 +0000 | <monochrom> | Inserting something in the middle also something Seq does well. |
| 2026-06-23 20:52:43 +0000 | <EvanR> | totalness is a useful idea to apply to your haskell code mentally (when appropriate) just like pure function is useful to apply in C (when appropriate) despite not having real support |
| 2026-06-23 20:53:20 +0000 | <jaror> | I'd like to keep things out of my head and in my source code. |
| 2026-06-23 20:53:58 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 20:54:09 +0000 | <EvanR> | we need inline simply typed lambda calculus like C has inline asm xD |
| 2026-06-23 20:54:43 +0000 | <monochrom> | I have static typing OCD but it doesn't mean I should go to the Python community and "contribute" a linter that says "Warning: Python is not statically typed" for every line of code. |
| 2026-06-23 20:54:52 +0000 | <EvanR> | instead of "C is too slow, switching to asm" it's "guarantees not strong enough switching to STLC" |
| 2026-06-23 20:55:23 +0000 | <int-e> | c_wraith: I used something Seq-like for https://research.ibm.com/blog/ponder-this-november-2025 (but the 64 bit restriction meant that I couldn't use Data.Seq itself) |
| 2026-06-23 20:55:36 +0000 | <monochrom> | I think with GHC you should go for inline System F-omega or something... |
| 2026-06-23 20:55:56 +0000 | <EvanR> | pick your poison |
| 2026-06-23 20:56:03 +0000 | acidjnk | (~acidjnk@p54ad50b4.dip0.t-ipconnect.de) acidjnk |
| 2026-06-23 20:56:05 +0000 | acidjnk_new | (~acidjnk@p200300d6e74def43ec2141b26299b177.dip0.t-ipconnect.de) |
| 2026-06-23 20:56:15 +0000 | <int-e> | (I simplified ; I didn't use a finger tree; in fact I didn't even balance the trees) |
| 2026-06-23 20:56:36 +0000 | <monochrom> | Oh ah I see what you mean now! :) |
| 2026-06-23 20:56:37 +0000 | <int-e> | (so basically, only the sharing and measuring ideas survived) |
| 2026-06-23 20:57:05 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) Inline |
| 2026-06-23 20:58:31 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-23 20:59:02 +0000 | <EvanR> | we have a pragma which makes everything in a module strict, I wonder if "everything in this module GHC must be convinced of total or it shall not pass" |
| 2026-06-23 20:59:16 +0000 | <EvanR> | the strict one seems even more non haskelly |
| 2026-06-23 20:59:56 +0000 | <jaror> | The Mu compiler has a "Recursion" language extension which is disable by default |
| 2026-06-23 21:02:35 +0000 | <geekosaur> | can't do very much when something must be provably total |
| 2026-06-23 21:02:54 +0000 | leppard | (~noOne@ipservice-092-209-218-237.092.209.pools.vodafone-ip.de) (Quit: KVIrc 5.2.8 Quasar http://www.kvirc.net/) |
| 2026-06-23 21:03:00 +0000 | <jaror> | You can do a lot in Agda |
| 2026-06-23 21:04:12 +0000 | <monochrom> | Someone would have to write a "simple" totality checker for GHC before you could have that pragma. |
| 2026-06-23 21:04:28 +0000 | <jaror> | No, it's easy to disallow recursion |
| 2026-06-23 21:04:41 +0000 | <jaror> | Just don't put the function in its own scope |
| 2026-06-23 21:05:03 +0000 | <monochrom> | :( |
| 2026-06-23 21:05:33 +0000 | <monochrom> | Well, I guess it won't happen anyway, so I don't need to argue against it. |
| 2026-06-23 21:06:29 +0000 | <jaror> | Some (at least on) of their employees was considering opening a GHC proposal |
| 2026-06-23 21:09:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 21:10:40 +0000 | user363627 | (~user@user/user363627) user363627 |
| 2026-06-23 21:13:39 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 21:14:31 +0000 | weary-traveler | (~user@user/user363627) (Ping timeout: 244 seconds) |
| 2026-06-23 21:20:49 +0000 | <EvanR> | ghc already does coverage analysis for case |
| 2026-06-23 21:21:11 +0000 | <EvanR> | if there's no recursion below that, it seems like there's not much else to check |
| 2026-06-23 21:21:22 +0000 | <EvanR> | no unsafePerformIO, etc |
| 2026-06-23 21:21:45 +0000 | <EvanR> | (and no recursive data types) |
| 2026-06-23 21:22:10 +0000 | <jaror> | and no Type :: Type |
| 2026-06-23 21:22:56 +0000 | <monochrom> | I was hoping to allow structure recursion. |
| 2026-06-23 21:23:05 +0000 | <monochrom> | err, structural recursion |
| 2026-06-23 21:24:07 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 21:24:51 +0000 | <jaror> | that should be fine to allow and not that hard to check |
| 2026-06-23 21:30:35 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 21:36:30 +0000 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2026-06-23 21:41:59 +0000 | <mauke> | does "recursive data types" include list? |
| 2026-06-23 21:42:07 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 21:44:14 +0000 | Fijxu | (~Fijxu@user/fijxu) fijxu |
| 2026-06-23 21:46:37 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 253 seconds) |
| 2026-06-23 21:51:12 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 21:53:11 +0000 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
| 2026-06-23 21:55:28 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2026-06-23 22:03:29 +0000 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2026-06-23 22:03:46 +0000 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2026-06-23 22:04:59 +0000 | <monochrom> | See? What takes forever (pun!) will not be implementing it, but rather getting the community to reach a consensus on how much to allow. |
| 2026-06-23 22:06:34 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 22:07:02 +0000 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-06-23 22:11:07 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-06-23 22:12:54 +0000 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2026-06-23 22:21:12 +0000 | <jreicher> | I really don't understand the current totality craze. I keep hearing people talk about it in lots of different places, but there never seems to be a reason other than it's being talked about. |
| 2026-06-23 22:21:35 +0000 | karenw | (~karenw@user/karenw) (Quit: Deep into that darkness peering...) |
| 2026-06-23 22:21:57 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 22:26:27 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-06-23 22:30:55 +0000 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 245 seconds) |
| 2026-06-23 22:34:00 +0000 | nyc | (~nyc@user/nyc) (Remote host closed the connection) |
| 2026-06-23 22:37:19 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 22:41:34 +0000 | jaror | (~jaror@user/jaror) (Quit: The Lounge - https://thelounge.chat) |
| 2026-06-23 22:42:06 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-06-23 22:42:12 +0000 | jaror | (~jaror@user/jaror) jaror |
| 2026-06-23 22:42:53 +0000 | <geekosaur> | on the one hand I see your point, on the other it kinda feels like how others react to strong typing? |
| 2026-06-23 22:52:42 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 22:55:29 +0000 | <jreicher> | I think gratuitous type checking is definitely a thing. But type checking has been around long enough that using it pointlessly is relatively rare. People usually have an intention. |
| 2026-06-23 22:56:58 +0000 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 273 seconds) |
| 2026-06-23 22:56:59 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-06-23 22:57:46 +0000 | <EvanR> | mauke, yep |
| 2026-06-23 22:58:07 +0000 | <EvanR> | I was going for "bottom of the barrel" low hanging fruit |
| 2026-06-23 23:00:58 +0000 | <EvanR> | jreicher, "totalness" as a brand might seem annoying and hype infused. But imagine a different equivalent presentation: a function that at the very least gives some answer for any relevant input (since we regularly document this function is not to be used on certain things in lieu of some overcomplicated subtyping system, e.g. square root) |
| 2026-06-23 23:01:10 +0000 | <EvanR> | *it just makes sense* |
| 2026-06-23 23:01:34 +0000 | <EvanR> | and when it's not satisfied we tend not to blame simply this lack of totalness |
| 2026-06-23 23:02:20 +0000 | <jreicher> | Making sense is insufficient. It needs to be useful. I could give you a function that returns "chicken" regardless of input. We can even make it variadic! It "makes sense", right? |
| 2026-06-23 23:02:23 +0000 | <EvanR> | instead it's usually oh it was a bug |
| 2026-06-23 23:02:47 +0000 | <EvanR> | jreicher, yeah it's really easy to satisfy. Assuming the target domain is not Void |
| 2026-06-23 23:03:08 +0000 | <jreicher> | I want to understand the contexts in which a function being total is useful. |
| 2026-06-23 23:03:15 +0000 | <EvanR> | similar to putting undefined in your haskell code to make it compile |
| 2026-06-23 23:03:20 +0000 | <jreicher> | I'm not saying there aren't any, but I find that's usually left out of the conversation. |
| 2026-06-23 23:03:47 +0000 | <EvanR> | to me it sounds like an odd reversal to ask for when it's useful |
| 2026-06-23 23:03:55 +0000 | <EvanR> | like when is a function being pure useful |
| 2026-06-23 23:04:23 +0000 | <EvanR> | answers to like when is impure useful sound more interesting |
| 2026-06-23 23:04:41 +0000 | <jreicher> | Let me put it a different way. We want a function to have the property P, and because we want this it's useful to have a (type) checker verify it has that property. But it all starts with why we want that property in the first place. |
| 2026-06-23 23:04:49 +0000 | <EvanR> | total is basically an ubiquitous default |
| 2026-06-23 23:05:06 +0000 | <jreicher> | What is the origin of the requirement for a function to be total? |
| 2026-06-23 23:05:13 +0000 | <EvanR> | when is a program that successfully compiles useful |
| 2026-06-23 23:05:54 +0000 | <jreicher> | I just explained it. The compiler can verify the program has the properties we want it to have, and then of course it generates an object that can be executed on the target. |
| 2026-06-23 23:06:07 +0000 | <jreicher> | But it all starts with what we want of that program. |
| 2026-06-23 23:06:31 +0000 | <EvanR> | it's a basic sanity check on most normal code |
| 2026-06-23 23:06:48 +0000 | <jreicher> | Explain why "total" is a necessary condition for "sane" |
| 2026-06-23 23:06:53 +0000 | <EvanR> | if it's broken on some inputs, then you then have to mentally make sure that you don't call it on those inputs. Probably need an invisible proof |
| 2026-06-23 23:07:06 +0000 | <jreicher> | The definition of "broken" is "not what we want" |
| 2026-06-23 23:07:08 +0000 | <EvanR> | which dynamic language programmers do all the time and they think it's normal |
| 2026-06-23 23:07:15 +0000 | <jreicher> | You still need to elaborate on the "want" here. You can't just assume it |
| 2026-06-23 23:07:18 +0000 | <EvanR> | broken means, crashes or freezes up in this case |
| 2026-06-23 23:07:31 +0000 | <jreicher> | That's BECAUSE we DON'T WANT it to crash or freeze |
| 2026-06-23 23:07:40 +0000 | <jreicher> | Those are obvious, so you don't need to explain them. Other wants are not obvious |
| 2026-06-23 23:07:53 +0000 | <EvanR> | if you intentionally want the code to crash (or even freeze up) that's a special form of coding that isn't the usual |
| 2026-06-23 23:08:04 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 23:08:24 +0000 | <EvanR> | crashing and freezing up is part of the definition of total so I'm not sure what you're getting at |
| 2026-06-23 23:09:10 +0000 | <jreicher> | "Total" means "always halts", no? Why is that desirable? |
| 2026-06-23 23:09:35 +0000 | <EvanR> | (stuff like square root is total *on its intended domain* but not on the compiler understood larger domain is part of why checking for this is tricky) |
| 2026-06-23 23:09:57 +0000 | <jreicher> | I'm not interested in the mechanics of the checking until I know why this is worth checking for in the first place. |
| 2026-06-23 23:09:59 +0000 | <EvanR> | halt is an implementation detail |
| 2026-06-23 23:10:10 +0000 | <jreicher> | I'm only after a definition of "total". |
| 2026-06-23 23:10:11 +0000 | <EvanR> | total functions are defined at each input, has a value |
| 2026-06-23 23:10:21 +0000 | <EvanR> | in haskell that could be an infinite value |
| 2026-06-23 23:10:24 +0000 | <jreicher> | OK. Why is that desirable? |
| 2026-06-23 23:10:26 +0000 | <EvanR> | but not bottom |
| 2026-06-23 23:10:44 +0000 | apache | (apache2@anubis.0x90.dk) (Remote host closed the connection) |
| 2026-06-23 23:10:55 +0000 | apache2 | (apache2@anubis.0x90.dk) apache2 |
| 2026-06-23 23:11:13 +0000 | <EvanR> | I have a function in C right now, like most functions, is supposed to be total |
| 2026-06-23 23:11:27 +0000 | <EvanR> | but when you pass in a certain polygon to it, it crashes badly |
| 2026-06-23 23:11:28 +0000 | <jreicher> | Why is it "supposed" to be total? Where is this "supposed" come from? God? |
| 2026-06-23 23:11:43 +0000 | <EvanR> | if the compiler "merely" told me it wasn't total, I would have saved myself a lot of work |
| 2026-06-23 23:11:48 +0000 | pounce | (8a023a9e4a@user/cute/pounce) (Ping timeout: 244 seconds) |
| 2026-06-23 23:11:48 +0000 | <jreicher> | What is "wrong" with a partial function? |
| 2026-06-23 23:11:56 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Ping timeout: 245 seconds) |
| 2026-06-23 23:12:04 +0000 | <jreicher> | Why did you want it to be total in the first place? |
| 2026-06-23 23:12:07 +0000 | <EvanR> | I'm telling you it's supposed to be total |
| 2026-06-23 23:12:12 +0000 | <jreicher> | Why? |
| 2026-06-23 23:12:21 +0000 | <jreicher> | I'm not saying you're wrong, I just want to understand why |
| 2026-06-23 23:12:24 +0000 | <EvanR> | for any shape you give it, it gaves some answer (also a specific answer, but that's another story) |
| 2026-06-23 23:12:31 +0000 | <jreicher> | Why? |
| 2026-06-23 23:12:38 +0000 | pounce | (8a023a9e4a@user/cute/pounce) pounce |
| 2026-06-23 23:12:40 +0000 | <jreicher> | Why is this the definition/requirement of that function? |
| 2026-06-23 23:12:50 +0000 | Digit | (~user@user/digit) (Ping timeout: 244 seconds) |
| 2026-06-23 23:13:00 +0000 | <EvanR> | it's a side effect of the requirements |
| 2026-06-23 23:13:16 +0000 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2026-06-23 23:13:36 +0000 | Digitteknohippie | (~user@user/digit) Digit |
| 2026-06-23 23:13:37 +0000 | <jreicher> | Now we're talking. So in the absence of being able to check the "more complete" properties of the function, you check totality. |
| 2026-06-23 23:13:51 +0000 | <EvanR> | compiler checking the actual requirements would be even harder |
| 2026-06-23 23:13:57 +0000 | <jreicher> | Exactly |
| 2026-06-23 23:14:04 +0000 | <jreicher> | So we aren't interested in totality for its own sake. |
| 2026-06-23 23:14:11 +0000 | <EvanR> | but I would find it useful to do the "easier" (hard) thing |
| 2026-06-23 23:14:21 +0000 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-06-23 23:14:38 +0000 | <jreicher> | You want to know your function is correct. The fact that correctness implies totality is somewhat incidental, and won't be the case for other functions. |
| 2026-06-23 23:14:49 +0000 | <EvanR> | of course not. In fact there are use cases for functions that mess up, like when doing LUB racing between threads |
| 2026-06-23 23:15:06 +0000 | <jreicher> | Cool. We're on the same page. I can see where you're coming from. |
| 2026-06-23 23:15:12 +0000 | <EvanR> | but if you're in a module where you know all the functions are total then that's a thing you can test |
| 2026-06-23 23:15:21 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-06-23 23:15:31 +0000 | xff0x | (~xff0x@2405:6580:b080:900:e63a:b024:3b2a:a5eb) (Quit: xff0x) |
| 2026-06-23 23:16:06 +0000 | <EvanR> | in game engines you sometimes have 1 special function that implements an infinite loop, it's not total, and isn't even a pure function so you wouldn't test for that |
| 2026-06-23 23:16:22 +0000 | <dolio> | Why isn't it total? |
| 2026-06-23 23:16:37 +0000 | xff0x | (~xff0x@2405:6580:b080:900:9353:b8c8:c41e:444d) |
| 2026-06-23 23:17:13 +0000 | <EvanR> | in my premise, it's not even a function in the math sense but a procedure |
| 2026-06-23 23:17:34 +0000 | <EvanR> | but if it was () -> IO () then sure |
| 2026-06-23 23:17:49 +0000 | <dolio> | I think the real issue with demanding totality is usually that a lot of things that are total aren't easy to show total, especially for corecursion. |
| 2026-06-23 23:17:59 +0000 | <EvanR> | yes |
| 2026-06-23 23:18:22 +0000 | <EvanR> | many algorithms are total but the compiler can't just look at it and verify |
| 2026-06-23 23:18:28 +0000 | <dolio> | Lots of Haskell tricks are fine, but not allowed in any straight forward way. |
| 2026-06-23 23:19:17 +0000 | <EvanR> | but it's surprising how much easier it is to mentally verify when you move from e.g. explicit for loops to foreach over a (finite) array |
| 2026-06-23 23:19:41 +0000 | <EvanR> | or map over finite structure |
| 2026-06-23 23:20:06 +0000 | Digitteknohippie | Digit |
| 2026-06-23 23:20:48 +0000 | <EvanR> | also I think the whole total thing really came out of theorem proving where proofs take the form of definitely terminating computations |
| 2026-06-23 23:20:55 +0000 | <EvanR> | so a vast subset of general programming |
| 2026-06-23 23:21:28 +0000 | <EvanR> | so you might ask why do we want proofs to terminate and confuse some people |
| 2026-06-23 23:23:31 +0000 | <jreicher> | A theorem prover is a very particular kind of program with very particular requirements. That explains the "want" in THAT case. |
| 2026-06-23 23:23:50 +0000 | <jreicher> | I would venture to say most programmers aren't writing theorem provers. |
| 2026-06-23 23:24:01 +0000 | <dolio> | Proofs don't need to 'terminate.' |
| 2026-06-23 23:24:23 +0000 | <dolio> | A proof that a Turing machine diverges is an infinite sequence of steps. |
| 2026-06-23 23:24:26 +0000 | <EvanR> | if proofs = programs, then freezing up programs can prove anything |
| 2026-06-23 23:24:42 +0000 | <EvanR> | making it logically pointless |
| 2026-06-23 23:26:06 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-06-23 23:26:54 +0000 | <EvanR> | there would be no way to run that proof and observe the fact that it's infinite |
| 2026-06-23 23:27:05 +0000 | <EvanR> | is another issue |
| 2026-06-23 23:27:07 +0000 | <dolio> | Well, it's infinite by construction. |
| 2026-06-23 23:27:18 +0000 | <EvanR> | if you have a meta proof of that, then great |
| 2026-06-23 23:27:22 +0000 | <jreicher> | dolio: I don't think what you've said makes sense. How do you know the Turing machine is going to have an infinite sequence of steps unless you can demonstrate that with a FINITE set of SENTENCES? |
| 2026-06-23 23:27:27 +0000 | <dolio> | Like `data Stream a = Cons a (Stream a)` |
| 2026-06-23 23:28:28 +0000 | <dolio> | Yeah, it's an infinite stream described in a finite way. |
| 2026-06-23 23:28:30 +0000 | <EvanR> | yeah you'd need a valid program which constructs the turing machine's stream, without failing to pick a next move |
| 2026-06-23 23:28:41 +0000 | <dolio> | Everything you write on a page is described finitely. |
| 2026-06-23 23:28:52 +0000 | <EvanR> | this program would need to be verfified |
| 2026-06-23 23:29:04 +0000 | <jreicher> | dolio: exactly. And that's the proof. |
| 2026-06-23 23:29:12 +0000 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 246 seconds) |
| 2026-06-23 23:29:20 +0000 | <jreicher> | So a theorem prover will always terminate if a proof exists. |
| 2026-06-23 23:29:40 +0000 | <EvanR> | if you carefully walk the space of sentences |
| 2026-06-23 23:29:54 +0000 | <jreicher> | "Good" theorem prover. :p |
| 2026-06-23 23:30:24 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-06-23 23:30:27 +0000 | <dolio> | All Haskell programs are finite, including the ones that don't finish. |
| 2026-06-23 23:30:59 +0000 | <dolio> | The ones that don't finish in pathological ways, too. |
| 2026-06-23 23:31:02 +0000 | <jreicher> | How does that relate to what we're talking about? |
| 2026-06-23 23:32:18 +0000 | <EvanR> | yeah the proof would be the program in this case, not the semantics value (the infinite stream) |
| 2026-06-23 23:33:26 +0000 | <EvanR> | each WHNF step terminates |
| 2026-06-23 23:33:51 +0000 | <EvanR> | presumably, for this case |
| 2026-06-23 23:33:52 +0000 | czan | (~czan@user/mange) czan |
| 2026-06-23 23:35:01 +0000 | <dolio> | The connection is that proofs are analogous to Haskell programs, but saying that the text of a Haskell program is finite doesn't really tell you whether it stops or not, and some Haskell programs are not 'supposed' to stop, depending on what you mean by that. |
| 2026-06-23 23:35:35 +0000 | <jreicher> | dolio: the analogy is not straightforward. You still have to be clear what is being proven by the program you are taking as a proof |
| 2026-06-23 23:35:58 +0000 | <dolio> | The type is what is being proved. |
| 2026-06-23 23:36:23 +0000 | <jreicher> | And how does that relate to termination? |
| 2026-06-23 23:36:37 +0000 | <EvanR> | base haskell being not particularly expressive as a logic, you basically proved some stream exists |
| 2026-06-23 23:37:04 +0000 | <EvanR> | something on top of that would need to identify that you're talking about a turing machine |
| 2026-06-23 23:37:16 +0000 | <dolio> | Non-termination allows vacuous proofs of false things, usually. |
| 2026-06-23 23:38:32 +0000 | <dolio> | Not really non-termination, I guess, depending on what you mean. |
| 2026-06-23 23:38:39 +0000 | <dolio> | That was my point. |
| 2026-06-23 23:38:54 +0000 | <EvanR> | a term which can be used at any type |
| 2026-06-23 23:40:38 +0000 | <dolio> | Like, 'non-termination' is fine if your witness of the infinitude of primes is a stream of distinct prime numbers, as long as there's no point in the stream where it goes, "hold on a second," and then never comes back. |
| 2026-06-23 23:41:07 +0000 | <dolio> | That is the 'productive' part of totality. |