Logs on 2025-05-04 (liberachat/#haskell)
| 00:07:14 | → | hiecaq joins (~hiecaq@user/hiecaq) |
| 00:09:49 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 00:12:33 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 248 seconds) |
| 00:14:51 | × | sprotte24 quits (~sprotte24@p200300d16f17ff001d650b9c3df58534.dip0.t-ipconnect.de) (Quit: Leaving) |
| 00:17:21 | → | Pozyomka joins (~pyon@user/pyon) |
| 00:20:31 | → | sajenim joins (~sajenim@user/sajenim) |
| 00:51:04 | × | gabriel_sevecek quits (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 276 seconds) |
| 00:51:33 | → | gabriel_sevecek joins (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 01:05:46 | × | bilegeek quits (~bilegeek@2600:1008:b01a:5c24:8c91:aa31:8c9:aaf) (Quit: Leaving) |
| 01:07:45 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 01:20:58 | × | hiecaq quits (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 01:21:26 | × | __jmcantrell__ quits (~weechat@user/jmcantrell) (Quit: WeeChat 4.6.2) |
| 01:28:19 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 245 seconds) |
| 01:28:26 | → | j1n37- joins (~j1n37@user/j1n37) |
| 01:39:09 | × | jackdk quits (sid373013@cssa/jackdk) (Changing host) |
| 01:39:09 | → | jackdk joins (sid373013@cssa/life/jackdk) |
| 01:40:49 | → | __jmcantrell__ joins (~weechat@user/jmcantrell) |
| 01:42:02 | × | j1n37- quits (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 01:45:53 | → | j1n37 joins (~j1n37@user/j1n37) |
| 01:46:10 | × | ttybitnik quits (~ttybitnik@user/wolper) (Quit: Fading out...) |
| 02:05:01 | × | op_4 quits (~tslil@user/op-4/x-9116473) (Remote host closed the connection) |
| 02:05:36 | → | op_4 joins (~tslil@user/op-4/x-9116473) |
| 02:08:49 | × | xff0x quits (~xff0x@2405:6580:b080:900:7099:7f52:1441:1e43) (Ping timeout: 248 seconds) |
| 02:12:52 | → | typedfern_ joins (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 02:13:42 | × | Typedfern quits (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 276 seconds) |
| 02:15:49 | × | td_ quits (~td@i53870919.versanet.de) (Ping timeout: 248 seconds) |
| 02:17:38 | → | td_ joins (~td@i53870915.versanet.de) |
| 02:21:12 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 02:23:24 | → | tolgo joins (~Thunderbi@199.115.144.130) |
| 02:44:00 | × | euleritian quits (~euleritia@dynamic-176-006-135-247.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 02:48:43 | → | euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 03:00:31 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 03:00:31 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 03:00:50 | → | califax joins (~califax@user/califx) |
| 03:01:14 | → | gmg joins (~user@user/gehmehgeh) |
| 03:21:56 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 03:22:31 | → | xff0x joins (~xff0x@2405:6580:b080:900:e1a9:cd8e:4cbb:591b) |
| 03:36:10 | × | infinity0 quits (~infinity0@pwned.gg) (Ping timeout: 276 seconds) |
| 03:36:52 | → | infinity0 joins (~infinity0@pwned.gg) |
| 03:38:12 | × | tomku quits (~tomku@user/tomku) (Ping timeout: 276 seconds) |
| 03:42:36 | → | j1n37- joins (~j1n37@user/j1n37) |
| 03:43:34 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 03:44:33 | → | tomku joins (~tomku@user/tomku) |
| 03:47:49 | → | aforemny_ joins (~aforemny@i59F4C6FD.versanet.de) |
| 03:48:06 | × | aforemny quits (~aforemny@i59F4C605.versanet.de) (Ping timeout: 252 seconds) |
| 04:08:54 | <haskellbridge> | <hellwolf> Huh? |
| 04:09:05 | <haskellbridge> | <hellwolf> sonic boom? |
| 04:15:26 | → | j1n37 joins (~j1n37@user/j1n37) |
| 04:15:58 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 04:16:19 | <haskellbridge> | <hellwolf> anyways, today is the day to confront the demon... |
| 04:16:19 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/xIZbjVwEiWebhDhhUHdAQgaI/rbHeUYfmCGw (4 lines) |
| 04:18:03 | <monochrom> | I think for sum types you go for prisms rather than lenses. |
| 04:23:10 | <haskellbridge> | <hellwolf> makePrisms |
| 04:23:54 | <haskellbridge> | <hellwolf> let me see that i can learn there. |
| 04:23:54 | <haskellbridge> | also, should i use generics-sop, though i would need code examples... |
| 04:27:05 | <haskellbridge> | <hellwolf> https://hackage-content.haskell.org/package/lens-5.3.4/docs/src/Control.Lens.Internal.PrismTH.html#makePrisms |
| 04:27:07 | <haskellbridge> | not too many lines to learn. it seems. i am relieved |
| 04:29:37 | × | sim590 quits (~simon@209-15-185-101.resi.cgocable.ca) (Ping timeout: 248 seconds) |
| 04:52:13 | × | tolgo quits (~Thunderbi@199.115.144.130) (Ping timeout: 276 seconds) |
| 04:56:21 | <haskellbridge> | <hellwolf> "isn't :: Prism s t a b -> s -> Bool" |
| 04:56:21 | <haskellbridge> | finally i see others using the single quote in names... |
| 04:56:45 | <monochrom> | :) |
| 04:59:21 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:16:05 | <EvanR> | ahem |
| 05:16:18 | <EvanR> | please. apostrophe |
| 05:35:04 | → | j1n37- joins (~j1n37@user/j1n37) |
| 05:35:10 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 05:44:10 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 05:59:18 | × | joeyadams quits (~textual@syn-162-154-010-038.res.spectrum.com) (Quit: Textual IRC Client: www.textualapp.com) |
| 06:05:52 | × | __jmcantrell__ quits (~weechat@user/jmcantrell) (Ping timeout: 244 seconds) |
| 06:13:07 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 06:23:21 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 06:24:13 | × | haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in) |
| 06:25:57 | → | acidjnk_new3 joins (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) |
| 06:26:36 | → | tromp joins (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 06:32:17 | → | j1n37 joins (~j1n37@user/j1n37) |
| 06:32:44 | × | j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 06:37:54 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 06:46:57 | → | euphores joins (~SASL_euph@user/euphores) |
| 06:53:50 | × | tromp quits (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 07:00:00 | × | caconym7 quits (~caconym@user/caconym) (Quit: bye) |
| 07:00:38 | → | caconym7 joins (~caconym@user/caconym) |
| 07:01:32 | → | tromp joins (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 07:04:44 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 07:07:14 | → | la1n2 joins (~la1n@81.222.176.125) |
| 07:09:53 | × | la1n23 quits (~la1n@109.197.206.191) (Ping timeout: 265 seconds) |
| 07:22:39 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 07:23:45 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 276 seconds) |
| 07:24:02 | Lord_of_Life_ | is now known as Lord_of_Life |
| 07:25:41 | <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" |
| 07:40:04 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 272 seconds) |
| 07:52:20 | → | __monty__ joins (~toonn@user/toonn) |
| 08:32:55 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:35:02 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 08:35:04 | <jackdk> | hellwolf: https://youtu.be/GZPup5Iuaqw?t=1499 (note the timecode, though the whole talk is good) |
| 08:50:59 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 08:57:16 | × | euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 08:57:39 | → | euleritian joins (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 09:08:06 | × | acidjnk_new3 quits (~acidjnk@p200300d6e71c4f7604057216e123cf7a.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 09:10:29 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 09:13:08 | → | acidjnk_new3 joins (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) |
| 09:16:27 | <haskellbridge> | <hellwolf> thank you! checking now |
| 09:21:57 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 09:22:22 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 09:37:12 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:47:19 | × | Square quits (~Square@user/square) (Ping timeout: 276 seconds) |
| 09:51:05 | × | tromp quits (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:00:10 | → | poscat joins (~poscat@user/poscat) |
| 10:04:37 | → | tromp joins (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 10:05:04 | × | euleritian quits (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 10:14:42 | × | poscat quits (~poscat@user/poscat) (Remote host closed the connection) |
| 10:15:17 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds) |
| 10:16:50 | → | poscat joins (~poscat@user/poscat) |
| 10:27:57 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 10:31:27 | <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 :) |
| 10:33:27 | <Rembane> | That sounds neat |
| 10:36:50 | <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. |
| 10:38:34 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 10:45:48 | → | aljazmc joins (~aljazmc@user/aljazmc) |
| 10:52:13 | × | gabiruh quits (~gabiruh@vps19177.publiccloud.com.br) (Ping timeout: 265 seconds) |
| 10:53:03 | → | hiecaq joins (~hiecaq@user/hiecaq) |
| 11:00:43 | → | euleritian joins (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 11:07:29 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 11:07:59 | × | aljazmc quits (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 11:08:16 | → | aljazmc joins (~aljazmc@user/aljazmc) |
| 11:13:44 | × | acidjnk_new3 quits (~acidjnk@p200300d6e71c4f525d73c8bc79cfad4f.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 11:16:15 | → | gabiruh joins (~gabiruh@vps19177.publiccloud.com.br) |
| 11:25:08 | → | acidjnk_new3 joins (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) |
| 11:38:10 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 11:45:09 | → | euphores joins (~SASL_euph@user/euphores) |
| 11:51:28 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 11:51:45 | × | euleritian quits (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 11:52:15 | → | euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 11:58:36 | <[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. |
| 11:58:47 | <[exa]> | s/if // |
| 12:01:26 | <[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. |
| 12:04:14 | <tomsmeding> | prolog? |
| 12:05:46 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 12:11:57 | → | tolgo joins (~Thunderbi@199.115.144.130) |
| 12:14:12 | × | tolgo quits (~Thunderbi@199.115.144.130) (Client Quit) |
| 12:15:19 | <[exa]> | tomsmeding: yeah like I could go full ListT but I guess it will need heuristics |
| 12:16:02 | <[exa]> | s/List/Logic/ |
| 12:21:16 | <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 |
| 12:21:47 | <tomsmeding> | what kind of things do you want to prove? |
| 12:22:24 | <tomsmeding> | and do you want there to be proof search or just checking of manual proofs |
| 12:26:50 | <haskellbridge> | <hellwolf> I wonder how well LLM nowadays to cope with these sort of things when it comes to heuristics |
| 12:31:23 | <[exa]> | hellwolf: if the heuristic is "there was more chat about it on the internet", it's going great. |
| 12:32:31 | <[exa]> | tomsmeding: I've just started reading up on the whole topic. Looks like I wanted more of a program synthesis. :D |
| 12:35:19 | <haskellbridge> | <hellwolf> I think the hvm person is doing this entire neogen thing, banking on LLM model. |
| 12:35:31 | <[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. |
| 12:36:52 | <[exa]> | hellwolf: what's hvm and neogen? (googling leads to either twiddler or spam, which is sus) |
| 12:37:20 | <tomsmeding> | [exa]: oh that definitely sounds like program synthesis :p |
| 12:38:18 | <tomsmeding> | and I mean, coding up a simple engine that tries to deduce a sequent from given ones with BFS isn't too hrad |
| 12:38:41 | <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 |
| 12:38:52 | <[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 |
| 12:39:01 | <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 |
| 12:39:17 | <tomsmeding> | I see |
| 12:39:28 | <haskellbridge> | <hellwolf> - bias of selling before confirmed result. |
| 12:39:45 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 12:39:53 | <[exa]> | hellwolf: I'd classify as scam tbh |
| 12:40:05 | tomsmeding | is afk for a while, sory |
| 12:40:10 | <tomsmeding> | *sorry |
| 12:40:28 | <haskellbridge> | <hellwolf> I know what you mean. But I will not be so quick to judge. |
| 12:40:46 | <[exa]> | tomsmeding: np enjoy the sunday :D |
| 12:41:12 | haskellbridge | hellwolf go doing something relax too. enjoy your sunday folks |
| 12:42:42 | → | tremon joins (~tremon@83.80.159.219) |
| 12:43:55 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 12:44:57 | <[exa]> | hellwolf: oh hvm is the thing with the "MAGIC" wannabe meme in the main readme |
| 12:45:26 | <[exa]> | turns out I already classified it as such like 2 years ago :D |
| 12:51:52 | × | euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 12:53:02 | → | euleritian joins (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 12:53:09 | × | aljazmc quits (~aljazmc@user/aljazmc) (Quit: Leaving) |
| 12:55:30 | × | euleritian quits (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 12:55:48 | → | euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 12:56:11 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 12:57:27 | <[exa]> | well screw it, I guess I'll do an A* and blame the heuristics. :D |
| 12:58:51 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 12:59:44 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 13:02:29 | <haskellbridge> | <hellwolf> data AThing a = DoSomethingWith a Person | ScamWith a Person |
| 13:06:47 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 13:11:40 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 13:12:09 | → | j1n37 joins (~j1n37@user/j1n37) |
| 13:14:59 | AlexZenon_2 | is now known as AlexZenon |
| 13:19:18 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 13:22:42 | × | sabathan2 quits (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 13:24:07 | × | TimWolla quits (~timwolla@2a01:4f8:150:6153:beef::6667) (Quit: Bye) |
| 13:26:26 | → | sabathan2 joins (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 13:28:54 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 13:29:11 | → | j1n37 joins (~j1n37@user/j1n37) |
| 13:29:59 | × | la1n2 quits (~la1n@81.222.176.125) (Read error: Connection reset by peer) |
| 13:30:02 | → | TimWolla joins (~timwolla@2a01:4f8:150:6153:beef::6667) |
| 13:31:49 | → | weary-traveler joins (~user@user/user363627) |
| 13:35:56 | → | la1n joins (~la1n@85.249.17.224) |
| 13:40:27 | → | la1n2 joins (~la1n@176.59.41.59) |
| 13:40:46 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 268 seconds) |
| 13:42:49 | × | la1n quits (~la1n@85.249.17.224) (Ping timeout: 244 seconds) |
| 13:51:13 | → | tabaqui joins (~tabaqui@167.71.80.236) |
| 14:22:48 | × | target_i quits (~target_i@user/target-i/x-6023099) (Ping timeout: 252 seconds) |
| 14:22:59 | → | haritz joins (~hrtz@152.37.68.178) |
| 14:22:59 | × | haritz quits (~hrtz@152.37.68.178) (Changing host) |
| 14:22:59 | → | haritz joins (~hrtz@user/haritz) |
| 14:23:04 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 14:23:10 | × | m1dnight quits (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 14:25:09 | → | m1dnight joins (~m1dnight@d8D861908.access.telenet.be) |
| 14:25:22 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 252 seconds) |
| 14:32:21 | → | euphores joins (~SASL_euph@user/euphores) |
| 14:38:56 | × | tromp quits (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 14:50:18 | × | m1dnight quits (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 14:52:27 | → | m1dnight joins (~m1dnight@d8D861908.access.telenet.be) |
| 14:53:05 | × | euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 14:54:06 | → | euleritian joins (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 14:56:17 | × | typedfern_ quits (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 248 seconds) |
| 14:56:42 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 14:56:56 | → | Typedfern joins (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 15:04:03 | × | noctuks quits (MR7CNKXm0J@user/noctux) (Quit: WeeChat 4.5.1) |
| 15:04:04 | × | yushyin quits (qjh7DQNxXf@mail.karif.server-speed.net) (Quit: WeeChat 4.5.1) |
| 15:04:04 | × | s4msung quits (HpS7xJgsJj@user/s4msung) (Quit: s4msung) |
| 15:04:24 | → | tromp joins (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 15:04:40 | → | noctuks joins (d32f0pjuYL@user/noctux) |
| 15:04:44 | → | s4msung joins (K4xiEoBBTh@user/s4msung) |
| 15:04:44 | → | yushyin joins (zv27G51Tbg@mail.karif.server-speed.net) |
| 15:04:54 | <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)”? |
| 15:06:30 | × | Typedfern quits (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 268 seconds) |
| 15:08:52 | → | Typedfern joins (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 15:11:34 | × | m1dnight quits (~m1dnight@d8D861908.access.telenet.be) (Ping timeout: 252 seconds) |
| 15:12:42 | → | CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) |
| 15:16:27 | → | m1dnight joins (~m1dnight@d8D861908.access.telenet.be) |
| 15:28:00 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 15:30:01 | <[exa]> | Pozyomka: not really but maybe it would be redundant with other functions there? |
| 15:39:08 | × | hiecaq quits (~hiecaq@user/hiecaq) (Quit: ERC 5.6.0.30.1 (IRC client for GNU Emacs 30.0.92)) |
| 15:43:50 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds) |
| 15:44:03 | <[exa]> | ok well probably not the case, the internal "single-lookup adjust" in the package doesn't seem to support passing the functors through |
| 15:44:23 | → | j1n37 joins (~j1n37@user/j1n37) |
| 15:44:37 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 15:45:40 | × | sajenim quits (~sajenim@user/sajenim) (Ping timeout: 252 seconds) |
| 15:50:53 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 15:55:15 | <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. |
| 15:56:07 | <int-e> | :t Data.Map.adjustF |
| 15:56:08 | <lambdabot> | error: |
| 15:56:09 | <lambdabot> | Not in scope: ‘Data.Map.adjustF’ |
| 15:56:09 | <lambdabot> | Perhaps you meant one of these: |
| 15:56:31 | <int-e> | :t Data.Map.alterF |
| 15:56:32 | <lambdabot> | (Functor f, Ord k) => (Maybe a -> f (Maybe a)) -> k -> M.Map k a -> f (M.Map k a) |
| 15:58:50 | <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.) |
| 16:05:36 | → | alecs joins (~alecs@61.pool85-58-154.dynamic.orange.es) |
| 16:11:08 | <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!” |
| 16:16:34 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 16:18:42 | × | CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 276 seconds) |
| 16:19:23 | <Pozyomka> | int-e: “pretty heavy machinery” -- Are zippers heavy machinery now? |
| 16:20:50 | → | j1n37 joins (~j1n37@user/j1n37) |
| 16:25:23 | <int-e> | Pozyomka: there's no zipper |
| 16:25:44 | <int-e> | it remembers a path in a bit mask |
| 16:26:21 | <Pozyomka> | Wow, that's just... bonkers. |
| 16:26:36 | <int-e> | and as far as I can tell, that was introduced just for the benefit of alterF |
| 16:27:03 | <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 |
| 16:27:58 | <Pozyomka> | Wow, and there's magical constants in the code too... |
| 16:29:13 | <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 |
| 16:35:22 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 16:38:33 | <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 |
| 16:39:47 | × | euleritian quits (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 16:40:05 | → | euleritian joins (~euleritia@77.23.248.47) |
| 16:41:39 | × | euleritian quits (~euleritia@77.23.248.47) (Read error: Connection reset by peer) |
| 16:42:12 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 264 seconds) |
| 16:42:19 | → | euleritian joins (~euleritia@77.23.248.47) |
| 16:42:23 | → | __jmcantrell__ joins (~weechat@user/jmcantrell) |
| 16:43:44 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 16:46:44 | → | euphores joins (~SASL_euph@user/euphores) |
| 16:55:19 | → | Arpad joins (~Arpad@2a02:ab88:38d:4700::b0d5) |
| 16:56:03 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 16:57:29 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 268 seconds) |
| 16:58:01 | → | Guest70 joins (~Guest80@82.153.135.43) |
| 16:58:47 | × | ttybitnik quits (~ttybitnik@user/wolper) (Remote host closed the connection) |
| 16:59:31 | × | Guest70 quits (~Guest80@82.153.135.43) (Client Quit) |
| 17:00:52 | → | ystael joins (~ystael@user/ystael) |
| 17:03:28 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 17:03:45 | × | acidjnk_new3 quits (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 17:04:00 | <hellwolf> | | Couldn't match type ‘BOOL’ with ‘(BOOL, b10)’ |
| 17:04:00 | <hellwolf> | I always have trouble reading this sentence: Which one was expected, and which one was actual? |
| 17:05:39 | × | euleritian quits (~euleritia@77.23.248.47) (Ping timeout: 244 seconds) |
| 17:06:06 | → | euleritian joins (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) |
| 17:06:27 | <int-e> | > let b = (b,b) in () |
| 17:06:29 | <lambdabot> | error: |
| 17:06:29 | <lambdabot> | • Occurs check: cannot construct the infinite type: a ~ (a, b) |
| 17:06:29 | <lambdabot> | • In the expression: b |
| 17:06:41 | <int-e> | ah no |
| 17:06:47 | × | euleritian quits (~euleritia@dynamic-176-006-131-173.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:06:59 | <int-e> | > let False = () in () |
| 17:07:00 | <lambdabot> | error: |
| 17:07:00 | <lambdabot> | • Couldn't match expected type ‘Bool’ with actual type ‘()’ |
| 17:07:00 | <lambdabot> | • In the expression: () |
| 17:07:05 | → | euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 17:07:20 | <hellwolf> | since when |
| 17:07:37 | <hellwolf> | actually, sometimes I see the "expected" and "actual" words, sometimes I don't. |
| 17:08:06 | × | tromp quits (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 17:08:10 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 17:09:46 | → | tromp joins (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) |
| 17:11:39 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 17:12:55 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 17:15:27 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 17:18:40 | <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. |
| 17:21:08 | <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. |
| 17:21:25 | <hellwolf> | *few more words |
| 17:21:31 | <int-e> | *decipher |
| 17:21:35 | <hellwolf> | :p |
| 17:23:33 | <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. |
| 17:24:03 | <int-e> | IME it does a good job of giving you all the relevant info though the result can be overwhelming. |
| 17:25:40 | <hellwolf> | a good job of being verbose, indeed |
| 17:26:36 | <int-e> | if it's too much you can usually help the compiler and yourself with extra type signatures |
| 17:27:01 | <int-e> | this may break down if you're heavily into type families and other type-level programming |
| 17:28:45 | <hellwolf> | I have learned that, and started to save those intermediate steps in the comments. |
| 17:29:17 | <hellwolf> | I do prefer the completely indecipherable code in the end without type signature. But the comments stay there. |
| 17:29:44 | <hellwolf> | and this time I listened to the Emacs's word correction advice. |
| 17:31:02 | <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. |
| 17:31:21 | <Pozyomka> | But then, I don't go crazy with type-level programming. Because why would I torture myself that way? |
| 17:32:49 | <tomsmeding> | hellwolf: I think GHC is pretty consistent in giving expected/actual full types if there are any such that make sense |
| 17:33:13 | <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) |
| 17:33:34 | <tomsmeding> | if there are no such full types, there isn't necessarily any "expected" or "actual" type |
| 17:34:51 | <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 |
| 17:35:19 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 17:35:46 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 17:36:23 | <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, |
| 17:36:25 | <tomsmeding> | sometimes. |
| 17:36:58 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:37:39 | <Pozyomka> | The type errors are the most unhelpful when you're trying to be too clever. |
| 17:40:53 | → | j1n37 joins (~j1n37@user/j1n37) |
| 17:40:57 | <tomsmeding> | or trying to do too much theorem proving |
| 17:42:23 | <Pozyomka> | Theorem proving is meant to be done with pen, paper and waste basket anyway. Not with a programming language. |
| 17:42:47 | <tomsmeding> | there's a rather large set of people that like to use computers to check their work with automated theorem proving |
| 17:43:01 | <tomsmeding> | it's not as suited for all kinds of proofs :) |
| 17:46:48 | <monochrom> | Hugs has better error messages. |
| 17:47:33 | <hellwolf> | if one is motivated enough by the end goal, these are just minor obstacles :) |
| 17:47:51 | <int-e> | Hugs has a simpler type system |
| 17:48:53 | <monochrom> | Yes, it's why. |
| 17:49:08 | <monochrom> | Moreover, the other pasture is always greener. :) |
| 17:52:58 | → | Googulator33 joins (~Googulato@2a01-036d-0106-4a24-1dc7-297e-fae3-e794.pool6.digikabel.hu) |
| 17:53:55 | <monochrom> | At some point we just have to say what Stroustrup said. People complain about GHC because it is actually used. |
| 17:54:50 | <hellwolf> | continuing along your interesting analogy, is it a "grass hopper" a suitable way to describe people jumping languages. |
| 17:55:04 | <hellwolf> | Sure, Stroustrup said. |
| 17:55:37 | <int-e> | Let me guess: There's two kinds of languages, those that everybody complains about and those that nobody uses. |
| 17:55:55 | <geekosaur> | sounds about right |
| 17:56:27 | <monochrom> | Rear Admiral Grass Hopper would like you to jump to COBOL. >:) |
| 17:56:30 | × | Googulator77 quits (~Googulato@2a01-036d-0106-4a24-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Ping timeout: 240 seconds) |
| 17:56:40 | <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. |
| 17:57:27 | geekosaur | already did his time there, tyvm |
| 17:57:29 | <hellwolf> | Mount my COBOL, fumble thy registers? |
| 17:57:46 | × | Arpad quits (~Arpad@2a02:ab88:38d:4700::b0d5) (Quit: Client closed) |
| 18:12:22 | × | mceresa quits (~mceresa@user/mceresa) (Ping timeout: 276 seconds) |
| 18:15:51 | → | __monty__ joins (~toonn@user/toonn) |
| 18:18:15 | → | mceresa joins (~mceresa@user/mceresa) |
| 18:25:38 | <mauke> | I like ghc's error messages better than hugs's |
| 18:33:02 | <[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 |
| 18:35:09 | <[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. |
| 18:37:18 | <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. |
| 18:38:23 | <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. |
| 18:47:13 | <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. |
| 18:48:56 | <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 |
| 18:49:20 | <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. |
| 18:49:58 | <monochrom> | Or, TL;DR: "Patches welcome". |
| 18:51:11 | <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... |
| 18:51:23 | <EvanR> | noted. Ignoring social facts now |
| 18:51:32 | → | acidjnk_new3 joins (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) |
| 18:56:43 | <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. |
| 18:57:12 | <int-e> | :t let adjustF f i s = (\x -> Seq.update i x s) <$> f (Seq.index s i) in adjustF |
| 18:57:13 | <lambdabot> | Functor f => (t -> f t) -> Int -> Seq.Seq t -> f (Seq.Seq t) |
| 18:57:23 | <monochrom> | Unified: There is 1 kind of library: n people use the library and n people complain about it. >:) |
| 18:58:23 | <int-e> | (I'm still unconvinced that you can get a meaningful speedup over this naive implementation.) |
| 19:00:02 | × | caconym7 quits (~caconym@user/caconym) (Quit: bye) |
| 19:00:18 | <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) |
| 19:00:43 | → | caconym7 joins (~caconym@user/caconym) |
| 19:04:26 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 19:07:38 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 19:07:38 | ljdarj1 | is now known as ljdarj |
| 19:12:06 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 19:12:20 | → | califax joins (~califax@user/califx) |
| 19:18:44 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 245 seconds) |
| 19:25:07 | <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? |
| 19:25:45 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 19:30:34 | <haskellbridge> | <sm> a cabal script does that I think |
| 19:31:14 | → | pavonia joins (~user@user/siracusa) |
| 19:31:33 | <monochrom> | `cabal run` can run it, but it compiles first. Is that acceptable? |
| 19:32:53 | <geekosaur> | @sm, these days (since cabal 3.8) scripts are compiled, just like stack does |
| 19:33:53 | <haskellbridge> | <sm> 👀 |
| 19:33:56 | <[exa]> | `echo :main | cabal repl` ? >:) |
| 19:34:05 | <monochrom> | If you truly insist on interpreting, yeah cabal repl |
| 19:34:31 | <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) |
| 19:34:35 | <[exa]> | is there some kinda -c,--command option for repl? |
| 19:34:43 | <geekosaur> | --repl-options? |
| 19:34:44 | <hellwolf> | no, not acceptable because it litters: |
| 19:34:44 | <hellwolf> | ls ~/.cabal/script-builds/| wc -l |
| 19:34:44 | <hellwolf> | 30 |
| 19:34:57 | <hellwolf> | can I specify entry point for a "cabal repl" session to emulate that? |
| 19:35:18 | <geekosaur> | not easily, I think |
| 19:35:22 | <hellwolf> | shall I do unix way "echo main" | cabal repl? |
| 19:35:34 | <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 |
| 19:36:00 | <geekosaur> | echo :main (args, if needed) | cabal repl --repl-args Foo.hs |
| 19:36:21 | <monochrom> | Even for .cabal/packages too. |
| 19:36:21 | <geekosaur> | I don't thinlk there's a reasonable way to make runghc work for this |
| 19:36:53 | <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. |
| 19:37:01 | <hellwolf> | and it seems slower than just repl it. |
| 19:37:31 | <haskellbridge> | <sm> geekosaur I believe you, but it's not mentioned at https://cabal.readthedocs.io/en/latest/cabal-commands.html#cabal-run |
| 19:37:41 | → | Arpad joins (~Arpad@2a02:ab88:38d:4700::b0d5) |
| 19:38:04 | <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. |
| 19:38:31 | <haskellbridge> | <sm> a stack script will run interpreted by default, unless you add --compile |
| 19:38:34 | <geekosaur> | sm, it's not explicitly stated but look for "The executable is cached…" |
| 19:39:10 | <haskellbridge> | <sm> 👍️ |
| 19:40:50 | <hellwolf> | I remember that behaviour of stack, I really like |
| 19:41:06 | <hellwolf> | But my project is too big and I haven't configured stack :/ |
| 19:41:15 | <geekosaur> | might put up a cabal issue then |
| 19:41:21 | <haskellbridge> | <sm> stack is easy |
| 19:41:26 | <haskellbridge> | <sm> I guess you can't use a simple runhaskell script because you want to depend on packages |
| 19:42:13 | <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. |
| 19:42:19 | <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 |
| 19:42:45 | <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. |
| 19:43:12 | <hellwolf> | I know how to run raw ghc with --package-db... |
| 19:43:30 | <hellwolf> | maybe I should really do that, for now. |
| 19:43:36 | <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 |
| 19:43:46 | → | rvalue- joins (~rvalue@user/rvalue) |
| 19:43:58 | <tomsmeding> | hellwolf: geekosaur's suggestion of `cabal install --lib --package-env=. ...` sounds like the least-friction approach with cabal, maybe |
| 19:44:03 | <hellwolf> | sm: thanks for the tips... I am just wary of having to maintain to build system. |
| 19:44:12 | <hellwolf> | *two |
| 19:44:45 | <hellwolf> | but you said no stack.yml needed, hmm |
| 19:44:54 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 19:45:18 | <tomsmeding> | sm: can you also put `system-ghc: True` in a stack script somehow, so that it uses GHCup's GHC? |
| 19:46:03 | × | alecs quits (~alecs@61.pool85-58-154.dynamic.orange.es) (Quit: Client closed) |
| 19:46:12 | <haskellbridge> | <sm> yes, you can add the --system-ghc and --no-install-ghc flags |
| 19:48:40 | × | acidjnk_new3 quits (~acidjnk@p200300d6e71c4f524d98fe298d45bbdf.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 19:49:02 | → | acidjnk_new3 joins (~acidjnk@p200300d6e71c4f52d4f1201e65d300bb.dip0.t-ipconnect.de) |
| 19:49:11 | <hellwolf> | I tried runghc: it has one other problem, I listed some defaultr extensions in cabal file :D |
| 19:49:27 | <hellwolf> | gosh, side effect of relying on build system to list default extensions. |
| 19:50:07 | <haskellbridge> | <sm> that's why a lot of people write them in the modules |
| 19:50:30 | rvalue- | is now known as rvalue |
| 19:50:30 | <haskellbridge> | <sm> more verbosity.. but more robust |
| 19:50:37 | <hellwolf> | I learned that now. |
| 19:51:06 | <hellwolf> | though, I do have a few to list beyond GHC2024 :D |
| 19:51:15 | <haskellbridge> | <sm> though you could specify them in the script header too I expect |
| 19:51:28 | <hellwolf> | that's right |
| 19:51:35 | <hellwolf> | runghc has script header too? |
| 19:51:40 | <hellwolf> | cabal, or stack has, I know of. |
| 19:51:43 | <haskellbridge> | <sm> but if you want people to write scripts using your lib easily.. then no |
| 19:52:04 | <haskellbridge> | <sm> well a runghc shebang script could pass ghc opts to runghc |
| 19:52:57 | <haskellbridge> | <sm> though, that's a pain because it varies between linux / mac / freebsd, whether env -S is required in the shebang line |
| 19:53:32 | <haskellbridge> | <sm> plus, I think relying on hidden package environment files will suck |
| 19:54:31 | <hellwolf> | cat <<EOF |
| 19:54:31 | <hellwolf> | package-dbs: clear, global, ${cabal_package_db}, ${yolc_package_db} |
| 19:54:31 | <hellwolf> | packages: |
| 19:54:31 | <hellwolf> | $cabal_path |
| 19:54:31 | <hellwolf> | runyol.cabal |
| 19:54:32 | <hellwolf> | EOF |
| 19:54:48 | <hellwolf> | I create cabal project file and run cabal <-- what I do |
| 19:55:20 | → | Square joins (~Square@user/square) |
| 19:55:36 | <hellwolf> | now that I have that cabal project file, I just run that within a interpretation mode. |
| 19:55:45 | <hellwolf> | *I just want to |
| 19:56:48 | <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. |
| 19:56:58 | <geekosaur> | cabal exec runghc … ? |
| 19:58:08 | <hellwolf> | cabal exec runghc runyol |
| 19:58:10 | <hellwolf> | didn't work |
| 20:01:20 | <int-e> | maybe: cabal -v0 repl --repl-options="-e main" |
| 20:03:51 | <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. |
| 20:05:01 | <int-e> | runghc will probably need something like runghc -ghc-arg=-i -ghc-arg=exe Main.hs |
| 20:05:11 | <int-e> | does `cabal run` even work for the thing you're testing |
| 20:05:12 | <hellwolf> | it worked |
| 20:05:18 | <hellwolf> | hurray |
| 20:05:33 | <hellwolf> | let me see if it's faster |
| 20:05:45 | <int-e> | err, --ghc-arg= |
| 20:07:09 | <hellwolf> | from |
| 20:07:09 | <hellwolf> | runbin=$(cabal "$@" -v0 list-bin runyol) |
| 20:07:09 | <hellwolf> | "$runbin" || die |
| 20:07:11 | <hellwolf> | to: |
| 20:07:15 | <hellwolf> | cabal "$@" -v1 repl --repl-options="-e main" RunYol |
| 20:10:16 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 20:10:46 | <hellwolf> | 3 ± 2 seconds difference |
| 20:10:56 | <hellwolf> | that's added by the linking when building the binary |
| 20:11:05 | <hellwolf> | probably not worth the effort, but good to know. |
| 20:11:20 | <hellwolf> | thanks everyone. learned a new trick today. |
| 20:13:03 | × | Arpad quits (~Arpad@2a02:ab88:38d:4700::b0d5) (Quit: Client closed) |
| 20:13:48 | → | Square2 joins (~Square@user/square) |
| 20:20:19 | → | user363627 joins (~user@user/user363627) |
| 20:24:19 | × | weary-traveler quits (~user@user/user363627) (Ping timeout: 276 seconds) |
| 20:35:44 | → | szkl joins (uid110435@id-110435.uxbridge.irccloud.com) |
| 20:44:19 | × | hsw quits (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) (Read error: Connection reset by peer) |
| 20:44:26 | → | hsw_ joins (~hsw@112-104-12-126.adsl.dynamic.seed.net.tw) |
| 20:47:49 | × | emergence quits (thelounge@vm0.max-p.me) (Ping timeout: 248 seconds) |
| 20:48:05 | → | emergence joins (emergence@vm0.max-p.me) |
| 20:52:12 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 20:57:27 | → | ystael joins (~ystael@user/ystael) |
| 21:12:49 | <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... |
| 21:13:43 | <Rembane> | hellwolf: What problem would that solve for you? |
| 21:14:12 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 252 seconds) |
| 21:16:25 | <geekosaur> | @hackage dependent-map |
| 21:16:25 | <lambdabot> | https://hackage.haskell.org/package/dependent-map |
| 21:16:53 | <geekosaur> | oh, hm, not quite the same thing |
| 21:17:47 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 21:17:51 | <tomsmeding> | it sounds like exactly the same thing so far |
| 21:18:04 | <hellwolf> | I am checking, sounds the same, but need to look into it. |
| 21:18:40 | <monochrom> | There is one interpretation of the question such that dependent-map is a correct answer. :) |
| 21:19:03 | <tomsmeding> | yes, and I'm lazy, so I retain said interpretation until evidence to the contrary has been presented |
| 21:20:46 | <hellwolf> | I am probably just thinking out loud. I am still looking for a solution. I am adding the "function object" support, which requires, well, a function type "Fn a b". Both are nominal, and representationaly I would probably just store a "Int", and let the evaluator to decide what to do what that Int. |
| 21:20:46 | <hellwolf> | Typically of a Map, but a Map without value depending on "a" and "b" may require unsafeCoerce. Though, the real codegen would just store a map of Int to Code, that's easy. But the simulation of it would be an actual haskell function of a -> b; for this, without type information I end up having to unsafeCoerce? |
| 21:22:04 | tomsmeding | does not follow |
| 21:22:27 | <tomsmeding> | it's a function from a to b, but a is really Int, but it's also a map without value (?)? |
| 21:24:19 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 21:25:30 | × | Typedfern quits (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 276 seconds) |
| 21:28:11 | <hellwolf> | Yea, sorry, I lost you probably because much context is needed. Let me try again: I need to represent a function object in the DSL, the function object "a" to "b" if applied "a" will give you a b. But this is all in DSL, it has no relation with Haskell data types. So, in the evaluation of the DSL, I need to do something about the function object. In Haskell, such a function object is represented by Int (at least tha |
| 21:28:11 | <hellwolf> | t's what I plan to do now). I need to somehow Map that Int to something that evaluator can use. The codegen is an avaluator, the map will be "Map Int T.Text" however, |
| 21:28:39 | <hellwolf> | However, with the simulator, I need a "Map Int (a -> b)" which is not possible, because key is now parametraized. |
| 21:29:18 | <hellwolf> | :) probably still not easy to follow... |
| 21:30:16 | <hellwolf> | I probably just need to change how I write my simulator |
| 21:30:21 | <hellwolf> | can be solved in easier way. |
| 21:30:59 | <tomsmeding> | hellwolf: is the underlying problem here that your "variables" (?) are simply represented by integer IDs in the evaluator (very sensible), yet the values of those variables are now heterogeneously typed? |
| 21:31:15 | <tomsmeding> | where they were, by happenstance, still homogeneously typed before adding these function objects? |
| 21:32:16 | <tomsmeding> | `newtype Var a = Var Int`; and use `DMap Var Value` with `data Value a where VFun :: (a -> b) -> Value (Fn a b) ; VOther :: YourOtherValues -> Value Other` |
| 21:32:22 | <tomsmeding> | ah no |
| 21:32:43 | <tomsmeding> | `data Var a = Var (TypeSingleton a) Int`, where TypeSingleton should be a GADT that reifies the type `a` |
| 21:33:03 | <tomsmeding> | so that you can write a function `geq :: TypeSingleton a -> TypeSingleton b -> Maybe (a :~: b)` |
| 21:33:21 | <tomsmeding> | (the method in the Data.GADT.Compare.GEq type class) |
| 21:34:16 | <hellwolf> | I am still trying to articulate it better. What I can say right away is that the type constructor is fixed, I can't change "data YulCat eff a b" |
| 21:34:40 | <tomsmeding> | but you can change what internal data structures your evaluator uses, surely? |
| 21:35:15 | <hellwolf> | I show you the Eval.hs |
| 21:35:17 | <hellwolf> | one sec |
| 21:36:16 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/hs-pkgs/yul-dsl/src/YulDSL/Eval.hs Super simple. The codegen is similarly simple, but of course with a bit more text templating. |
| 21:36:59 | <hellwolf> | What I need to add here is the function object, aka. cartesian closed. But all I get is a constructor analysis on "Cat eff a b" type |
| 21:37:41 | <tomsmeding> | so here either a or b could be a `Fn c d`? |
| 21:37:48 | <EvanR> | lookup :: IndexedMap -> Key a -> Maybe a, with a bunch of guardrails around creating the keys |
| 21:38:08 | <tomsmeding> | that's essentially DMap |
| 21:38:10 | <tomsmeding> | but strange |
| 21:38:11 | <EvanR> | yeah |
| 21:38:15 | <EvanR> | same results |
| 21:39:18 | <EvanR> | and then to practically use it you'll need higher rank utilities |
| 21:39:26 | <tomsmeding> | hellwolf: where's the YulCat data type? |
| 21:39:28 | <EvanR> | since how likely is it you have exactly the right key |
| 21:39:35 | <hellwolf> | https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/hs-pkgs/yul-dsl/src/YulDSL/Core/YulCat.hs |
| 21:40:09 | <hellwolf> | I will try not use complicated solution. I think I probably can let Eval to decide the actual representation of each data type; for function object I just use haskell function to represent. |
| 21:40:12 | <tomsmeding> | okay yeah so the untyped integer references are baked into the DSL you're interpreting |
| 21:40:38 | <tomsmeding> | so strong will be pointless, because DMap allows you to _preserve_ typing, but there's no typing here to preserve in the first place |
| 21:40:48 | <tomsmeding> | the YulCat term could be horrendously ill-typed |
| 21:40:55 | <tomsmeding> | and the evaluator will have no choice but error |
| 21:40:57 | <hellwolf> | Currently Eval assumes that I can store all data type as it is in Haskell too, but for function object, I will have to create such a "a -> b" |
| 21:41:14 | <tomsmeding> | well all you're currently storing is WORD |
| 21:41:39 | → | Typedfern joins (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) |
| 21:41:46 | × | tromp quits (~textual@2001:1c00:3487:1b00:25b8:e34c:8097:c1c7) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:41:58 | <hellwolf> | yea, deadend, I won't do that for Eval. The codegen is easy though, because codegen can use Map Int T.Text to store code snippets |
| 21:42:10 | <hellwolf> | For Eval, I need to find a different strategy. |
| 21:42:27 | <tomsmeding> | I suspect you'll have no choice but to do `data Value = VWord WORD | VFun (Value -> Value)`; `newtype EvalData = MkEvalData (M.Map B32 Value)` |
| 21:42:38 | <tomsmeding> | and then you'll have to branch on what Value you get to see if it's what you expect |
| 21:42:59 | <hellwolf> | I can't, the function is created in DSL itself, I have no way to recreate that function in Hask |
| 21:43:05 | <hellwolf> | the only way to playback in Hask is through Eval. |
| 21:43:11 | <tomsmeding> | I don't fucking care lol |
| 21:43:15 | <hellwolf> | haha |
| 21:43:21 | <tomsmeding> | `data Value = VWord WORD | VFun (WhateverYourFunctionRepresentationWillBe)` |
| 21:43:38 | <hellwolf> | it will be represented in code snippets :D |
| 21:43:39 | <hellwolf> | in really |
| 21:43:41 | <hellwolf> | reality |
| 21:43:51 | <tomsmeding> | `data SomeTerm = forall a b. SomeTerm (YulCat eff a b)` ; `data Value eff = VWord WORD | VFun (SomeTerm eff)` |
| 21:44:05 | <hellwolf> | which is not very useful because I can't even run the code snippets until the external compile compiles it |
| 21:44:09 | <EvanR> | at least your codesnippets are in a more convenient form than blob of Text? At least it's a string of tokens? xD |
| 21:44:22 | <EvanR> | if not an AST |
| 21:44:33 | <tomsmeding> | perhaps `data SomeTerm = forall a b. YulO2 a b => SOmeTerm (YulCat eff a b)` |
| 21:44:45 | <hellwolf> | code snippets is basically what's generated by https://github.com/yolc-dev/yul-dsl-monorepo/blob/master/hs-pkgs/yul-dsl/src/YulDSL/CodeGens/Yul/Internal/FunctionGen.hs |
| 21:44:59 | <hellwolf> | I store the snippets and it becomes a function object |
| 21:45:07 | <EvanR> | there's always a way to convert code into a haskell function |
| 21:45:09 | <hellwolf> | I can't do that in Eval. But let it be, I think I find away. |
| 21:45:14 | <tomsmeding> | alternatively: `data Value = VWord WORD | VFun (Value -> State EvalData Value)` |
| 21:45:29 | <tomsmeding> | and create that `->` function by partially-applying `go` to the term you wish to store in the Value |
| 21:45:30 | <hellwolf> | | there's always a way to convert code into a haskell function |
| 21:45:30 | <hellwolf> | what code? This code snippets is not even Haskell... |
| 21:45:58 | <EvanR> | yes this is what higher order abstract syntax does |
| 21:46:11 | <EvanR> | functions are expressed as functions |
| 21:46:29 | <EvanR> | doesn't matter what source language |
| 21:46:45 | <EvanR> | see what tomsmeding just did |
| 21:47:13 | <hellwolf> | I am digesting |
| 21:48:31 | <tomsmeding> | if you want practice with this particular trick, do assignment 0.3 here https://utrechtuniversity.github.io/infomcpd/assignments/asg0.pdf |
| 21:48:33 | <tomsmeding> | :') |
| 21:52:22 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 21:53:19 | <tomsmeding> | apologies for being impatient for a bit there by the way, it's late here |
| 21:53:27 | <tomsmeding> | I've written this kind of code too often |
| 21:53:50 | <tomsmeding> | though usually I do have more types in the language to interpret so that there's actually something to preserve :p |
| 21:54:03 | <tomsmeding> | anyway bedtime for me o/ |
| 21:54:08 | <hellwolf> | no, that's good. I have different approach here. But I can do a similar thing. |
| 21:55:20 | <hellwolf> | YulITE :: YulCat eff a b -> YulCat eff a b -> YulCat eff a (YulCat eff BOOL b) |
| 21:55:38 | <hellwolf> | that'd be my new constructor to replace old inefficient ITE. |
| 21:55:40 | <hellwolf> | thanks for the help |
| 21:55:49 | <hellwolf> | I don't need the INT after all, if I can make this type-check |
| 21:55:53 | <hellwolf> | to be continued. |
| 21:58:10 | → | notdabs joins (~Owner@2600:1700:69cf:9000:953a:ffda:3cd1:4a35) |
| 21:58:16 | <hellwolf> | ^-- that constructor reads: give me two morphisms from a ~> b, representing two branches of the if-then-else, I will you give back a new morphism also from a (must be, otherwise doesn't compose) to another morphism (hence closed cartesian) that is BOOL ~> b |
| 21:58:30 | ← | notdabs parts (~Owner@2600:1700:69cf:9000:953a:ffda:3cd1:4a35) () |
| 21:58:34 | <hellwolf> | my old ITE didn't use cartesian closed, created duplicated coded. |
| 22:00:19 | <hellwolf> | that becomes the essence of the if-then-else control structure, the codegen will translate that to the target language code, which is rather short. |
| 22:02:43 | <hellwolf> | in contrast, my current YulITE :: YulCat eff a b -> YulCat eff a b -> YulCat eff (BOOL, a) b |
| 22:03:16 | <EvanR> | Yultide |
| 22:03:55 | <hellwolf> | the currently one doesn't compose, makes some code duplication. Anyways, perhaps too specific. |
| 22:06:31 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 22:07:10 | × | Square2 quits (~Square@user/square) (Quit: Leaving) |
| 22:07:36 | → | Square2 joins (~Square@user/square) |
| 22:08:29 | × | Square2 quits (~Square@user/square) (Client Quit) |
| 22:08:33 | × | Square quits (~Square@user/square) (Remote host closed the connection) |
| 22:18:43 | × | Typedfern quits (~Typedfern@213.red-83-37-26.dynamicip.rima-tde.net) (Ping timeout: 252 seconds) |
| 22:18:58 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 22:23:16 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 22:29:31 | × | sm quits (znc@plaintextaccounting/sm) (Quit: ZNC 1.6.6+deb1ubuntu0.2 - http://znc.in) |
| 22:31:10 | → | sm joins (znc@plaintextaccounting/sm) |
| 22:34:44 | → | hiredman joins (~hiredman@frontier1.downey.family) |
| 22:50:49 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 22:52:27 | → | jbalint joins (~jbalint@syn-071-090-119-177.res.spectrum.com) |
| 22:55:47 | → | sprotte24 joins (~sprotte24@p200300d16f243100f18c0be91bdc6e3d.dip0.t-ipconnect.de) |
| 22:58:05 | <hellwolf> | here you go, |
| 22:58:08 | <hellwolf> | YulCurry :: forall eff a b c. YulO3 a b c => YulCat eff (a ⊗ b) c -> YulCat eff a (YulCat eff b c) |
| 22:58:12 | <hellwolf> | YulSwitch :: [(B32, YulCat eff a b)] -> YulCat eff (a ⊗ B32) b |
| 22:58:17 | <hellwolf> | a curry and a switch, job done. |
| 22:59:06 | <hellwolf> | no more specialized ITE, but a switch statement, which the target langauge is using anyways. |
| 22:59:36 | <hellwolf> | YulSwitch constructs the specialized switch statement |
| 22:59:48 | <hellwolf> | and curry is general categorical operation |
| 23:00:37 | <hellwolf> | YulCurry (YulSwitch [(True, ..), (False, ..)]) :: YulCat eff (a ⊗ BOOL) c |
| 23:01:21 | <hellwolf> | to complete, apply is: |
| 23:01:21 | <hellwolf> | YulApply :: forall eff a b. YulO2 a b => YulCat eff (YulCat eff a b ⊗ a) b |
| 23:01:24 | <hellwolf> | good night. |
| 23:15:06 | × | Googulator33 quits (~Googulato@2a01-036d-0106-4a24-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed) |
| 23:20:30 | → | sajenim joins (~sajenim@user/sajenim) |
| 23:21:16 | × | sprotte24 quits (~sprotte24@p200300d16f243100f18c0be91bdc6e3d.dip0.t-ipconnect.de) (Quit: Leaving) |
| 23:21:50 | × | tremon quits (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 23:25:10 | → | Square joins (~Square@user/square) |
| 23:28:11 | × | acidjnk_new3 quits (~acidjnk@p200300d6e71c4f52d4f1201e65d300bb.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 23:34:04 | × | smalltalkman quits (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 23:37:25 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:37:35 | → | Axma14181 joins (~Axman6@user/axman6) |
| 23:39:49 | × | Axman6 quits (~Axman6@user/axman6) (Ping timeout: 250 seconds) |
| 23:40:26 | → | tolgo joins (~Thunderbi@199.115.144.130) |
| 23:40:49 | → | j1n37- joins (~j1n37@user/j1n37) |
| 23:41:38 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 23:41:41 | × | j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 265 seconds) |
| 23:43:19 | <monochrom> | onoes, is that the much fabled monad with tensor strength? |
| 23:46:02 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 23:46:02 | ljdarj1 | is now known as ljdarj |
| 23:55:21 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 23:56:54 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds) |
| 23:56:54 | ljdarj1 | is now known as ljdarj |
All times are in UTC on 2025-05-04.