| 2025-05-04 00:00:15 +0200 | tromp | (~textual@2001:1c00:3487:1b00:31c9:5f27:18bf:4d4e) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 00:04:06 +0200 | P1RATEZ | (piratez@user/p1ratez) (Quit: Going offline, see ya! (www.adiirc.com)) |
| 2025-05-04 00:09:27 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 00:15:09 +0200 | amadaluzia | (~amadaluzi@user/amadaluzia) (Ping timeout: 252 seconds) |
| 2025-05-04 00:16:12 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-04 00:22:19 +0200 | Buliarous | (~gypsydang@46.232.210.139) (Remote host closed the connection) |
| 2025-05-04 00:22:48 +0200 | Buliarous | (~gypsydang@46.232.210.139) Buliarous |
| 2025-05-04 00:23:52 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 00:32:36 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-05-04 00:56:36 +0200 | nacation | (~m-3l4s76@user/nacation) (Ping timeout: 252 seconds) |
| 2025-05-04 00:57:45 +0200 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-05-04 01:00:43 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 01:00:51 +0200 | nacation | (~m-3l4s76@user/nacation) nacation |
| 2025-05-04 01:08:53 +0200 | preflex_ | (~preflex@user/mauke/bot/preflex) preflex |
| 2025-05-04 01:10:37 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 01:12:29 +0200 | preflex | (~preflex@user/mauke/bot/preflex) (Ping timeout: 245 seconds) |
| 2025-05-04 01:12:47 +0200 | preflex_ | preflex |
| 2025-05-04 01:14:40 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-05-04 01:14:41 +0200 | ljdarj1 | ljdarj |
| 2025-05-04 01:15:34 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) chiselfuse |
| 2025-05-04 01:15:43 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2025-05-04 01:33:43 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-05-04 01:40:00 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) |
| 2025-05-04 01:42:22 +0200 | hiredman | (~hiredman@frontier1.downey.family) (Quit: Lost terminal) |
| 2025-05-04 01:46:12 +0200 | la1n2 | (~la1n@176.59.166.253) (Read error: Connection reset by peer) |
| 2025-05-04 01:47:58 +0200 | la1n2 | (~la1n@176.59.56.11) |
| 2025-05-04 01:53:42 +0200 | AlexZenon_2 | (~alzenon@5.139.233.9) |
| 2025-05-04 01:55:15 +0200 | la1n23 | (~la1n@109.197.206.191) |
| 2025-05-04 01:55:16 +0200 | AlexZenon | (~alzenon@5.139.233.9) (Ping timeout: 252 seconds) |
| 2025-05-04 01:55:22 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-05-04 01:57:50 +0200 | la1n2 | (~la1n@176.59.56.11) (Ping timeout: 252 seconds) |
| 2025-05-04 01:58:55 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-05-04 01:59:29 +0200 | euleritian | (~euleritia@dynamic-176-006-135-247.176.6.pool.telefonica.de) |
| 2025-05-04 02:07:14 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2025-05-04 02:09:49 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-05-04 02:12:33 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 2025-05-04 02:14:51 +0200 | sprotte24 | (~sprotte24@p200300d16f17ff001d650b9c3df58534.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-05-04 02:17:21 +0200 | Pozyomka | (~pyon@user/pyon) pyon |
| 2025-05-04 02:20:31 +0200 | sajenim | (~sajenim@user/sajenim) sajenim |
| 2025-05-04 02:51:04 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 276 seconds) |
| 2025-05-04 02:51:33 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) gabriel_sevecek |
| 2025-05-04 03:05:46 +0200 | bilegeek | (~bilegeek@2600:1008:b01a:5c24:8c91:aa31:8c9:aaf) (Quit: Leaving) |
| 2025-05-04 03:07:45 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-05-04 03:20:58 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 2025-05-04 03:21:26 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.2) |
| 2025-05-04 03:28:19 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 245 seconds) |
| 2025-05-04 03:28:26 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 03:39:09 +0200 | jackdk | (sid373013@cssa/jackdk) (Changing host) |
| 2025-05-04 03:39:09 +0200 | jackdk | (sid373013@cssa/life/jackdk) jackdk |
| 2025-05-04 03:40:49 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-05-04 03:42:02 +0200 | j1n37- | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-05-04 03:45:53 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 03:46:10 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 2025-05-04 04:05:01 +0200 | op_4 | (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 2025-05-04 04:05:36 +0200 | op_4 | (~tslil@user/op-4/x-9116473) op_4 |
| 2025-05-04 04:08:49 +0200 | xff0x | (~xff0x@2405:6580:b080:900:7099:7f52:1441:1e43) (Ping timeout: 248 seconds) |
| 2025-05-04 04:12:52 +0200 | typedfern_ | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 2025-05-04 04:13:42 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 276 seconds) |
| 2025-05-04 04:15:49 +0200 | td_ | (~td@i53870919.versanet.de) (Ping timeout: 248 seconds) |
| 2025-05-04 04:17:38 +0200 | td_ | (~td@i53870915.versanet.de) |
| 2025-05-04 04:21:12 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2025-05-04 04:23:24 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 04:44:00 +0200 | euleritian | (~euleritia@dynamic-176-006-135-247.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 04:48:43 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 05:00:31 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-05-04 05:00:31 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-05-04 05:00:50 +0200 | califax | (~califax@user/califx) califx |
| 2025-05-04 05:01:14 +0200 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-05-04 05:21:56 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2025-05-04 05:22:31 +0200 | xff0x | (~xff0x@2405:6580:b080:900:e1a9:cd8e:4cbb:591b) |
| 2025-05-04 05:36:10 +0200 | infinity0 | (~infinity0@pwned.gg) (Ping timeout: 276 seconds) |
| 2025-05-04 05:36:52 +0200 | infinity0 | (~infinity0@pwned.gg) infinity0 |
| 2025-05-04 05:38:12 +0200 | tomku | (~tomku@user/tomku) (Ping timeout: 276 seconds) |
| 2025-05-04 05:42:36 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 05:43:34 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-04 05:44:33 +0200 | tomku | (~tomku@user/tomku) tomku |
| 2025-05-04 05:47:49 +0200 | aforemny_ | (~aforemny@i59F4C6FD.versanet.de) aforemny |
| 2025-05-04 05:48:06 +0200 | aforemny | (~aforemny@i59F4C605.versanet.de) (Ping timeout: 252 seconds) |
| 2025-05-04 06:08:54 +0200 | <haskellbridge> | <hellwolf> Huh? |
| 2025-05-04 06:09:05 +0200 | <haskellbridge> | <hellwolf> sonic boom? |
| 2025-05-04 06:15:26 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 06:15:58 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 06:16:19 +0200 | <haskellbridge> | <hellwolf> anyways, today is the day to confront the demon... |
| 2025-05-04 06:16:19 +0200 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/xIZbjVwEiWebhDhhUHdAQgaI/rbHeUYfmCGw (4 lines) |
| 2025-05-04 06:18:03 +0200 | <monochrom> | I think for sum types you go for prisms rather than lenses. |
| 2025-05-04 06:23:10 +0200 | <haskellbridge> | <hellwolf> makePrisms |
| 2025-05-04 06:23:54 +0200 | <haskellbridge> | <hellwolf> let me see that i can learn there. |
| 2025-05-04 06:23:54 +0200 | <haskellbridge> | also, should i use generics-sop, though i would need code examples... |
| 2025-05-04 06:27:05 +0200 | <haskellbridge> | <hellwolf> https://hackage-content.haskell.org/package/lens-5.3.4/docs/src/Control.Lens.Internal.PrismTH.html… |
| 2025-05-04 06:27:07 +0200 | <haskellbridge> | not too many lines to learn. it seems. i am relieved |
| 2025-05-04 06:29:37 +0200 | sim590 | (~simon@209-15-185-101.resi.cgocable.ca) (Ping timeout: 248 seconds) |
| 2025-05-04 06:52:13 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Ping timeout: 276 seconds) |
| 2025-05-04 06:56:21 +0200 | <haskellbridge> | <hellwolf> "isn't :: Prism s t a b -> s -> Bool" |
| 2025-05-04 06:56:21 +0200 | <haskellbridge> | finally i see others using the single quote in names... |
| 2025-05-04 06:56:45 +0200 | <monochrom> | :) |
| 2025-05-04 06:59:21 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-04 07:16:05 +0200 | <EvanR> | ahem |
| 2025-05-04 07:16:18 +0200 | <EvanR> | please. apostrophe |
| 2025-05-04 07:35:04 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 07:35:10 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 07:44:10 +0200 | bitmapper | (uid464869@id-464869.lymington.irccloud.com) bitmapper |
| 2025-05-04 07:59:18 +0200 | joeyadams | (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 2025-05-04 08:05:52 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 2025-05-04 08:13:07 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-05-04 08:23:21 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-04 08:24:13 +0200 | haritz | (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 2025-05-04 08:25:57 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) acidjnk |
| 2025-05-04 08:26:36 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 08:32:17 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 08:32:44 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-05-04 08:37:54 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-05-04 08:46:57 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 08:53:50 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 09:00:00 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-05-04 09:00:38 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-05-04 09:01:32 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 09:04:44 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 09:07:14 +0200 | la1n2 | (~la1n@81.222.176.125) |
| 2025-05-04 09:09:53 +0200 | la1n23 | (~la1n@109.197.206.191) (Ping timeout: 265 seconds) |
| 2025-05-04 09:22:39 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-05-04 09:23:45 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 2025-05-04 09:24:02 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2025-05-04 09:25:41 +0200 | <haskellbridge> | <hellwolf> what's the reason for classy lenses or prisma? It's non obvious to me, and the docs doesn't explain the "why" |
| 2025-05-04 09:40:04 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 2025-05-04 09:52:20 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-05-04 10:32:55 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-05-04 10:35:02 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 10:35:04 +0200 | <jackdk> | hellwolf: https://youtu.be/GZPup5Iuaqw?t=1499 (note the timecode, though the whole talk is good) |
| 2025-05-04 10:50:59 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-05-04 10:57:16 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-05-04 10:57:39 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 11:08:06 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-05-04 11:10:29 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) Tuplanolla |
| 2025-05-04 11:13:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) |
| 2025-05-04 11:16:27 +0200 | <haskellbridge> | <hellwolf> thank you! checking now |
| 2025-05-04 11:21:57 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-05-04 11:22:22 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-05-04 11:37:12 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-05-04 11:47:19 +0200 | Square | (~Square@user/square) (Ping timeout: 276 seconds) |
| 2025-05-04 11:51:05 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 12:00:10 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 12:04:37 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 12:05:04 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 2025-05-04 12:14:42 +0200 | poscat | (~poscat@user/poscat) (Remote host closed the connection) |
| 2025-05-04 12:15:17 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds) |
| 2025-05-04 12:16:50 +0200 | poscat | (~poscat@user/poscat) poscat |
| 2025-05-04 12:27:57 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-05-04 12:31:27 +0200 | <hellwolf> | I watched it. TL;DV: to index optical operations into one type class, so that you can stack them up in your application monad. It's probably obvious if you actually build such a application that deal with real world :) |
| 2025-05-04 12:33:27 +0200 | <Rembane> | That sounds neat |
| 2025-05-04 12:36:50 +0200 | <hellwolf> | I wish the docs actually care to give just a few lines of "why". But I guess it risks of being too brief and confuses some people. Not sure what's the good middle ground of these sort of things is. |
| 2025-05-04 12:38:34 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-05-04 12:45:48 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 12:52:13 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 265 seconds) |
| 2025-05-04 12:53:03 +0200 | hiecaq | (~hiecaq@user/hiecaq) hiecaq |
| 2025-05-04 13:00:43 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 13:07:29 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-05-04 13:07:59 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 13:08:16 +0200 | aljazmc | (~aljazmc@user/aljazmc) aljazmc |
| 2025-05-04 13:13:44 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2025-05-04 13:16:15 +0200 | gabiruh | (~gabiruh@vps19177.publiccloud.com.br) gabiruh |
| 2025-05-04 13:25:08 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) |
| 2025-05-04 13:38:10 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 2025-05-04 13:45:09 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 13:51:28 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 13:51:45 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 13:52:15 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 13:58:36 +0200 | <[exa]> | are there some good "small" libraries theorem proving? E.g. I've got an algebra, a few axioms on it, and I want to see how the axioms can be combined to derive some expression in the algebra. Ideally if axiom schemes are supported. |
| 2025-05-04 13:58:47 +0200 | <[exa]> | s/if // |
| 2025-05-04 14:01:26 +0200 | <[exa]> | the issue with the theorem provers I see is that they kinda assume some particular fixed algebra (some kind of logic), I need some freedom in there without having to encode stuff too much. |
| 2025-05-04 14:04:14 +0200 | <tomsmeding> | prolog? |
| 2025-05-04 14:05:46 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-04 14:11:57 +0200 | tolgo | (~Thunderbi@199.115.144.130) |
| 2025-05-04 14:14:12 +0200 | tolgo | (~Thunderbi@199.115.144.130) (Client Quit) |
| 2025-05-04 14:15:19 +0200 | <[exa]> | tomsmeding: yeah like I could go full ListT but I guess it will need heuristics |
| 2025-05-04 14:16:02 +0200 | <[exa]> | s/List/Logic/ |
| 2025-05-04 14:21:16 +0200 | <tomsmeding> | I mean you can actually model a proof checker, but at that point you're writing what you're asking already exists, I guess :p |
| 2025-05-04 14:21:47 +0200 | <tomsmeding> | what kind of things do you want to prove? |
| 2025-05-04 14:22:24 +0200 | <tomsmeding> | and do you want there to be proof search or just checking of manual proofs |
| 2025-05-04 14:26:50 +0200 | <haskellbridge> | <hellwolf> I wonder how well LLM nowadays to cope with these sort of things when it comes to heuristics |
| 2025-05-04 14:31:23 +0200 | <[exa]> | hellwolf: if the heuristic is "there was more chat about it on the internet", it's going great. |
| 2025-05-04 14:32:31 +0200 | <[exa]> | tomsmeding: I've just started reading up on the whole topic. Looks like I wanted more of a program synthesis. :D |
| 2025-05-04 14:35:19 +0200 | <haskellbridge> | <hellwolf> I think the hvm person is doing this entire neogen thing, banking on LLM model. |
| 2025-05-04 14:35:31 +0200 | <[exa]> | and yeah well it's actually prolog. I want to write constraints on what holds "before" and should hold "after" the program, and the thing would ideally fill in some "middle" so that the "after" is satisfied. |
| 2025-05-04 14:36:52 +0200 | <[exa]> | hellwolf: what's hvm and neogen? (googling leads to either twiddler or spam, which is sus) |
| 2025-05-04 14:37:20 +0200 | <tomsmeding> | [exa]: oh that definitely sounds like program synthesis :p |
| 2025-05-04 14:38:18 +0200 | <tomsmeding> | and I mean, coding up a simple engine that tries to deduce a sequent from given ones with BFS isn't too hrad |
| 2025-05-04 14:38:41 +0200 | <haskellbridge> | <hellwolf> https://x.com/VictorTaelin he is the frontman doing it. There is this VC vibe thing: so, there is sometimes selling before confirmation bias, but there are some interesting bits from time to time. I don't fully follow, tbh |
| 2025-05-04 14:38:52 +0200 | <[exa]> | tomsmeding: the issue is that my "instructions" won't very "simple" (usually multiple effects tied together), so just going the syntax way ("forth is instructions!") is going to be brutally bad |
| 2025-05-04 14:39:01 +0200 | <tomsmeding> | and that sounds limited, but if you want something more than can be expressed to an engine like that, things become very hard, very undecidable, very quickly |
| 2025-05-04 14:39:17 +0200 | <tomsmeding> | I see |
| 2025-05-04 14:39:28 +0200 | <haskellbridge> | <hellwolf> - bias of selling before confirmed result. |
| 2025-05-04 14:39:45 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 14:39:53 +0200 | <[exa]> | hellwolf: I'd classify as scam tbh |
| 2025-05-04 14:40:05 +0200 | tomsmeding | is afk for a while, sory |
| 2025-05-04 14:40:10 +0200 | <tomsmeding> | *sorry |
| 2025-05-04 14:40:28 +0200 | <haskellbridge> | <hellwolf> I know what you mean. But I will not be so quick to judge. |
| 2025-05-04 14:40:46 +0200 | <[exa]> | tomsmeding: np enjoy the sunday :D |
| 2025-05-04 14:41:12 +0200 | haskellbridge | hellwolf go doing something relax too. enjoy your sunday folks |
| 2025-05-04 14:42:42 +0200 | tremon | (~tremon@83.80.159.219) tremon |
| 2025-05-04 14:43:55 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 2025-05-04 14:44:57 +0200 | <[exa]> | hellwolf: oh hvm is the thing with the "MAGIC" wannabe meme in the main readme |
| 2025-05-04 14:45:26 +0200 | <[exa]> | turns out I already classified it as such like 2 years ago :D |
| 2025-05-04 14:51:52 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-05-04 14:53:02 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 14:53:09 +0200 | aljazmc | (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 2025-05-04 14:55:30 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 14:55:48 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 14:56:11 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-05-04 14:57:27 +0200 | <[exa]> | well screw it, I guess I'll do an A* and blame the heuristics. :D |
| 2025-05-04 14:58:51 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-05-04 14:59:44 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 15:02:29 +0200 | <haskellbridge> | <hellwolf> data AThing a = DoSomethingWith a Person | ScamWith a Person |
| 2025-05-04 15:06:47 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-05-04 15:11:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 15:12:09 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 15:14:59 +0200 | AlexZenon_2 | AlexZenon |
| 2025-05-04 15:19:18 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-05-04 15:22:42 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2025-05-04 15:24:07 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) (Quit: Bye) |
| 2025-05-04 15:26:26 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-05-04 15:28:54 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 15:29:11 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 15:29:59 +0200 | la1n2 | (~la1n@81.222.176.125) (Read error: Connection reset by peer) |
| 2025-05-04 15:30:02 +0200 | TimWolla | (~timwolla@2a01:4f8:150:6153:beef::6667) TimWolla |
| 2025-05-04 15:31:49 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-05-04 15:35:56 +0200 | la1n | (~la1n@85.249.17.224) |
| 2025-05-04 15:40:27 +0200 | la1n2 | (~la1n@176.59.41.59) |
| 2025-05-04 15:40:46 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 268 seconds) |
| 2025-05-04 15:42:49 +0200 | la1n | (~la1n@85.249.17.224) (Ping timeout: 244 seconds) |
| 2025-05-04 15:51:13 +0200 | tabaqui | (~tabaqui@167.71.80.236) tabaqui |
| 2025-05-04 16:22:48 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Ping timeout: 252 seconds) |
| 2025-05-04 16:22:59 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-05-04 16:22:59 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-05-04 16:22:59 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-05-04 16:23:04 +0200 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-05-04 16:23:10 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 2025-05-04 16:25:09 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
| 2025-05-04 16:25:22 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 2025-05-04 16:32:21 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 16:38:56 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 16:50:18 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 2025-05-04 16:52:27 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
| 2025-05-04 16:53:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2025-05-04 16:54:06 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 16:56:17 +0200 | typedfern_ | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 248 seconds) |
| 2025-05-04 16:56:42 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-05-04 16:56:56 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) typedfern |
| 2025-05-04 17:04:03 +0200 | noctuks | (MR7CNKXm0J@user/noctux) (Quit: WeeChat 4.5.1) |
| 2025-05-04 17:04:04 +0200 | yushyin | (qjh7DQNxXf@mail.karif.server-speed.net) (Quit: WeeChat 4.5.1) |
| 2025-05-04 17:04:04 +0200 | s4msung | (HpS7xJgsJj@user/s4msung) (Quit: s4msung) |
| 2025-05-04 17:04:24 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 17:04:40 +0200 | noctuks | (d32f0pjuYL@user/noctux) noctux |
| 2025-05-04 17:04:44 +0200 | s4msung | (K4xiEoBBTh@user/s4msung) s4msung |
| 2025-05-04 17:04:44 +0200 | yushyin | (zv27G51Tbg@mail.karif.server-speed.net) yushyin |
| 2025-05-04 17:04:54 +0200 | <Pozyomka> | Is there any good reason why Data.Sequence doesn't export a function “adjustF :: Functor f => (a -> f a) -> Int -> Seq a -> f (Seq a)”? |
| 2025-05-04 17:06:30 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 268 seconds) |
| 2025-05-04 17:08:52 +0200 | Typedfern | (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 2025-05-04 17:11:34 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 2025-05-04 17:12:42 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2025-05-04 17:16:27 +0200 | m1dnight | (~m1dnight@d8D861908.access.telenet.be) m1dnight |
| 2025-05-04 17:28:00 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-05-04 17:30:01 +0200 | <[exa]> | Pozyomka: not really but maybe it would be redundant with other functions there? |
| 2025-05-04 17:39:08 +0200 | hiecaq | (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 2025-05-04 17:43:50 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 2025-05-04 17:44:03 +0200 | <[exa]> | ok well probably not the case, the internal "single-lookup adjust" in the package doesn't seem to support passing the functors through |
| 2025-05-04 17:44:23 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 17:44:37 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-05-04 17:45:40 +0200 | sajenim | (~sajenim@user/sajenim) (Ping timeout: 252 seconds) |
| 2025-05-04 17:50:53 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-05-04 17:55:15 +0200 | <int-e> | The Data.Map version of this introduces some pretty heavy machinery to both find the altered element and remember the path to the corresponding leaf, and then reuses that path to speed up the update process. For Data.Sequence.Seq I think the potential savings over the obvious lookup and then fmap adjust aren't nearly as impressive. |
| 2025-05-04 17:56:07 +0200 | <int-e> | :t Data.Map.adjustF |
| 2025-05-04 17:56:08 +0200 | <lambdabot> | error: |
| 2025-05-04 17:56:09 +0200 | <lambdabot> | Not in scope: ‘Data.Map.adjustF’ |
| 2025-05-04 17:56:09 +0200 | <lambdabot> | Perhaps you meant one of these: |
| 2025-05-04 17:56:31 +0200 | <int-e> | :t Data.Map.alterF |
| 2025-05-04 17:56:32 +0200 | <lambdabot> | (Functor f, Ord k) => (Maybe a -> f (Maybe a)) -> k -> M.Map k a -> f (M.Map k a) |
| 2025-05-04 17:58:50 +0200 | <int-e> | (Even for Data.Map, I believe the main thing it saves is repeated key comparisons. Which of course may be expensive, depending on the key type.) |
| 2025-05-04 18:05:36 +0200 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) alecs |
| 2025-05-04 18:11:08 +0200 | <Pozyomka> | The lengths through which Haskell programmers go to avoid defining types to represent intermediate steps of the lookup process... “I'd rather write a higher-order function with a Functor constraint than define a zipper type!” |
| 2025-05-04 18:16:34 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 2025-05-04 18:18:42 +0200 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 2025-05-04 18:19:23 +0200 | <Pozyomka> | int-e: “pretty heavy machinery” -- Are zippers heavy machinery now? |
| 2025-05-04 18:20:50 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 18:25:23 +0200 | <int-e> | Pozyomka: there's no zipper |
| 2025-05-04 18:25:44 +0200 | <int-e> | it remembers a path in a bit mask |
| 2025-05-04 18:26:21 +0200 | <Pozyomka> | Wow, that's just... bonkers. |
| 2025-05-04 18:26:36 +0200 | <int-e> | and as far as I can tell, that was introduced just for the benefit of alterF |
| 2025-05-04 18:27:03 +0200 | <int-e> | that said, yes, zippers are heavy machinery in the sense that they tend to require a lot of code for non-trivial data structures |
| 2025-05-04 18:27:58 +0200 | <Pozyomka> | Wow, and there's magical constants in the code too... |
| 2025-05-04 18:29:13 +0200 | <geekosaur> | and, uh, look at the implementation. they're usually pretty expensive. I mean, even a list zipper turns one list into two plus a lot of pushing and popping |
| 2025-05-04 18:35:22 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-05-04 18:38:33 +0200 | <EvanR> | I'm ok if Data.Map's implementation is packed with esoteric constants and jiggery pokery if it means more performance and I never have to mess with it xD |
| 2025-05-04 18:39:47 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 18:40:05 +0200 | euleritian | (~euleritia@77.23.248.47) |
| 2025-05-04 18:41:39 +0200 | euleritian | (~euleritia@77.23.248.47) (Read error: Connection reset by peer) |
| 2025-05-04 18:42:12 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 264 seconds) |
| 2025-05-04 18:42:19 +0200 | euleritian | (~euleritia@77.23.248.47) |
| 2025-05-04 18:42:23 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-05-04 18:43:44 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-05-04 18:46:44 +0200 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-05-04 18:55:19 +0200 | Arpad | (~Arpad@2a02:ab88:38d:4700::b0d5) |
| 2025-05-04 18:56:03 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-05-04 18:57:29 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 268 seconds) |
| 2025-05-04 18:58:01 +0200 | Guest70 | (~Guest80@82.153.135.43) |
| 2025-05-04 18:58:47 +0200 | ttybitnik | (~ttybitnik@user/wolper) (Remote host closed the connection) |
| 2025-05-04 18:59:31 +0200 | Guest70 | (~Guest80@82.153.135.43) (Client Quit) |
| 2025-05-04 19:00:52 +0200 | ystael | (~ystael@user/ystael) ystael |
| 2025-05-04 19:03:28 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-05-04 19:03:45 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-05-04 19:04:00 +0200 | <hellwolf> | | Couldn't match type ‘BOOL’ with ‘(BOOL, b10)’ |
| 2025-05-04 19:04:00 +0200 | <hellwolf> | I always have trouble reading this sentence: Which one was expected, and which one was actual? |
| 2025-05-04 19:05:39 +0200 | euleritian | (~euleritia@77.23.248.47) (Ping timeout: 244 seconds) |
| 2025-05-04 19:06:06 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 2025-05-04 19:06:27 +0200 | <int-e> | > let b = (b,b) in () |
| 2025-05-04 19:06:29 +0200 | <lambdabot> | error: |
| 2025-05-04 19:06:29 +0200 | <lambdabot> | • Occurs check: cannot construct the infinite type: a ~ (a, b) |
| 2025-05-04 19:06:29 +0200 | <lambdabot> | • In the expression: b |
| 2025-05-04 19:06:41 +0200 | <int-e> | ah no |
| 2025-05-04 19:06:47 +0200 | euleritian | (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-05-04 19:06:59 +0200 | <int-e> | > let False = () in () |
| 2025-05-04 19:07:00 +0200 | <lambdabot> | error: |
| 2025-05-04 19:07:00 +0200 | <lambdabot> | • Couldn't match expected type ‘Bool’ with actual type ‘()’ |
| 2025-05-04 19:07:00 +0200 | <lambdabot> | • In the expression: () |
| 2025-05-04 19:07:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-05-04 19:07:20 +0200 | <hellwolf> | since when |
| 2025-05-04 19:07:37 +0200 | <hellwolf> | actually, sometimes I see the "expected" and "actual" words, sometimes I don't. |
| 2025-05-04 19:08:06 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-05-04 19:08:10 +0200 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-05-04 19:09:46 +0200 | tromp | (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 2025-05-04 19:11:39 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2025-05-04 19:12:55 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2025-05-04 19:15:27 +0200 | JuanDaugherty | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-05-04 19:18:40 +0200 | <int-e> | hellwolf: Okay, so several versions of this exist. One elaborates expected/actual right after the "couldn't match type" (the example is matching the type from an instance implementation with the type class declaraion. Another variant refers to the left-hand and right-hand sides of ~ so the actual/expected distinction makes no sense. There's undoubtedly more scenarios. |
| 2025-05-04 19:21:08 +0200 | <hellwolf> | sounds like low hanging fruits to improve error messages. at least few words wouldn't make it worse. Though, sometimes the message can still be confusing and it takes experience to decypher it. |
| 2025-05-04 19:21:25 +0200 | <hellwolf> | *few more words |
| 2025-05-04 19:21:31 +0200 | <int-e> | *decipher |
| 2025-05-04 19:21:35 +0200 | <hellwolf> | :p |
| 2025-05-04 19:23:33 +0200 | <int-e> | It's hard because the exact error you get depends on the order in which GHC decides to tackle all the constraints it's juggling while type-checking. |
| 2025-05-04 19:24:03 +0200 | <int-e> | IME it does a good job of giving you all the relevant info though the result can be overwhelming. |
| 2025-05-04 19:25:40 +0200 | <hellwolf> | a good job of being verbose, indeed |
| 2025-05-04 19:26:36 +0200 | <int-e> | if it's too much you can usually help the compiler and yourself with extra type signatures |
| 2025-05-04 19:27:01 +0200 | <int-e> | this may break down if you're heavily into type families and other type-level programming |
| 2025-05-04 19:28:45 +0200 | <hellwolf> | I have learned that, and started to save those intermediate steps in the comments. |
| 2025-05-04 19:29:17 +0200 | <hellwolf> | I do prefer the completely indecipherable code in the end without type signature. But the comments stay there. |
| 2025-05-04 19:29:44 +0200 | <hellwolf> | and this time I listened to the Emacs's word correction advice. |
| 2025-05-04 19:31:02 +0200 | <Pozyomka> | In ML, what I normally do is annotate types in module signatures, but not in modules themselves. The Haskell equivalent would be to annotate only the type signatures of those values that the module exports. I find that this works well in practice. |
| 2025-05-04 19:31:21 +0200 | <Pozyomka> | But then, I don't go crazy with type-level programming. Because why would I torture myself that way? |
| 2025-05-04 19:32:49 +0200 | <tomsmeding> | hellwolf: I think GHC is pretty consistent in giving expected/actual full types if there are any such that make sense |
| 2025-05-04 19:33:13 +0200 | <tomsmeding> | (there might be other notes in between the first line and the expected/actual types, so be sure to look further than the top part of the diagnostic) |
| 2025-05-04 19:33:34 +0200 | <tomsmeding> | if there are no such full types, there isn't necessarily any "expected" or "actual" type |
| 2025-05-04 19:34:51 +0200 | <tomsmeding> | e.g. in int-e's example `let False = () in ()`, clearly the error is that Bool is not (), but which of the two is expected, and which of the two is actual? Depends on whether the error comes from the pattern or the right-hand side. And the more type-level shenanigans you do, the more type-equality constraints you get that are not directly attributable to a particular syntactic expression anyway |
| 2025-05-04 19:35:19 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 2025-05-04 19:35:46 +0200 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2025-05-04 19:36:23 +0200 | <tomsmeding> | I fully agree GHC's error messages are often overwhelming and sometimes (or often, depending on the kind of code you write) unhelpful -- but if you start thinking about how to do better, one tends to quickly realise that sure, one can do better on the particular code you have, but can one do better without overfitting to your code, and without making other cases worse? It's actually not easy, |
| 2025-05-04 19:36:25 +0200 | <tomsmeding> | sometimes. |
| 2025-05-04 19:36:58 +0200 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 19:37:39 +0200 | <Pozyomka> | The type errors are the most unhelpful when you're trying to be too clever. |
| 2025-05-04 19:40:53 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-05-04 19:40:57 +0200 | <tomsmeding> | or trying to do too much theorem proving |
| 2025-05-04 19:42:23 +0200 | <Pozyomka> | Theorem proving is meant to be done with pen, paper and waste basket anyway. Not with a programming language. |
| 2025-05-04 19:42:47 +0200 | <tomsmeding> | there's a rather large set of people that like to use computers to check their work with automated theorem proving |
| 2025-05-04 19:43:01 +0200 | <tomsmeding> | it's not as suited for all kinds of proofs :) |
| 2025-05-04 19:46:48 +0200 | <monochrom> | Hugs has better error messages. |
| 2025-05-04 19:47:33 +0200 | <hellwolf> | if one is motivated enough by the end goal, these are just minor obstacles :) |
| 2025-05-04 19:47:51 +0200 | <int-e> | Hugs has a simpler type system |
| 2025-05-04 19:48:53 +0200 | <monochrom> | Yes, it's why. |
| 2025-05-04 19:49:08 +0200 | <monochrom> | Moreover, the other pasture is always greener. :) |
| 2025-05-04 19:52:58 +0200 | Googulator33 | (~Googulato@2a01-036d-0106-4a24-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 2025-05-04 19:53:55 +0200 | <monochrom> | At some point we just have to say what Stroustrup said. People complain about GHC because it is actually used. |
| 2025-05-04 19:54:50 +0200 | <hellwolf> | continuing along your interesting analogy, is it a "grass hopper" a suitable way to describe people jumping languages. |
| 2025-05-04 19:55:04 +0200 | <hellwolf> | Sure, Stroustrup said. |
| 2025-05-04 19:55:37 +0200 | <int-e> | Let me guess: There's two kinds of languages, those that everybody complains about and those that nobody uses. |
| 2025-05-04 19:55:55 +0200 | <geekosaur> | sounds about right |
| 2025-05-04 19:56:27 +0200 | <monochrom> | Rear Admiral Grass Hopper would like you to jump to COBOL. >:) |
| 2025-05-04 19:56:30 +0200 | Googulator77 | (~Googulato@2a01-036d-0106-4a24-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Ping timeout: 240 seconds) |
| 2025-05-04 19:56:40 +0200 | <hellwolf> | I think if we are all net givers, in that we complain only if we have contributed, probably we will be of a better world. |
| 2025-05-04 19:57:27 +0200 | geekosaur | already did his time there, tyvm |
| 2025-05-04 19:57:29 +0200 | <hellwolf> | Mount my COBOL, fumble thy registers? |
| 2025-05-04 19:57:46 +0200 | Arpad | (~Arpad@2a02:ab88:38d:4700::b0d5) (Quit: Client closed) |
| 2025-05-04 20:12:22 +0200 | mceresa | (~mceresa@user/mceresa) (Ping timeout: 276 seconds) |
| 2025-05-04 20:15:51 +0200 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-05-04 20:18:15 +0200 | mceresa | (~mceresa@user/mceresa) mceresa |
| 2025-05-04 20:25:38 +0200 | <mauke> | I like ghc's error messages better than hugs's |
| 2025-05-04 20:33:02 +0200 | <[exa]> | Pozyomka: btw re Data.Sequence and zipper, iirc the structure there is already a kinda 2-sided zipper so I can kinda guess why they wouldn't increase the complexity once more |
| 2025-05-04 20:35:09 +0200 | <[exa]> | Pozyomka: otoh I think they (and many other folks) could solve this quite cheaply by exposing an interface like `getset :: Seq a -> Int -> (a, a -> Seq a)`. Not sure if it isn't there already, somewhere. |
| 2025-05-04 20:37:18 +0200 | <Pozyomka> | It's not as efficient as the lens version. You can think of “adjust” as having three steps: (a) locate the element, (b) perform the update, (c) rebuild the sequence. In the lens version, step (b) produces a functorful of new values, and step (c) is a map over those values. |
| 2025-05-04 20:38:23 +0200 | <Pozyomka> | So you can perform step (a) just once, and then step (c) lots of times. Or maybe zero times. Or maybe one time, but only after doing I/O. Or who knows. |
| 2025-05-04 20:47:13 +0200 | <c_wraith> | fwiw, worry about constant factors too much with Seq is.. well, it's a data structure you already aren't using for its constant factors. |
| 2025-05-04 20:48:56 +0200 | <c_wraith> | so the fact that the Ix implementation for Seq doesn't get an optimized internal version really isn't reducing the use cases too much |
| 2025-05-04 20:49:20 +0200 | <monochrom> | One can all day argue about technical merits or demerits why or why not Data.Sequence exposes one more operations, and ignore the social fact that very few people use it and even fewer people contribute PRs so the whole point is moot. |
| 2025-05-04 20:49:58 +0200 | <monochrom> | Or, TL;DR: "Patches welcome". |
| 2025-05-04 20:51:11 +0200 | <c_wraith> | Surprisingly, *nothing* in containers appears to have optimized implementations for ix. Several things do have optimized implementations for at, but Seq can't support it, so... |
| 2025-05-04 20:51:23 +0200 | <EvanR> | noted. Ignoring social facts now |
| 2025-05-04 20:51:32 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) acidjnk |
| 2025-05-04 20:56:43 +0200 | <monochrom> | There are 3 kinds of libraries: Those that everyone complains about, those that no one uses, and those that very few people use but they all complain about. |
| 2025-05-04 20:57:12 +0200 | <int-e> | :t let adjustF f i s = (\x -> Seq.update i x s) <$> f (Seq.index s i) in adjustF |
| 2025-05-04 20:57:13 +0200 | <lambdabot> | Functor f => (t -> f t) -> Int -> Seq.Seq t -> f (Seq.Seq t) |
| 2025-05-04 20:57:23 +0200 | <monochrom> | Unified: There is 1 kind of library: n people use the library and n people complain about it. >:) |
| 2025-05-04 20:58:23 +0200 | <int-e> | (I'm still unconvinced that you can get a meaningful speedup over this naive implementation.) |
| 2025-05-04 21:00:02 +0200 | caconym7 | (~caconym@user/caconym) (Quit: bye) |
| 2025-05-04 21:00:18 +0200 | <int-e> | (I don't know, but it's not obvious where the speedup would come from when rediscovering the path to the leaf to update is a bunch of machine word comparisons. Building up and repeatedly invoking an a -> Seq a function isn't totally free either) |
| 2025-05-04 21:00:43 +0200 | caconym7 | (~caconym@user/caconym) caconym |
| 2025-05-04 21:04:26 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-05-04 21:07:38 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-05-04 21:07:38 +0200 | ljdarj1 | ljdarj |
| 2025-05-04 21:12:06 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2025-05-04 21:12:20 +0200 | califax | (~califax@user/califx) califx |
| 2025-05-04 21:18:44 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 245 seconds) |
| 2025-05-04 21:25:07 +0200 | <hellwolf> | I might have asked, but I can're call. Can you use cabal to run a Main module in interpretation mode, as opposed to compiling it? |
| 2025-05-04 21:25:45 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-05-04 21:30:34 +0200 | <haskellbridge> | <sm> a cabal script does that I think |
| 2025-05-04 21:31:14 +0200 | pavonia | (~user@user/siracusa) siracusa |
| 2025-05-04 21:31:33 +0200 | <monochrom> | `cabal run` can run it, but it compiles first. Is that acceptable? |
| 2025-05-04 21:32:53 +0200 | <geekosaur> | @sm, these days (since cabal 3.8) scripts are compiled, just like stack does |
| 2025-05-04 21:33:53 +0200 | <haskellbridge> | <sm> 👀 |
| 2025-05-04 21:33:56 +0200 | <[exa]> | `echo :main | cabal repl` ? >:) |
| 2025-05-04 21:34:05 +0200 | <monochrom> | If you truly insist on interpreting, yeah cabal repl |
| 2025-05-04 21:34:31 +0200 | <geekosaur> | (it was actually added in 3.6 iirc, but it compiled every time; as of 3.8 it compiles only if the script is changed) |
| 2025-05-04 21:34:35 +0200 | <[exa]> | is there some kinda -c,--command option for repl? |
| 2025-05-04 21:34:43 +0200 | <geekosaur> | --repl-options? |
| 2025-05-04 21:34:44 +0200 | <hellwolf> | no, not acceptable because it litters: |
| 2025-05-04 21:34:44 +0200 | <hellwolf> | ls ~/.cabal/script-builds/| wc -l |
| 2025-05-04 21:34:44 +0200 | <hellwolf> | 30 |
| 2025-05-04 21:34:57 +0200 | <hellwolf> | can I specify entry point for a "cabal repl" session to emulate that? |
| 2025-05-04 21:35:18 +0200 | <geekosaur> | not easily, I think |
| 2025-05-04 21:35:22 +0200 | <hellwolf> | shall I do unix way "echo main" | cabal repl? |
| 2025-05-04 21:35:34 +0200 | <monochrom> | Oh I add some commands in my .profile to clean out that. Because I already need that for my $HOME/tmp and $HOME/Downloads |
| 2025-05-04 21:36:00 +0200 | <geekosaur> | echo :main (args, if needed) | cabal repl --repl-args Foo.hs |
| 2025-05-04 21:36:21 +0200 | <monochrom> | Even for .cabal/packages too. |
| 2025-05-04 21:36:21 +0200 | <geekosaur> | I don't thinlk there's a reasonable way to make runghc work for this |
| 2025-05-04 21:36:53 +0200 | <hellwolf> | so, this is the context: for my edsl project, compiling to a binary seems unnecessary, since all it does is to spit out the code once to the stdout. |
| 2025-05-04 21:37:01 +0200 | <hellwolf> | and it seems slower than just repl it. |
| 2025-05-04 21:37:31 +0200 | <haskellbridge> | <sm> geekosaur I believe you, but it's not mentioned at https://cabal.readthedocs.io/en/latest/cabal-commands.html#cabal-run |
| 2025-05-04 21:37:41 +0200 | Arpad | (~Arpad@2a02:ab88:38d:4700::b0d5) |
| 2025-05-04 21:38:04 +0200 | <hellwolf> | though, repl maybe is -O0, it might be a bit slower to compile at some point. Currently, compiling the target binary itself seems the slow one. |
| 2025-05-04 21:38:31 +0200 | <haskellbridge> | <sm> a stack script will run interpreted by default, unless you add --compile |
| 2025-05-04 21:38:34 +0200 | <geekosaur> | sm, it's not explicitly stated but look for "The executable is cached…" |
| 2025-05-04 21:39:10 +0200 | <haskellbridge> | <sm> 👍️ |
| 2025-05-04 21:40:50 +0200 | <hellwolf> | I remember that behaviour of stack, I really like |
| 2025-05-04 21:41:06 +0200 | <hellwolf> | But my project is too big and I haven't configured stack :/ |
| 2025-05-04 21:41:15 +0200 | <geekosaur> | might put up a cabal issue then |
| 2025-05-04 21:41:21 +0200 | <haskellbridge> | <sm> stack is easy |
| 2025-05-04 21:41:26 +0200 | <haskellbridge> | <sm> I guess you can't use a simple runhaskell script because you want to depend on packages |
| 2025-05-04 21:42:13 +0200 | <hellwolf> | I cannot. But now I learned enough of how these works, after setting up my own customized haskell playground instances, I think I can manage. But maybe I should contribute to Cabal so more people can benefit. |
| 2025-05-04 21:42:19 +0200 | <geekosaur> | meanwhile the only quickfix I can think of is `cabal install --lib --package-env=. <dependencies of script>`, then `runghc script.hs` shopuld work in that directory |
| 2025-05-04 21:42:45 +0200 | <hellwolf> | Easy said than done, due to time. I go to zurihac pre event though, hopefully I can learn from some people to bootstrap Cabal contribution there. |
| 2025-05-04 21:43:12 +0200 | <hellwolf> | I know how to run raw ghc with --package-db... |
| 2025-05-04 21:43:30 +0200 | <hellwolf> | maybe I should really do that, for now. |
| 2025-05-04 21:43:36 +0200 | <haskellbridge> | <sm> just to be clear hellwolf, and of course use what you prefer: a stack script doesn't require "configuring stack", eg no stack.yaml needed |
| 2025-05-04 21:43:46 +0200 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-05-04 21:43:58 +0200 | <tomsmeding> | hellwolf: geekosaur's suggestion of `cabal install --lib --package-env=. ...` sounds like the least-friction approach with cabal, maybe |
| 2025-05-04 21:44:03 +0200 | <hellwolf> | sm: thanks for the tips... I am just wary of having to maintain to build system. |
| 2025-05-04 21:44:12 +0200 | <hellwolf> | *two |
| 2025-05-04 21:44:45 +0200 | <hellwolf> | but you said no stack.yml needed, hmm |
| 2025-05-04 21:44:54 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 2025-05-04 21:45:18 +0200 | <tomsmeding> | sm: can you also put `system-ghc: True` in a stack script somehow, so that it uses GHCup's GHC? |
| 2025-05-04 21:46:03 +0200 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) (Quit: Client closed) |
| 2025-05-04 21:46:12 +0200 | <haskellbridge> | <sm> yes, you can add the --system-ghc and --no-install-ghc flags |
| 2025-05-04 21:48:40 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2025-05-04 21:49:02 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e71c4f52d4f1201e65d300bb.dip0.t-ipconnect.de) acidjnk |
| 2025-05-04 21:49:11 +0200 | <hellwolf> | I tried runghc: it has one other problem, I listed some defaultr extensions in cabal file :D |
| 2025-05-04 21:49:27 +0200 | <hellwolf> | gosh, side effect of relying on build system to list default extensions. |
| 2025-05-04 21:50:07 +0200 | <haskellbridge> | <sm> that's why a lot of people write them in the modules |
| 2025-05-04 21:50:30 +0200 | rvalue- | rvalue |
| 2025-05-04 21:50:30 +0200 | <haskellbridge> | <sm> more verbosity.. but more robust |
| 2025-05-04 21:50:37 +0200 | <hellwolf> | I learned that now. |
| 2025-05-04 21:51:06 +0200 | <hellwolf> | though, I do have a few to list beyond GHC2024 :D |
| 2025-05-04 21:51:15 +0200 | <haskellbridge> | <sm> though you could specify them in the script header too I expect |
| 2025-05-04 21:51:28 +0200 | <hellwolf> | that's right |
| 2025-05-04 21:51:35 +0200 | <hellwolf> | runghc has script header too? |
| 2025-05-04 21:51:40 +0200 | <hellwolf> | cabal, or stack has, I know of. |
| 2025-05-04 21:51:43 +0200 | <haskellbridge> | <sm> but if you want people to write scripts using your lib easily.. then no |
| 2025-05-04 21:52:04 +0200 | <haskellbridge> | <sm> well a runghc shebang script could pass ghc opts to runghc |
| 2025-05-04 21:52:57 +0200 | <haskellbridge> | <sm> though, that's a pain because it varies between linux / mac / freebsd, whether env -S is required in the shebang line |
| 2025-05-04 21:53:32 +0200 | <haskellbridge> | <sm> plus, I think relying on hidden package environment files will suck |
| 2025-05-04 21:54:31 +0200 | <hellwolf> | cat <<EOF |
| 2025-05-04 21:54:31 +0200 | <hellwolf> | package-dbs: clear, global, ${cabal_package_db}, ${yolc_package_db} |
| 2025-05-04 21:54:31 +0200 | <hellwolf> | packages: |
| 2025-05-04 21:54:31 +0200 | <hellwolf> | $cabal_path |
| 2025-05-04 21:54:31 +0200 | <hellwolf> | runyol.cabal |
| 2025-05-04 21:54:32 +0200 | <hellwolf> | EOF |
| 2025-05-04 21:54:48 +0200 | <hellwolf> | I create cabal project file and run cabal <-- what I do |
| 2025-05-04 21:55:20 +0200 | Square | (~Square@user/square) Square |
| 2025-05-04 21:55:36 +0200 | <hellwolf> | now that I have that cabal project file, I just run that within a interpretation mode. |
| 2025-05-04 21:55:45 +0200 | <hellwolf> | *I just want to |
| 2025-05-04 21:56:48 +0200 | <hellwolf> | anyways, feeling like beating a dead horse now, I guess I will have to live with it or do something about it either using stack just for this or fix cabal. |
| 2025-05-04 21:56:58 +0200 | <geekosaur> | cabal exec runghc … ? |
| 2025-05-04 21:58:08 +0200 | <hellwolf> | cabal exec runghc runyol |
| 2025-05-04 21:58:10 +0200 | <hellwolf> | didn't work |
| 2025-05-04 22:01:20 +0200 | <int-e> | maybe: cabal -v0 repl --repl-options="-e main" |
| 2025-05-04 22:03:51 +0200 | <hellwolf> | | Internal error when trying to open a repl for the package fake-package-0. The package is not in the set of available targets for the project plan, which would suggest an inconsistency between readTargetSelectors and resolveTargets. |
| 2025-05-04 22:05:01 +0200 | <int-e> | runghc will probably need something like runghc -ghc-arg=-i -ghc-arg=exe Main.hs |
| 2025-05-04 22:05:11 +0200 | <int-e> | does `cabal run` even work for the thing you're testing |
| 2025-05-04 22:05:12 +0200 | <hellwolf> | it worked |
| 2025-05-04 22:05:18 +0200 | <hellwolf> | hurray |
| 2025-05-04 22:05:33 +0200 | <hellwolf> | let me see if it's faster |
| 2025-05-04 22:05:45 +0200 | <int-e> | err, --ghc-arg= |
| 2025-05-04 22:07:09 +0200 | <hellwolf> | from |
| 2025-05-04 22:07:09 +0200 | <hellwolf> | runbin=$(cabal "$@" -v0 list-bin runyol) |
| 2025-05-04 22:07:09 +0200 | <hellwolf> | "$runbin" || die |
| 2025-05-04 22:07:11 +0200 | <hellwolf> | to: |
| 2025-05-04 22:07:15 +0200 | <hellwolf> | cabal "$@" -v1 repl --repl-options="-e main" RunYol |
| 2025-05-04 22:10:16 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2025-05-04 22:10:46 +0200 | <hellwolf> | 3 ± 2 seconds difference |
| 2025-05-04 22:10:56 +0200 | <hellwolf> | that's added by the linking when building the binary |
| 2025-05-04 22:11:05 +0200 | <hellwolf> | probably not worth the effort, but good to know. |
| 2025-05-04 22:11:20 +0200 | <hellwolf> | thanks everyone. learned a new trick today. |
| 2025-05-04 22:13:03 +0200 | Arpad | (~Arpad@2a02:ab88:38d:4700::b0d5) (Quit: Client closed) |
| 2025-05-04 22:13:48 +0200 | Square2 | (~Square@user/square) Square |
| 2025-05-04 22:20:19 +0200 | user363627 | (~user@user/user363627) user363627 |
| 2025-05-04 22:24:19 +0200 | weary-traveler | (~user@user/user363627) (Ping timeout: 276 seconds) |
| 2025-05-04 22:35:44 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) szkl |
| 2025-05-04 22:44:19 +0200 | hsw | (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) (Read error: Connection reset by peer) |
| 2025-05-04 22:44:26 +0200 | hsw_ | (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) hsw |
| 2025-05-04 22:47:49 +0200 | emergence | (thelounge@vm0.max-p.me) (Ping timeout: 248 seconds) |
| 2025-05-04 22:48:05 +0200 | emergence | (emergence@vm0.max-p.me) emergence |
| 2025-05-04 22:52:12 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2025-05-04 22:57:27 +0200 | ystael | (~ystael@user/ystael) ystael |
| 2025-05-04 23:12:49 +0200 | <hellwolf> | I wish there is such a parameterized Map container type: Map (k :: Type -> Type) (a :: Type -> Type), where k and a are indexed by a same type, so that a changes type as k changes type... |
| 2025-05-04 23:13:43 +0200 | <Rembane> | hellwolf: What problem would that solve for you? |
| 2025-05-04 23:14:12 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 2025-05-04 23:16:25 +0200 | <geekosaur> | @hackage dependent-map |
| 2025-05-04 23:16:25 +0200 | <lambdabot> | https://hackage.haskell.org/package/dependent-map |
| 2025-05-04 23:16:53 +0200 | <geekosaur> | oh, hm, not quite the same thing |