| 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 :) |