IRCBrowse

2024/06/25

2024-06-25 00:07:27 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Quit: Lost terminal)
2024-06-25 00:08:42 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-25 00:09:46 +0000 <Axman6> I feel like I need to read the output of :help in ghci more often, there's so many things in there I forget exist. I didn't know :show had so many different things it could display!
2024-06-25 00:32:14 +0000henry40408(~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds))
2024-06-25 00:32:40 +0000henry40408(~henry4040@175.182.111.183)
2024-06-25 00:35:17 +0000califax(~califax@user/califx) (Remote host closed the connection)
2024-06-25 00:36:53 +0000ystael(~ystael@user/ystael) (Ping timeout: 240 seconds)
2024-06-25 00:37:09 +0000califax(~califax@user/califx)
2024-06-25 01:04:41 +0000philopsos1(~caecilius@user/philopsos) (Ping timeout: 252 seconds)
2024-06-25 01:06:16 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 246 seconds)
2024-06-25 01:17:52 +0000danse-nr3(~danse-nr3@151.37.245.96)
2024-06-25 01:20:16 +0000mrmr155334346(~mrmr@user/mrmr)
2024-06-25 01:22:09 +0000mrmr15533434(~mrmr@user/mrmr) (Ping timeout: 268 seconds)
2024-06-25 01:22:09 +0000mrmr155334346mrmr15533434
2024-06-25 01:43:50 +0000andrewboltachev(~andrey@178.141.121.180)
2024-06-25 01:44:48 +0000 <andrewboltachev> Hi. Could one make cata (cataM in my case https://github.com/andrewboltachev/matcher/blob/match_let/src/Logicore/Matcher/Core.hs#L1468 ) to first "visit" parent nodes then leafs, so that StateT could have worked correctly?
2024-06-25 01:53:03 +0000danse-nr3(~danse-nr3@151.37.245.96) (Ping timeout: 264 seconds)
2024-06-25 02:05:36 +0000 <monochrom> I was thinking of asking "where can I read the definition of cataM" but realistically I will not read it anyway so I won't actually ask that. What I can say though is when I wrote my own expression ADT and traversers, I wrote both a parent-before-child one and a child-before-parent one, precisely because both are necessary.
2024-06-25 02:05:53 +0000 <c_wraith> monochrom: it's around line 120 of that file
2024-06-25 02:09:36 +0000 <andrewboltachev> In fact original definition is here: https://github.com/recursion-schemes/recursion-schemes/issues/3#issuecomment-377856187
2024-06-25 02:10:11 +0000 <monochrom> I don't use recursion-schemes.
2024-06-25 02:10:32 +0000 <monochrom> I use neither recursion-schemes nor the other one that provides Control.Monad.Loop
2024-06-25 02:11:20 +0000 <andrewboltachev> ah, that imperative-like stuff
2024-06-25 02:11:26 +0000 <andrewboltachev> also forM_ etc
2024-06-25 02:11:50 +0000 <andrewboltachev> that's what ChatGPT (ollama code) generated me when I asked for some Haskell
2024-06-25 02:12:16 +0000 <monochrom> I use forM_. That is not contrived at all.
2024-06-25 02:12:28 +0000 <andrewboltachev> monochrom: do you find recursion-schemes limiting?
2024-06-25 02:12:30 +0000 <c_wraith> It seems like cataA is easier to use than cataM anyway.
2024-06-25 02:12:57 +0000 <c_wraith> But more importantly, since it gives you effect blobs individually, you can order them however you want
2024-06-25 02:13:23 +0000 <andrewboltachev> c_wraith: I have hard time extracting the value from cataA's argument, like: MatchResultF (MatchStatusT (KeyMap Value) m1 Value) -> MatchResultF Value
2024-06-25 02:13:25 +0000 <monochrom> No, the opposite, too many things I don't need. I need at most cata and ana. Not worth bringing in the whole package.
2024-06-25 02:13:49 +0000ubert(~Thunderbi@p200300ecdf49174f0b4465dc752c7466.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
2024-06-25 02:14:07 +0000 <andrewboltachev> c_wraith: yes I believe so. but how is it easier?
2024-06-25 02:14:36 +0000 <monochrom> I can confess that when I learned free monads, first thing I did was to write the catamorphism of the Free type. That still doesn't mean I should care about recursion-schemes.
2024-06-25 02:15:02 +0000 <andrewboltachev> ah. I understand Cofree Comonad, but not a free monad still :/
2024-06-25 02:16:23 +0000 <monochrom> And I have needed anamorphisms so sparingly, the only one I have ever used is [a]'s unfoldr. (But it's very pleasant when I need it.)
2024-06-25 02:16:45 +0000 <c_wraith> you think unfoldr is "very pleasant"?
2024-06-25 02:17:00 +0000 <monochrom> Yes.
2024-06-25 02:17:15 +0000 <c_wraith> Maybe (a, b) has about the worst possible ergonomics for what it does
2024-06-25 02:17:21 +0000 <monochrom> Or rather, yes under the conditions of my use cases.
2024-06-25 02:17:41 +0000 <c_wraith> bizarrely, it also has performance problems I can't understand when it doesn't fully fuse away
2024-06-25 02:18:30 +0000 <andrewboltachev> I've recently had a simple line like acc <- acc', which was a duplicate of another one. Then amount of calculation grown exponentially
2024-06-25 02:18:33 +0000ubert(~Thunderbi@p200300ecdf32ea35d7e32474cc4feedf.dip0.t-ipconnect.de)
2024-06-25 02:19:07 +0000 <monochrom> This thread contains both your view and the opposite view: https://discourse.haskell.org/t/equivalence-of-unfoldr-and-unfold/9657
2024-06-25 02:20:42 +0000 <c_wraith> Ugh, no. Not unfold type either. That's an *incredibly* verbose way of avoiding Church encoding. I'd much rather just do the Church encoding.
2024-06-25 02:20:51 +0000 <monochrom> Oh yeah I tease my students with "why is this exp-time? f(n) = f(n-1) + f(n-1)"
2024-06-25 02:24:16 +0000 <monochrom> What is the ergonomic version you have in mind?
2024-06-25 02:24:38 +0000 <c_wraith> Church encode it. (forall r. (a -> b -> r) -> r -> b -> r) -> b -> [a]
2024-06-25 02:28:10 +0000xff0x(~xff0x@2405:6580:b080:900:dc9b:52bd:4c0c:b888) (Ping timeout: 246 seconds)
2024-06-25 02:30:03 +0000 <andrewboltachev> UPD: solved my issue with using paraM :/ (to modify as little code as I can): https://github.com/andrewboltachev/matcher/blob/match_let/src/Logicore/Matcher/Core.hs#L1468
2024-06-25 02:30:26 +0000 <andrewboltachev> this also allowed to change the order of effects
2024-06-25 02:38:32 +0000henry40408(~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds))
2024-06-25 02:39:01 +0000henry40408(~henry4040@175.182.111.183)
2024-06-25 02:41:18 +0000edrx(~Eduardo@170-233-51-85.static.sumicity.net.br)
2024-06-25 02:43:57 +0000 <edrx> hi all! is there a way to make ghci print the types with the foralls?
2024-06-25 02:44:00 +0000 <edrx> for example:
2024-06-25 02:44:01 +0000 <edrx> ghci> :t \ (a,b) -> a
2024-06-25 02:44:02 +0000 <edrx> \ (a,b) -> a :: (a, b) -> a
2024-06-25 02:44:29 +0000 <edrx> I'm looking for something like
2024-06-25 02:44:30 +0000terrorjack(~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat)
2024-06-25 02:44:41 +0000 <geekosaur> :set -print-explicit-foralls
2024-06-25 02:44:44 +0000 <edrx> \ (a,b) -> a :: Forall a b. (a, b) -> a
2024-06-25 02:45:22 +0000 <edrx> ghci> :set -print-explicit-foralls
2024-06-25 02:45:22 +0000 <edrx> Some flags have not been recognized: -print-explicit-foralls
2024-06-25 02:45:32 +0000 <geekosaur> sorry, just noticed I typoed that
2024-06-25 02:45:35 +0000 <geekosaur> :set -fprint-explicit-foralls
2024-06-25 02:46:01 +0000 <edrx> fantastic! thanks =)
2024-06-25 02:47:23 +0000terrorjack(~terrorjac@2a01:4f8:c17:87f8::)
2024-06-25 02:50:26 +0000td_(~td@i5387092F.versanet.de) (Ping timeout: 256 seconds)
2024-06-25 02:50:35 +0000Leary(~Leary@user/Leary/x-0910699)
2024-06-25 02:51:26 +0000edrx(~Eduardo@170-233-51-85.static.sumicity.net.br) (Killed buffer)
2024-06-25 02:51:44 +0000andrewboltachev(~andrey@178.141.121.180) (Quit: Leaving.)
2024-06-25 02:52:21 +0000td_(~td@i53870933.versanet.de)
2024-06-25 03:13:46 +0000zzz(~yin@user/zero) (Ping timeout: 268 seconds)
2024-06-25 03:15:45 +0000zzz(~yin@user/zero)
2024-06-25 03:26:01 +0000danse-nr3(~danse-nr3@151.37.245.96)
2024-06-25 03:27:48 +0000philopsos1(~caecilius@user/philopsos)
2024-06-25 03:28:34 +0000zzz(~yin@user/zero) (Ping timeout: 268 seconds)
2024-06-25 03:33:19 +0000xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-25 03:34:30 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751)
2024-06-25 03:34:53 +0000danse-nr3(~danse-nr3@151.37.245.96) (Read error: Connection reset by peer)
2024-06-25 03:34:58 +0000zzz(~yin@user/zero)
2024-06-25 03:35:03 +0000danse-nr3(~danse-nr3@151.37.247.173)
2024-06-25 03:35:03 +0000waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds)
2024-06-25 03:38:38 +0000aforemny(~aforemny@2001:9e8:6cdd:b100:c11c:c2a2:7e21:6fd9)
2024-06-25 03:39:08 +0000wbooze(~wbooze@2a02:908:1244:9a20:b9d0:f0c5:81d6:5db5) (Remote host closed the connection)
2024-06-25 03:40:17 +0000aforemny_(~aforemny@2001:9e8:6cf7:eb00:b3e4:61be:b332:f613) (Ping timeout: 268 seconds)
2024-06-25 03:51:14 +0000krasjet(~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
2024-06-25 03:51:38 +0000krjst(~krjst@2604:a880:800:c1::16b:8001)
2024-06-25 04:01:46 +0000wootehfoot(~wootehfoo@user/wootehfoot)
2024-06-25 04:06:30 +0000xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds)
2024-06-25 04:06:51 +0000wootehfoot(~wootehfoo@user/wootehfoot) (Ping timeout: 264 seconds)
2024-06-25 04:08:06 +0000xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-25 04:17:42 +0000madhavanmiui(~madhavanm@2409:40f4:1a:fff3:8000::)
2024-06-25 04:19:40 +0000madhavanmiui(~madhavanm@2409:40f4:1a:fff3:8000::) (Client Quit)
2024-06-25 04:24:01 +0000pavonia(~user@user/siracusa) (Quit: Bye!)
2024-06-25 04:26:49 +0000zzz(~yin@user/zero) (Ping timeout: 246 seconds)
2024-06-25 04:33:10 +0000takuan(~takuan@178-116-218-225.access.telenet.be)
2024-06-25 04:46:46 +0000aaronv(~aaronv@user/aaronv)
2024-06-25 04:50:08 +0000danse-nr3(~danse-nr3@151.37.247.173) (Remote host closed the connection)
2024-06-25 04:50:33 +0000danse-nr3(~danse-nr3@151.37.247.173)
2024-06-25 05:02:18 +0000tabemann__(~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Remote host closed the connection)
2024-06-25 05:03:07 +0000CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-06-25 05:03:14 +0000tabemann__(~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net)
2024-06-25 05:05:37 +0000CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
2024-06-25 05:09:32 +0000wbooze(~wbooze@2a02:908:1244:9a20:570c:a8cf:25a8:c6db)
2024-06-25 05:12:59 +0000 <danse-nr3> huh looks like the foundation has bought serokell's certifications
2024-06-25 05:15:49 +0000ubert1(~Thunderbi@p200300ecdf32eac70fea81216be0fe50.dip0.t-ipconnect.de)
2024-06-25 05:15:51 +0000ubert(~Thunderbi@p200300ecdf32ea35d7e32474cc4feedf.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
2024-06-25 05:15:51 +0000ubert1ubert
2024-06-25 05:27:01 +0000aaronv(~aaronv@user/aaronv) (Ping timeout: 246 seconds)
2024-06-25 05:29:29 +0000ec(~ec@gateway/tor-sasl/ec) (Remote host closed the connection)
2024-06-25 05:31:11 +0000euleritian(~euleritia@dynamic-176-007-161-051.176.7.pool.telefonica.de) (Ping timeout: 264 seconds)
2024-06-25 05:31:49 +0000euleritian(~euleritia@dynamic-176-007-195-192.176.7.pool.telefonica.de)
2024-06-25 05:32:30 +0000aaronv(~aaronv@user/aaronv)
2024-06-25 05:37:31 +0000danse-nr3(~danse-nr3@151.37.247.173) (Ping timeout: 246 seconds)
2024-06-25 05:44:10 +0000philopsos1(~caecilius@user/philopsos) (Ping timeout: 246 seconds)
2024-06-25 06:00:12 +0000philopsos1(~caecilius@user/philopsos)
2024-06-25 06:00:31 +0000 <haskellbridge> <maerwald> Bought?
2024-06-25 06:00:50 +0000euleritian(~euleritia@dynamic-176-007-195-192.176.7.pool.telefonica.de) (Ping timeout: 256 seconds)
2024-06-25 06:05:42 +0000Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-06-25 06:06:13 +0000 <haskellbridge> <magic_rb> Huh? I used to be employed by serokell so im curious
2024-06-25 06:06:25 +0000 <haskellbridge> <maerwald> It was donated
2024-06-25 06:07:08 +0000MrFox(~MrFox___@89-201-184-155.dsl.optinet.hr)
2024-06-25 06:07:27 +0000 <haskellbridge> <magic_rb> Oh cool
2024-06-25 06:17:14 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751) (Ping timeout: 268 seconds)
2024-06-25 06:18:53 +0000acidjnk_new3(~acidjnk@p200300d6e714dc90fd0a56c96235233a.dip0.t-ipconnect.de)
2024-06-25 06:25:50 +0000danse-nr3(~danse-nr3@151.37.247.173)
2024-06-25 06:26:42 +0000danse-nr3(~danse-nr3@151.37.247.173) (Remote host closed the connection)
2024-06-25 06:27:07 +0000danse-nr3(~danse-nr3@151.37.247.173)
2024-06-25 06:27:30 +0000bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds)
2024-06-25 06:28:31 +0000 <danse-nr3> did not mean "bought" just as in a financial transaction. Also bought the idea
2024-06-25 06:30:03 +0000bitdex(~bitdex@gateway/tor-sasl/bitdex)
2024-06-25 06:42:49 +0000aaronv(~aaronv@user/aaronv) (Ping timeout: 268 seconds)
2024-06-25 06:45:45 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751)
2024-06-25 06:49:59 +0000lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-25 06:54:01 +0000sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-25 06:56:17 +0000CiaoSen(~Jura@2a05:5800:282:3d00:e6b9:7aff:fe80:3d03)
2024-06-25 06:59:41 +0000 <haskellbridge> <magic_rb> Ahhhh
2024-06-25 07:03:21 +0000lisbeths(uid135845@id-135845.lymington.irccloud.com)
2024-06-25 07:19:59 +0000CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-06-25 07:20:11 +0000MrFox(~MrFox___@89-201-184-155.dsl.optinet.hr) (Quit: Leaving)
2024-06-25 07:21:41 +0000ft(~ft@p3e9bcb39.dip0.t-ipconnect.de) (Quit: leaving)
2024-06-25 07:22:39 +0000CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
2024-06-25 07:23:59 +0000rvalue(~rvalue@user/rvalue) (Ping timeout: 264 seconds)
2024-06-25 07:36:59 +0000chele(~chele@user/chele)
2024-06-25 07:38:01 +0000danse-nr3(~danse-nr3@151.37.247.173) (Ping timeout: 268 seconds)
2024-06-25 07:38:16 +0000danse-nr3(~danse-nr3@151.43.174.90)
2024-06-25 07:43:55 +0000danse-nr3(~danse-nr3@151.43.174.90) (Ping timeout: 260 seconds)
2024-06-25 07:48:51 +0000cfricke(~cfricke@user/cfricke)
2024-06-25 07:58:32 +0000gmg(~user@user/gehmehgeh)
2024-06-25 07:59:14 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-25 08:05:59 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751) (Quit: Leaving.)
2024-06-25 08:06:08 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 08:07:00 +0000econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-25 08:11:16 +0000rvalue(~rvalue@user/rvalue)
2024-06-25 08:18:43 +0000FragByte(~christian@user/fragbyte)
2024-06-25 08:18:59 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 08:23:40 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751)
2024-06-25 08:23:57 +0000CiaoSen(~Jura@2a05:5800:282:3d00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds)
2024-06-25 08:23:57 +0000FragByte(~christian@user/fragbyte) (Ping timeout: 268 seconds)
2024-06-25 08:27:07 +0000FragByte(~christian@user/fragbyte)
2024-06-25 08:27:11 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751) (Client Quit)
2024-06-25 08:28:12 +0000lxsameer(~lxsameer@Serene/lxsameer)
2024-06-25 08:32:06 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 08:34:42 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751)
2024-06-25 08:45:14 +0000cfricke(~cfricke@user/cfricke) (Remote host closed the connection)
2024-06-25 08:45:31 +0000cfricke(~cfricke@user/cfricke)
2024-06-25 08:47:00 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 08:47:55 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751) (Ping timeout: 246 seconds)
2024-06-25 08:48:39 +0000philopsos1(~caecilius@user/philopsos) (Ping timeout: 256 seconds)
2024-06-25 08:53:06 +0000bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds)
2024-06-25 08:53:55 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 08:55:20 +0000bitdex(~bitdex@gateway/tor-sasl/bitdex)
2024-06-25 08:55:35 +0000CiaoSen(~Jura@2a05:5800:282:3d00:e6b9:7aff:fe80:3d03)
2024-06-25 08:59:28 +0000dcoutts(~duncan@2a00:23c6:1c8d:901:b94:4566:9d63:4848)
2024-06-25 09:03:15 +0000danse-nr3(~danse-nr3@151.43.174.90)
2024-06-25 09:04:37 +0000xff0x_(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-25 09:06:05 +0000xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 256 seconds)
2024-06-25 09:06:30 +0000CiaoSen(~Jura@2a05:5800:282:3d00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds)
2024-06-25 09:07:25 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 09:08:58 +0000chexum(~quassel@gateway/tor-sasl/chexum) (Ping timeout: 260 seconds)
2024-06-25 09:13:26 +0000chexum(~quassel@gateway/tor-sasl/chexum)
2024-06-25 09:22:55 +0000lisbeths(uid135845@id-135845.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-25 09:27:28 +0000soverysour(~soverysou@81.196.150.219)
2024-06-25 09:27:28 +0000soverysour(~soverysou@81.196.150.219) (Changing host)
2024-06-25 09:27:28 +0000soverysour(~soverysou@user/soverysour)
2024-06-25 09:32:24 +0000Nixkernal(~Nixkernal@240.17.194.178.dynamic.cust.swisscom.net) (Ping timeout: 268 seconds)
2024-06-25 09:32:39 +0000Nixkernal(~Nixkernal@240.17.194.178.dynamic.cust.swisscom.net)
2024-06-25 09:41:19 +0000soverysour(~soverysou@user/soverysour) (Ping timeout: 272 seconds)
2024-06-25 09:45:03 +0000ubert(~Thunderbi@p200300ecdf32eac70fea81216be0fe50.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2024-06-25 09:47:13 +0000Nixkernal_(~Nixkernal@240.17.194.178.dynamic.cust.swisscom.net)
2024-06-25 09:48:55 +0000Nixkernal(~Nixkernal@240.17.194.178.dynamic.cust.swisscom.net) (Ping timeout: 272 seconds)
2024-06-25 09:49:47 +0000__monty__(~toonn@user/toonn)
2024-06-25 09:51:25 +0000lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-06-25 09:53:59 +0000Nixkernal_(~Nixkernal@240.17.194.178.dynamic.cust.swisscom.net) (Ping timeout: 264 seconds)
2024-06-25 09:54:30 +0000ubert(~Thunderbi@2a02:8109:ab8a:5a00:fafc:98d0:fb97:e3fd)
2024-06-25 10:09:11 +0000xff0x_(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds)
2024-06-25 10:22:42 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 10:25:57 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751)
2024-06-25 10:41:48 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Quit: Lost terminal)
2024-06-25 10:42:50 +0000czy(~user@fortigate.wolfson.cam.ac.uk)
2024-06-25 10:42:57 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-25 10:43:19 +0000sawilagar(~sawilagar@user/sawilagar)
2024-06-25 10:50:08 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer)
2024-06-25 10:50:51 +0000lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-25 10:58:28 +0000danse-nr3(~danse-nr3@151.43.174.90) (Remote host closed the connection)
2024-06-25 10:58:53 +0000danse-nr3(~danse-nr3@151.43.174.90)
2024-06-25 10:59:13 +0000madhavanmiui(~madhavanm@2409:40f4:15:fe92:8000::)
2024-06-25 11:00:33 +0000madhavanmiui(~madhavanm@2409:40f4:15:fe92:8000::) (Client Quit)
2024-06-25 11:10:46 +0000xff0x(~xff0x@ai068022.d.east.v6connect.net)
2024-06-25 11:10:58 +0000smalltalkman(uid545680@id-545680.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:10:58 +0000hamishmack(sid389057@id-389057.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:10:58 +0000Kamuela(sid111576@id-111576.tinside.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:10:58 +0000lexi-lambda(sid92601@id-92601.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:11:03 +0000ProofTechnique_(sid79547@id-79547.ilkley.irccloud.com) (Ping timeout: 264 seconds)
2024-06-25 11:11:15 +0000NiKaN(sid385034@id-385034.helmsley.irccloud.com) (Ping timeout: 272 seconds)
2024-06-25 11:11:19 +0000sa(sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:24 +0000degraafk(sid71464@id-71464.lymington.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:11:25 +0000sclv(sid39734@haskell/developer/sclv) (Ping timeout: 246 seconds)
2024-06-25 11:11:25 +0000Fangs(sid141280@id-141280.hampstead.irccloud.com) (Ping timeout: 246 seconds)
2024-06-25 11:11:25 +0000T_S_____(sid501726@id-501726.uxbridge.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:11:25 +0000SanchayanMaity(sid478177@id-478177.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:11:25 +0000haasn(sid579015@id-579015.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:11:27 +0000hook54321(sid149355@user/hook54321) (Ping timeout: 256 seconds)
2024-06-25 11:11:27 +0000snek(sid280155@id-280155.lymington.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:27 +0000shawwwn(sid6132@id-6132.helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:39 +0000aristid(sid1599@id-1599.uxbridge.irccloud.com) (Ping timeout: 264 seconds)
2024-06-25 11:11:41 +0000lally(sid388228@id-388228.uxbridge.irccloud.com) (Ping timeout: 268 seconds)
2024-06-25 11:11:41 +0000bradparker(sid262931@id-262931.uxbridge.irccloud.com) (Ping timeout: 268 seconds)
2024-06-25 11:11:41 +0000onliner10_(uid656258@user/onliner10) (Ping timeout: 240 seconds)
2024-06-25 11:11:46 +0000jackdk(sid373013@cssa/jackdk) (Ping timeout: 246 seconds)
2024-06-25 11:11:51 +0000delyan_(sid523379@id-523379.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:11:51 +0000bjs(sid190364@user/bjs) (Ping timeout: 255 seconds)
2024-06-25 11:11:51 +0000NemesisD(sid24071@id-24071.lymington.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:11:53 +0000SrPx(sid108780@id-108780.uxbridge.irccloud.com) (Ping timeout: 272 seconds)
2024-06-25 11:11:53 +0000buhman(sid411355@user/buhman) (Ping timeout: 272 seconds)
2024-06-25 11:11:53 +0000taktoa[c](sid282096@id-282096.tinside.irccloud.com) (Ping timeout: 272 seconds)
2024-06-25 11:11:53 +0000jonrh(sid5185@id-5185.ilkley.irccloud.com) (Ping timeout: 272 seconds)
2024-06-25 11:11:53 +0000Pent(sid313808@id-313808.lymington.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:53 +0000edwardk(sid47016@haskell/developer/edwardk) (Ping timeout: 256 seconds)
2024-06-25 11:11:53 +0000carter_(sid14827@id-14827.helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:56 +0000alinab(sid468903@id-468903.helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:56 +0000edmundnoble_(sid229620@id-229620.helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:56 +0000edm(sid147314@id-147314.hampstead.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:11:56 +0000iphy(sid67735@user/iphy) (Ping timeout: 256 seconds)
2024-06-25 11:12:07 +0000SethTisue(sid14912@id-14912.ilkley.irccloud.com) (Ping timeout: 246 seconds)
2024-06-25 11:12:18 +0000mustafa(sid502723@rockylinux/releng/mustafa) (Ping timeout: 255 seconds)
2024-06-25 11:12:18 +0000Boarders_____(sid425905@id-425905.lymington.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:19 +0000jakesyl_____(sid56879@id-56879.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:19 +0000caasih(sid13241@id-13241.ilkley.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:27 +0000alanz(sid110616@id-110616.uxbridge.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:27 +0000systemfault(sid267009@about/typescript/member/systemfault) (Ping timeout: 256 seconds)
2024-06-25 11:12:27 +0000PotatoGim(sid99505@id-99505.lymington.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:30 +0000idnar(sid12240@debian/mithrandi) (Ping timeout: 256 seconds)
2024-06-25 11:12:31 +0000b20n(sid115913@id-115913.uxbridge.irccloud.com) (Ping timeout: 272 seconds)
2024-06-25 11:12:31 +0000hovsater(sid499516@user/hovsater) (Ping timeout: 272 seconds)
2024-06-25 11:12:31 +0000Techcable(sid534393@user/Techcable) (Ping timeout: 272 seconds)
2024-06-25 11:12:35 +0000amir(sid22336@user/amir) (Ping timeout: 256 seconds)
2024-06-25 11:12:35 +0000gaze__(sid387101@id-387101.helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:35 +0000davetapley(sid666@id-666.uxbridge.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:35 +0000chessai(sid225296@id-225296.lymington.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:35 +0000aspen(sid449115@id-449115.helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:35 +0000Adeon(sid418992@id-418992.lymington.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:35 +0000tritlo_(sid58727@id-58727.hampstead.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:35 +0000S11001001(sid42510@id-42510.ilkley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:12:45 +0000bw_______(sid2730@id-2730.ilkley.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:46 +0000tapas(sid467876@id-467876.ilkley.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:46 +0000gmc(sid58314@id-58314.ilkley.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:46 +0000mankyKitty(sid31287@id-31287.helmsley.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:46 +0000astra(sid289983@id-289983.hampstead.irccloud.com) (Ping timeout: 255 seconds)
2024-06-25 11:12:49 +0000JSharp(sid4580@user/JSharp) (Ping timeout: 246 seconds)
2024-06-25 11:12:53 +0000dmj`(uid72307@id-72307.hampstead.irccloud.com) (Ping timeout: 240 seconds)
2024-06-25 11:12:55 +0000rubin55(sid175221@id-175221.hampstead.irccloud.com) (Ping timeout: 268 seconds)
2024-06-25 11:12:59 +0000meinside(uid24933@id-24933.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2024-06-25 11:13:01 +0000jmct(sid160793@id-160793.tinside.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:13:02 +0000dy(sid3438@user/dy) (Ping timeout: 256 seconds)
2024-06-25 11:13:04 +0000geekosaur(sid609282@xmonad/geekosaur) (Ping timeout: 256 seconds)
2024-06-25 11:13:09 +0000sa1(sid7690@id-7690.ilkley.irccloud.com) (Ping timeout: 272 seconds)
2024-06-25 11:13:09 +0000rune_(sid21167@id-21167.ilkley.irccloud.com) (Ping timeout: 272 seconds)
2024-06-25 11:13:09 +0000evertedsphere(sid434122@id-434122.hampstead.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:13:09 +0000integral(sid296274@user/integral) (Ping timeout: 256 seconds)
2024-06-25 11:13:09 +0000cbarrett(sid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:13:09 +0000dsal(sid13060@id-13060.lymington.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:13:32 +0000tnks(sid412124@id-412124.helmsley.irccloud.com) (Ping timeout: 268 seconds)
2024-06-25 11:18:46 +0000danse-nr3(~danse-nr3@151.43.174.90) (Ping timeout: 246 seconds)
2024-06-25 11:19:32 +0000tabemann__(~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Read error: Connection reset by peer)
2024-06-25 11:21:02 +0000tabemann__(~tabemann@2600:1700:7990:24e0:a80c:5b74:1624:82db)
2024-06-25 11:21:10 +0000T_S_____(sid501726@id-501726.uxbridge.irccloud.com)
2024-06-25 11:21:18 +0000aspen(sid449115@id-449115.helmsley.irccloud.com)
2024-06-25 11:21:21 +0000hamishmack(sid389057@id-389057.hampstead.irccloud.com)
2024-06-25 11:21:23 +0000bradparker(sid262931@id-262931.uxbridge.irccloud.com)
2024-06-25 11:21:33 +0000S11001001(sid42510@id-42510.ilkley.irccloud.com)
2024-06-25 11:21:34 +0000haasn(sid579015@id-579015.hampstead.irccloud.com)
2024-06-25 11:21:39 +0000evertedsphere(sid434122@id-434122.hampstead.irccloud.com)
2024-06-25 11:21:39 +0000aristid(sid1599@id-1599.uxbridge.irccloud.com)
2024-06-25 11:21:41 +0000Fangs(sid141280@id-141280.hampstead.irccloud.com)
2024-06-25 11:21:42 +0000onliner10_(uid656258@user/onliner10)
2024-06-25 11:21:44 +0000sa(sid1055@id-1055.tinside.irccloud.com)
2024-06-25 11:21:51 +0000rubin55(sid175221@id-175221.hampstead.irccloud.com)
2024-06-25 11:21:54 +0000mankyKitty(sid31287@id-31287.helmsley.irccloud.com)
2024-06-25 11:21:56 +0000snek(sid280155@id-280155.lymington.irccloud.com)
2024-06-25 11:21:58 +0000dy(sid3438@user/dy)
2024-06-25 11:21:58 +0000PotatoGim(sid99505@id-99505.lymington.irccloud.com)
2024-06-25 11:21:59 +0000b20n(sid115913@id-115913.uxbridge.irccloud.com)
2024-06-25 11:22:00 +0000lexi-lambda(sid92601@id-92601.hampstead.irccloud.com)
2024-06-25 11:22:09 +0000tritlo_(sid58727@id-58727.hampstead.irccloud.com)
2024-06-25 11:22:09 +0000caasih(sid13241@id-13241.ilkley.irccloud.com)
2024-06-25 11:22:11 +0000SrPx(sid108780@id-108780.uxbridge.irccloud.com)
2024-06-25 11:22:13 +0000edwardk(sid47016@haskell/developer/edwardk)
2024-06-25 11:22:26 +0000chessai(sid225296@id-225296.lymington.irccloud.com)
2024-06-25 11:22:28 +0000meinside(uid24933@id-24933.helmsley.irccloud.com)
2024-06-25 11:22:37 +0000davetapley(sid666@id-666.uxbridge.irccloud.com)
2024-06-25 11:22:42 +0000jakesyl_____(sid56879@id-56879.hampstead.irccloud.com)
2024-06-25 11:22:44 +0000geekosaur(sid609282@xmonad/geekosaur)
2024-06-25 11:22:46 +0000taktoa[c](sid282096@id-282096.tinside.irccloud.com)
2024-06-25 11:22:50 +0000sa1(sid7690@id-7690.ilkley.irccloud.com)
2024-06-25 11:22:52 +0000SanchayanMaity(sid478177@id-478177.hampstead.irccloud.com)
2024-06-25 11:22:55 +0000systemfault(sid267009@about/typescript/member/systemfault)
2024-06-25 11:22:56 +0000dsal(sid13060@id-13060.lymington.irccloud.com)
2024-06-25 11:22:58 +0000jonrh(sid5185@id-5185.ilkley.irccloud.com)
2024-06-25 11:22:58 +0000Adeon(sid418992@id-418992.lymington.irccloud.com)
2024-06-25 11:22:58 +0000NemesisD(sid24071@id-24071.lymington.irccloud.com)
2024-06-25 11:22:59 +0000SethTisue(sid14912@id-14912.ilkley.irccloud.com)
2024-06-25 11:23:02 +0000jackdk(sid373013@cssa/jackdk)
2024-06-25 11:23:07 +0000gmc(sid58314@id-58314.ilkley.irccloud.com)
2024-06-25 11:23:08 +0000hovsater(sid499516@user/hovsater)
2024-06-25 11:23:08 +0000tapas(sid467876@id-467876.ilkley.irccloud.com)
2024-06-25 11:23:09 +0000smalltalkman(uid545680@id-545680.hampstead.irccloud.com)
2024-06-25 11:23:09 +0000tnks(sid412124@id-412124.helmsley.irccloud.com)
2024-06-25 11:23:16 +0000integral(sid296274@user/integral)
2024-06-25 11:23:16 +0000Boarders_____(sid425905@id-425905.lymington.irccloud.com)
2024-06-25 11:23:17 +0000iphy(sid67735@user/iphy)
2024-06-25 11:23:21 +0000Pent(sid313808@id-313808.lymington.irccloud.com)
2024-06-25 11:23:21 +0000JSharp(sid4580@user/JSharp)
2024-06-25 11:23:21 +0000lally(sid388228@id-388228.uxbridge.irccloud.com)
2024-06-25 11:23:25 +0000carter_(sid14827@id-14827.helmsley.irccloud.com)
2024-06-25 11:23:27 +0000buhman(sid411355@user/buhman)
2024-06-25 11:23:28 +0000rune_(sid21167@id-21167.ilkley.irccloud.com)
2024-06-25 11:23:34 +0000dmj`(uid72307@id-72307.hampstead.irccloud.com)
2024-06-25 11:23:36 +0000alinab(sid468903@id-468903.helmsley.irccloud.com)
2024-06-25 11:23:37 +0000jmct(sid160793@id-160793.tinside.irccloud.com)
2024-06-25 11:23:40 +0000delyan_(sid523379@id-523379.hampstead.irccloud.com)
2024-06-25 11:23:42 +0000ProofTechnique_(sid79547@id-79547.ilkley.irccloud.com)
2024-06-25 11:23:49 +0000amir(sid22336@user/amir)
2024-06-25 11:23:49 +0000edmundnoble_(sid229620@id-229620.helmsley.irccloud.com)
2024-06-25 11:24:03 +0000idnar(sid12240@debian/mithrandi)
2024-06-25 11:24:04 +0000mustafa(sid502723@rockylinux/releng/mustafa)
2024-06-25 11:24:06 +0000Techcable(sid534393@user/Techcable)
2024-06-25 11:24:07 +0000bw_______(sid2730@id-2730.ilkley.irccloud.com)
2024-06-25 11:24:08 +0000sclv(sid39734@haskell/developer/sclv)
2024-06-25 11:24:18 +0000degraafk(sid71464@id-71464.lymington.irccloud.com)
2024-06-25 11:24:19 +0000cbarrett(sid192934@id-192934.helmsley.irccloud.com)
2024-06-25 11:24:20 +0000Kamuela(sid111576@id-111576.tinside.irccloud.com)
2024-06-25 11:24:21 +0000shawwwn(sid6132@id-6132.helmsley.irccloud.com)
2024-06-25 11:24:24 +0000alanz(sid110616@id-110616.uxbridge.irccloud.com)
2024-06-25 11:24:27 +0000edm(sid147314@id-147314.hampstead.irccloud.com)
2024-06-25 11:24:34 +0000bjs(sid190364@user/bjs)
2024-06-25 11:24:45 +0000astra(sid289983@id-289983.hampstead.irccloud.com)
2024-06-25 11:24:54 +0000NiKaN(sid385034@id-385034.helmsley.irccloud.com)
2024-06-25 11:25:39 +0000hook54321(sid149355@user/hook54321)
2024-06-25 11:28:03 +0000gaze__(sid387101@helmsley.irccloud.com)
2024-06-25 11:36:18 +0000gaze__(sid387101@helmsley.irccloud.com) (Ping timeout: 256 seconds)
2024-06-25 11:36:48 +0000gaze__(sid387101@id-387101.helmsley.irccloud.com)
2024-06-25 11:46:55 +0000danse-nr3(~danse-nr3@151.37.135.52)
2024-06-25 11:47:47 +0000danse-nr3(~danse-nr3@151.37.135.52) (Remote host closed the connection)
2024-06-25 11:48:11 +0000danse-nr3(~danse-nr3@151.37.135.52)
2024-06-25 11:48:33 +0000wbooze(~wbooze@2a02:908:1244:9a20:570c:a8cf:25a8:c6db) (Remote host closed the connection)
2024-06-25 12:00:07 +0000 <lxsameer> hey folks, anything wrong with this test? I'm using hedgehog and tasty, this specific test falls in an infinit loop apparently. https://dpaste.com/F4NPGNTHE
2024-06-25 12:01:01 +0000JamesMowery9(~JamesMowe@ip98-167-207-182.ph.ph.cox.net)
2024-06-25 12:01:16 +0000 <lxsameer> or better to ask, how can I debug this
2024-06-25 12:02:59 +0000JamesMowery(~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Ping timeout: 264 seconds)
2024-06-25 12:02:59 +0000JamesMowery9JamesMowery
2024-06-25 12:08:13 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751) (Quit: Leaving.)
2024-06-25 12:13:38 +0000gmg(~user@user/gehmehgeh) (Remote host closed the connection)
2024-06-25 12:14:08 +0000CiaoSen(~Jura@2a05:5800:282:3d00:e6b9:7aff:fe80:3d03)
2024-06-25 12:19:50 +0000gmg(~user@user/gehmehgeh)
2024-06-25 12:20:59 +0000falafel(~falafel@79.117.174.22)
2024-06-25 12:22:16 +0000wbooze(~wbooze@2a02:908:1244:9a20:a1b0:ffa4:26e:2946)
2024-06-25 12:28:28 +0000 <int-e> What does genFunc do?
2024-06-25 12:29:04 +0000 <int-e> (My suspicion is that you're testing 10^11 cases which will take a while.)
2024-06-25 12:29:15 +0000danse-nr3(~danse-nr3@151.37.135.52) (Ping timeout: 255 seconds)
2024-06-25 12:30:52 +0000CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-06-25 12:31:49 +0000 <bwe> (Right 4 >>= (\x -> Right $ x+1)) -- returns Right 5
2024-06-25 12:32:16 +0000 <bwe> how can I pass multiple monads into the function?
2024-06-25 12:32:49 +0000 <bwe> (Right 4, Right 3) >>= (\x y -> Right $ x+y+1)) -- should return `Right 8`
2024-06-25 12:33:19 +0000CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
2024-06-25 12:35:07 +0000stiell(~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
2024-06-25 12:36:31 +0000stiell(~stiell@gateway/tor-sasl/stiell)
2024-06-25 12:40:01 +0000 <lxsameer> int-e: hmmm, let me show you the entire module
2024-06-25 12:40:03 +0000czy(~user@fortigate.wolfson.cam.ac.uk) (Ping timeout: 255 seconds)
2024-06-25 12:40:33 +0000 <lxsameer> int-e: https://dpaste.com/4A3CZMDQ3
2024-06-25 12:44:33 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751)
2024-06-25 12:49:10 +0000 <Leary> lxsameer: I don't know what else might be wrong, but that `Show` instance will produce infinite nonsense.
2024-06-25 12:49:42 +0000 <lxsameer> Leary: oh cool, I'll fix it
2024-06-25 12:50:16 +0000 <int-e> lxsameer: okay so it's only 200 cases which should be fine. hmm
2024-06-25 12:51:37 +0000zzz(~yin@user/zero)
2024-06-25 12:52:11 +0000 <int-e> (maybe you actually have a broken return or bind)
2024-06-25 12:52:22 +0000 <ncf> bwe: are you looking for join (liftA2 f a b)
2024-06-25 12:52:33 +0000bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2024-06-25 12:52:33 +0000 <ncf> that's not "multiple monads", though
2024-06-25 12:53:00 +0000 <int-e> well, it's multiple actions
2024-06-25 12:53:22 +0000 <lxsameer> It's not cause of the Show implementation. I replaced it with a constant function and still it is falling in an infinit loop
2024-06-25 12:53:44 +0000 <int-e> (monadic actions aren't monads, but confusing those is a common mistake)
2024-06-25 12:56:46 +0000zmt00(~zmt00@user/zmt00) (Ping timeout: 256 seconds)
2024-06-25 12:58:12 +0000 <bwe> ncf: my real problem is chaining monads of `Wrapper (Either a b)` where the b are different types (basically all args to a function are in a Monad and the function returns that Monad again)
2024-06-25 12:58:39 +0000falafel(~falafel@79.117.174.22) (Read error: Connection reset by peer)
2024-06-25 12:59:23 +0000andrewboltachev(~andrey@178.141.121.180)
2024-06-25 12:59:51 +0000cfricke(~cfricke@user/cfricke) (Ping timeout: 260 seconds)
2024-06-25 13:02:34 +0000ystael(~ystael@user/ystael)
2024-06-25 13:12:46 +0000generalbigm(~generalbi@2001:250:3c0f:2000::e751) (Quit: Leaving.)
2024-06-25 13:13:29 +0000noctux(~noctux@user/noctux) (Ping timeout: 268 seconds)
2024-06-25 13:15:35 +0000mjacob(~mjacob@adrastea.uberspace.de) (Ping timeout: 264 seconds)
2024-06-25 13:16:13 +0000Luj(~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat)
2024-06-25 13:16:36 +0000Luj(~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5)
2024-06-25 13:16:50 +0000noctux(~noctux@user/noctux)
2024-06-25 13:22:21 +0000noctux(~noctux@user/noctux) (Ping timeout: 256 seconds)
2024-06-25 13:22:29 +0000noctux(~noctux@user/noctux)
2024-06-25 13:25:44 +0000mjacob(~mjacob@adrastea.uberspace.de)
2024-06-25 13:26:43 +0000cfricke(~cfricke@user/cfricke)
2024-06-25 13:30:18 +0000sord937(~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds)
2024-06-25 13:41:35 +0000Guest5(~Guest5@102.215.56.232)
2024-06-25 13:45:16 +0000 <Guest5> Hey guys, I just started learning haskell using haskell mooc tutorial, i will really appreciate if they is some one i can ask questions personally and some questions won't make total sense since i'm still a beginner tho... but someone i could talk to when i have issue relating to haskell, a mentor and a friend i will appreciate it
2024-06-25 13:46:10 +0000zzz(~yin@user/zero) (Ping timeout: 268 seconds)
2024-06-25 13:46:54 +0000 <yushyin> ask here, this chat is super beginner friendly
2024-06-25 13:47:19 +0000sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-25 13:52:35 +0000zzz(~yin@user/zero)
2024-06-25 13:55:22 +0000Guest5(~Guest5@102.215.56.232) (Ping timeout: 250 seconds)
2024-06-25 13:58:27 +0000Guest5(~Guest5@102.215.56.232)
2024-06-25 14:04:35 +0000TactfulCitrus(al@gateway/vpn/protonvpn/tactfulcitrus)
2024-06-25 14:06:15 +0000 <haskellbridge> <sm> welcome Guest5
2024-06-25 14:07:36 +0000 <Guest5> Hello haskellbridge can i Dm you personally??
2024-06-25 14:07:52 +0000sata(~sata@185.57.29.142)
2024-06-25 14:12:35 +0000poscat-(~poscat@user/poscat) (Ping timeout: 264 seconds)
2024-06-25 14:14:25 +0000Guest5(~Guest5@102.215.56.232) (Ping timeout: 250 seconds)
2024-06-25 14:15:02 +0000 <haskellbridge> <sm> Guest5: a bit is fine, sure. FYI I'm sm, "haskellbridge" what you see on IRC when someone using the matrix chat system speaks
2024-06-25 14:20:51 +0000poscat(~poscat@user/poscat)
2024-06-25 14:21:22 +0000 <jackdk> FWIW, beginner questions are definitely on-topic here, and asking them means you might help out other learners who are lurking.
2024-06-25 14:23:41 +0000Guest5(~Guest5@102.215.56.232)
2024-06-25 14:24:46 +0000 <jackdk> FWIW, beginner questions are definitely on-topic here, and asking them means you might help out other learners who are lurking.
2024-06-25 14:25:01 +0000 <jackdk> (I'm assuming you're the same Guest5 who was here a second ago)
2024-06-25 14:25:39 +0000 <Guest5> yes
2024-06-25 14:30:34 +0000 <Guest5> But i will love to have someone i can message personally, like a mentor and a friend
2024-06-25 14:31:26 +0000 <Guest5> If i close the libra.chat tab on my browser i loose all the chat data
2024-06-25 14:32:17 +0000 <Guest5> i really hope you understand jackdk
2024-06-25 14:33:22 +0000 <sm> sure Guest5. You can wait, or also try asking on the haskell discourse or reddit, to reach more people
2024-06-25 14:33:52 +0000 <sm> an easy fix for losing the chat history is to connect via matrix: https://matrix.to/#/#haskell:matrix.org
2024-06-25 14:33:57 +0000 <jackdk> I think it is an overly limiting strategy but if it's one that's going to work better for you then I still wish you the best of luck. Haskell is a really fun language to learn and I hope you get to enjoy it.
2024-06-25 14:42:22 +0000lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-06-25 14:58:00 +0000CiaoSen(~Jura@2a05:5800:282:3d00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds)
2024-06-25 15:01:19 +0000sata(~sata@185.57.29.142) (Quit: Client closed)
2024-06-25 15:02:11 +0000flareon(~irfan@user/irfan)
2024-06-25 15:03:35 +0000 <flareon> i'm running GHC version 9.2.6. is forall printing after `:type` command in `ghci` on by default? how can i turn it off?
2024-06-25 15:11:52 +0000flareon(~irfan@user/irfan) (Ping timeout: 246 seconds)
2024-06-25 15:17:18 +0000poscat(~poscat@user/poscat) (Quit: Bye)
2024-06-25 15:17:31 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 15:17:32 +0000poscat(~poscat@user/poscat)
2024-06-25 15:19:52 +0000iza4k5(~iza4k5@2806:2f0:5321:fd27:4a57:5593:2173:1822)
2024-06-25 15:20:18 +0000danse-nr3(~danse-nr3@185.211.82.93)
2024-06-25 15:20:33 +0000Guest25(~Guest25@2a02-a45a-5cfd-1-2d76-bb4f-dde-6580.fixed6.kpn.net)
2024-06-25 15:21:09 +0000Guest25(~Guest25@2a02-a45a-5cfd-1-2d76-bb4f-dde-6580.fixed6.kpn.net) (Client Quit)
2024-06-25 15:23:43 +0000iza4k5(~iza4k5@2806:2f0:5321:fd27:4a57:5593:2173:1822) (Remote host closed the connection)
2024-06-25 15:23:52 +0000iza4k5(~iza4k5@2806:2f0:5321:fd27:4a57:5593:2173:1822)
2024-06-25 15:23:59 +0000soverysour(~soverysou@user/soverysour)
2024-06-25 15:28:55 +0000Guest5(~Guest5@102.215.56.232) (Quit: Client closed)
2024-06-25 15:34:47 +0000chele(~chele@user/chele) (Remote host closed the connection)
2024-06-25 15:40:52 +0000AlexNoo_(~AlexNoo@5.139.233.94)
2024-06-25 15:42:29 +0000AlexNoo(~AlexNoo@5.139.233.94) (Ping timeout: 252 seconds)
2024-06-25 15:42:57 +0000AlexZenon(~alzenon@5.139.233.94) (Ping timeout: 272 seconds)
2024-06-25 15:43:34 +0000cfricke(~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
2024-06-25 15:44:26 +0000hc(~hc@mail.hce.li)
2024-06-25 15:47:03 +0000AlexNoo(~AlexNoo@94.233.241.180)
2024-06-25 15:48:34 +0000AlexNoo_(~AlexNoo@5.139.233.94) (Ping timeout: 268 seconds)
2024-06-25 15:51:40 +0000philopsos1(~caecilius@user/philopsos)
2024-06-25 15:51:57 +0000philopsos1(~caecilius@user/philopsos) (Client Quit)
2024-06-25 15:52:18 +0000philopsos1(~caecilius@user/philopsos)
2024-06-25 15:54:06 +0000AlexZenon(~alzenon@94.233.241.180)
2024-06-25 15:57:22 +0000 <jackdk> flareon: I assume 9.2.8 is similar; use `:set -fno-print-explicit-foralls` to turn it off but I think it's off by default: https://www.irccloud.com/pastebin/TuB85DKb/fprint-explicit-foralls.txt
2024-06-25 16:00:13 +0000iza4k5(~iza4k5@2806:2f0:5321:fd27:4a57:5593:2173:1822) (Remote host closed the connection)
2024-06-25 16:01:45 +0000flareon(~irfan@223.182.115.80)
2024-06-25 16:02:49 +0000 <jackdk> flareon: I assume 9.2.8 is similar; use `:set -fno-print-explicit-foralls` to turn it off but I think it's off by default: https://www.irccloud.com/pastebin/TuB85DKb/fprint-explicit-foralls.txt
2024-06-25 16:09:26 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 252 seconds)
2024-06-25 16:22:29 +0000 <lxsameer> hey folks, how do you implement the Monad type class for a type like this? `data ExpectT (m :: Type -> Type) a = Success !(m a) | Failure !Error deriving stock (Show, Eq)`
2024-06-25 16:23:45 +0000 <ncf> https://hackage.haskell.org/package/transformers-0.6.1.1/docs/src/Control.Monad.Trans.Except.html#…
2024-06-25 16:26:43 +0000 <davean> Hum that question is so direct perhaps they're asking something else like how one goes about deriving it?
2024-06-25 16:28:29 +0000 <lxsameer> ncf: read that actually, but I'm a bit confused
2024-06-25 16:28:36 +0000rosco(~rosco@175.136.155.137)
2024-06-25 16:29:39 +0000 <davean> lxsameer: about what with it?
2024-06-25 16:30:09 +0000rosco(~rosco@175.136.155.137) (Client Quit)
2024-06-25 16:30:13 +0000 <lxsameer> davean: about the implementation of >>= for that type
2024-06-25 16:30:16 +0000 <lxsameer> for example
2024-06-25 16:30:39 +0000 <lxsameer> I don't know how to approach this case `Success m >>= g`
2024-06-25 16:31:21 +0000 <ncf> write down all the types in your context and the goal type
2024-06-25 16:31:25 +0000 <c_wraith> you need to use m's instance of >>=
2024-06-25 16:31:57 +0000 <lxsameer> ncf: what do you mean?
2024-06-25 16:32:02 +0000 <davean> Its pretty straight forward. "a <- runExceptT m" is what does that basicly. It just runs the inner thing.
2024-06-25 16:32:18 +0000 <davean> runExceptT is just an accessor that extracts the inner part.
2024-06-25 16:32:19 +0000 <ncf> m :: ?, g :: ?, goal :: ?
2024-06-25 16:32:25 +0000 <lxsameer> c_wraith: I've tried that, but since g is a -> ExpectT m b and not a -> mb
2024-06-25 16:32:26 +0000 <ncf> then play type tetris
2024-06-25 16:32:51 +0000 <lxsameer> ncf: that's what I was doing for the past couple of hours :P
2024-06-25 16:32:54 +0000 <davean> lxsameer: so you extract it!
2024-06-25 16:32:58 +0000 <c_wraith> if only there was a way to convert an ExceptT m a to an m a....
2024-06-25 16:33:15 +0000 <lxsameer> davean: I'm trying to let me show you some code
2024-06-25 16:33:24 +0000flareon(~irfan@223.182.115.80) (Quit: leaving)
2024-06-25 16:33:53 +0000 <davean> you apply an "a" to "a -> ExpectT m b", you get "ExpectT m b", you apply an "ExpectT m b -> m b".
2024-06-25 16:34:01 +0000 <davean> You have an "m b", you're done
2024-06-25 16:34:53 +0000 <lxsameer> how do you handle the Failure case of "ExpectT m b -> m b"
2024-06-25 16:35:00 +0000 <c_wraith> oh, you know what? people were mislead by your naming
2024-06-25 16:35:04 +0000 <c_wraith> *misled
2024-06-25 16:35:09 +0000 <davean> lxsameer: use a "case" statement
2024-06-25 16:35:10 +0000 <c_wraith> that's not ExceptT
2024-06-25 16:35:13 +0000 <ncf> hang on... this isn't a monad
2024-06-25 16:35:17 +0000 <ncf> lol
2024-06-25 16:35:21 +0000 <lxsameer> oh yeah, it's a new type
2024-06-25 16:35:23 +0000 <c_wraith> it's "some weirdo type"
2024-06-25 16:35:32 +0000 <ncf> this is Either (m a) Error
2024-06-25 16:35:34 +0000 <lxsameer> it does not have anything to do with ExceptT :D
2024-06-25 16:35:35 +0000 <c_wraith> and yes, it can't have a monad instance
2024-06-25 16:35:37 +0000 <ncf> you can't make a monad out of that
2024-06-25 16:35:53 +0000 <lxsameer> ok so I'm not crazy then :)))
2024-06-25 16:35:58 +0000 <ncf> ExceptT is m (Either Error a)
2024-06-25 16:36:10 +0000tabaqui(~root@91.74.190.107)
2024-06-25 16:36:17 +0000 <ncf> yes sorry should have looked closer
2024-06-25 16:36:29 +0000 <lxsameer> my bad, the naming is horrible i know
2024-06-25 16:36:35 +0000 <ncf> (ExpectT was not what i Expect'T)
2024-06-25 16:36:51 +0000 <lxsameer> :D
2024-06-25 16:37:00 +0000 <haskellbridge> <sm> good one
2024-06-25 16:37:45 +0000 <lxsameer> thanks folks
2024-06-25 16:39:27 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 16:39:51 +0000danse-nr3(~danse-nr3@185.211.82.93) (Ping timeout: 264 seconds)
2024-06-25 16:41:52 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 16:43:37 +0000tabaqui(~root@91.74.190.107)
2024-06-25 16:43:59 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 16:45:59 +0000tabaqui(~root@91.74.190.107)
2024-06-25 16:47:33 +0000zzz(~yin@user/zero) (Ping timeout: 255 seconds)
2024-06-25 16:50:41 +0000econo_(uid147250@id-147250.tinside.irccloud.com)
2024-06-25 16:54:34 +0000zzz(~yin@user/zero)
2024-06-25 16:58:21 +0000madhavanmiui(~madhavanm@2409:40f4:305f:dd79:8000::)
2024-06-25 16:59:18 +0000madhavanmiui(~madhavanm@2409:40f4:305f:dd79:8000::) (Client Quit)
2024-06-25 17:01:06 +0000target_i(~target_i@user/target-i/x-6023099)
2024-06-25 17:05:59 +0000zzz(~yin@user/zero) (Ping timeout: 264 seconds)
2024-06-25 17:06:29 +0000pavonia(~user@user/siracusa)
2024-06-25 17:08:15 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 17:12:43 +0000zzz(~yin@user/zero)
2024-06-25 17:16:03 +0000tabaqui(~root@91.74.190.107) (Quit: WeeChat 4.2.2)
2024-06-25 17:16:18 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:17:32 +0000MrFox(~MrFox___@95-178-182-201.dsl.optinet.hr)
2024-06-25 17:18:37 +0000ubert(~Thunderbi@2a02:8109:ab8a:5a00:fafc:98d0:fb97:e3fd) (Remote host closed the connection)
2024-06-25 17:19:58 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:20:14 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:20:43 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:21:06 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:21:33 +0000 <probie> Are you sure you can't make a monad instance? It's not a regular monad transformer, but I think you can probably do `instance (Traversable m) => Monad (ExpectT m)`
2024-06-25 17:21:42 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:22:13 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:23:13 +0000 <ncf> yes, you can't have a general monad instance
2024-06-25 17:23:36 +0000 <ncf> but if m distributes over Either then you can
2024-06-25 17:23:36 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:24:18 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:24:37 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:24:52 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:24:55 +0000 <ncf> i mean Either Error
2024-06-25 17:25:03 +0000 <probie> but like, you can't have a "general monad instance" for something like `ReaderT` either, right?
2024-06-25 17:25:43 +0000 <ncf> ? ReaderT is a monad transformer
2024-06-25 17:25:48 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:26:03 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:27:14 +0000lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 268 seconds)
2024-06-25 17:28:27 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:29:48 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:31:07 +0000 <probie> sure, but `ReaderT m` is a monad if `m` is a monad, and `ExpectT m` is a monad if `m` is traversable. Given that the conversation above wasn't immediately a domain error, I assume we're talking writing a monad instance for `ExpectT m` and not `ExpectT`
2024-06-25 17:31:50 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:32:06 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:32:43 +0000 <ncf> so ExpectT isn't a monad transformer. that's all i'm saying
2024-06-25 17:33:23 +0000MrFox(~MrFox___@95-178-182-201.dsl.optinet.hr) (Quit: Leaving)
2024-06-25 17:34:17 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:34:52 +0000tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2024-06-25 17:35:22 +0000euleritian(~euleritia@dynamic-176-004-206-189.176.4.pool.telefonica.de)
2024-06-25 17:36:39 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:36:44 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:41:00 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:41:13 +0000MrFox(~MrFox___@95-178-182-201.dsl.optinet.hr)
2024-06-25 17:44:51 +0000MrFox(~MrFox___@95-178-182-201.dsl.optinet.hr) (Client Quit)
2024-06-25 17:45:34 +0000waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-25 17:48:41 +0000philopsos1(~caecilius@user/philopsos) (Ping timeout: 256 seconds)
2024-06-25 17:53:51 +0000tabaqui(~root@91.74.190.107) (Quit: WeeChat 4.2.2)
2024-06-25 17:54:06 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:55:03 +0000safinaskar(~quassel@212.73.77.104)
2024-06-25 17:55:09 +0000tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-25 17:55:25 +0000tabaqui(~root@91.74.190.107)
2024-06-25 17:59:14 +0000 <safinaskar> why this code doesn't work? https://play.haskell.org/saved/uSEhLigM
2024-06-25 17:59:24 +0000 <safinaskar> DataKinds
2024-06-25 17:59:33 +0000 <safinaskar> type system trickery, forall, etc
2024-06-25 17:59:37 +0000philopsos1(~caecilius@user/philopsos)
2024-06-25 18:00:48 +0000 <EvanR> cannot instantiate unification variable with a type involving polytypes
2024-06-25 18:00:52 +0000 <geekosaur> it's impredicative
2024-06-25 18:01:57 +0000 <geekosaur> and indeed adding `{-# LANGUAGE ImpredicativeTypes #-}` makes it work
2024-06-25 18:02:59 +0000 <ncf> try ind _ _ = undefined
2024-06-25 18:04:23 +0000philopsos1(~caecilius@user/philopsos) (Ping timeout: 252 seconds)
2024-06-25 18:05:59 +0000euleritian(~euleritia@dynamic-176-004-206-189.176.4.pool.telefonica.de) (Ping timeout: 264 seconds)
2024-06-25 18:06:24 +0000kmein(~weechat@user/kmein) (Quit: ciao kakao)
2024-06-25 18:06:32 +0000euleritian(~euleritia@dynamic-176-001-141-070.176.1.pool.telefonica.de)
2024-06-25 18:06:46 +0000kmein(~weechat@user/kmein)
2024-06-25 18:12:07 +0000Lord_of_Life_(~Lord@user/lord-of-life/x-2819915)
2024-06-25 18:13:03 +0000Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds)
2024-06-25 18:13:25 +0000tabaqui(~root@91.74.190.107) (Quit: WeeChat 4.2.2)
2024-06-25 18:13:30 +0000Lord_of_Life_Lord_of_Life
2024-06-25 18:13:46 +0000tabaqui(~root@91.74.190.107)
2024-06-25 18:15:06 +0000euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-06-25 18:16:10 +0000wootehfoot(~wootehfoo@user/wootehfoot)
2024-06-25 18:17:16 +0000danse-nr3(~danse-nr3@151.35.129.90)
2024-06-25 18:18:00 +0000danse-nr3(~danse-nr3@151.35.129.90) (Remote host closed the connection)
2024-06-25 18:18:25 +0000danse-nr3(~danse-nr3@151.35.129.90)
2024-06-25 18:20:52 +0000euphores(~SASL_euph@user/euphores)
2024-06-25 18:22:27 +0000zzz(~yin@user/zero) (Ping timeout: 264 seconds)
2024-06-25 18:28:27 +0000soverysour(~soverysou@user/soverysour) (Ping timeout: 264 seconds)
2024-06-25 18:33:06 +0000zzz(~yin@user/zero)
2024-06-25 18:40:17 +0000kmein(~weechat@user/kmein) (Quit: ciao kakao)
2024-06-25 18:40:37 +0000kmein(~weechat@user/kmein)
2024-06-25 18:46:42 +0000kmein(~weechat@user/kmein) (Quit: ciao kakao)
2024-06-25 18:47:03 +0000kmein(~weechat@user/kmein)
2024-06-25 19:04:18 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 19:05:05 +0000kmein(~weechat@user/kmein) (Quit: ciao kakao)
2024-06-25 19:05:25 +0000kmein(~weechat@user/kmein)
2024-06-25 19:11:11 +0000 <safinaskar> ncf: it worked, thank you!
2024-06-25 19:11:59 +0000 <safinaskar> geekosaur: ImpredicativeTypes worked, too! thank you!
2024-06-25 19:15:15 +0000euleritian(~euleritia@dynamic-176-001-141-070.176.1.pool.telefonica.de) (Ping timeout: 264 seconds)
2024-06-25 19:16:29 +0000euleritian(~euleritia@dynamic-176-001-142-009.176.1.pool.telefonica.de)
2024-06-25 19:21:19 +0000euleritian(~euleritia@dynamic-176-001-142-009.176.1.pool.telefonica.de) (Ping timeout: 268 seconds)
2024-06-25 19:22:37 +0000euleritian(~euleritia@dynamic-176-001-142-009.176.1.pool.telefonica.de)
2024-06-25 19:25:02 +0000safinaskar(~quassel@212.73.77.104) ()
2024-06-25 19:38:17 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-25 19:48:51 +0000danse-nr3(~danse-nr3@151.35.129.90) (Ping timeout: 264 seconds)
2024-06-25 19:49:11 +0000danse-nr3(~danse-nr3@151.35.138.53)
2024-06-25 19:58:17 +0000wbooze(~wbooze@2a02:908:1244:9a20:a1b0:ffa4:26e:2946) (Remote host closed the connection)
2024-06-25 19:58:30 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 20:00:35 +0000safinaskar(~quassel@212.73.77.104)
2024-06-25 20:06:39 +0000danse-nr3(~danse-nr3@151.35.138.53) (Ping timeout: 268 seconds)
2024-06-25 20:07:11 +0000ss4(~wootehfoo@user/wootehfoot)
2024-06-25 20:08:16 +0000 <safinaskar> https://godbolt.org/z/z4EdxaeEv
2024-06-25 20:08:32 +0000 <safinaskar> how to make this "x" refer to "x" defined above? is this possible?
2024-06-25 20:09:10 +0000 <EvanR> lowercase letters are type variables
2024-06-25 20:09:30 +0000 <EvanR> make a datatype called X
2024-06-25 20:09:30 +0000 <safinaskar> okay, is there a way to make this "x" to refer to x defined above?
2024-06-25 20:09:35 +0000 <safinaskar> maybe 'x ?
2024-06-25 20:09:39 +0000 <safinaskar> or ''x ?
2024-06-25 20:09:39 +0000 <ncf> no
2024-06-25 20:09:47 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 256 seconds)
2024-06-25 20:09:51 +0000wootehfoot(~wootehfoo@user/wootehfoot) (Ping timeout: 264 seconds)
2024-06-25 20:10:47 +0000 <EvanR> you're basically writing y :: forall x . x
2024-06-25 20:10:54 +0000 <ncf> that would require running arbitrary programs during type-checking, which is a feature of dependently-typed programming languages, but not haskell
2024-06-25 20:10:58 +0000phma(phma@2001:5b0:211f:da48:e550:db55:4d2e:255e) (Read error: Connection reset by peer)
2024-06-25 20:11:44 +0000phma(~phma@host-67-44-208-116.hnremote.net)
2024-06-25 20:11:59 +0000 <monochrom> Option 1: Add "type X = Type", then you may use "y :: X".
2024-06-25 20:12:27 +0000 <monochrom> Option 2: Delete "y :: ...". Wrtie "y = undefined `asTypeOf` x"
2024-06-25 20:12:44 +0000 <ncf> that's not the same at all though
2024-06-25 20:13:01 +0000 <monochrom> I have given up "sameness".
2024-06-25 20:13:02 +0000 <EvanR> newtype X = X
2024-06-25 20:13:17 +0000 <ncf> i mean this seems unrelated
2024-06-25 20:14:13 +0000 <monochrom> Ah, maybe I misread the question.
2024-06-25 20:14:45 +0000 <monochrom> No, I did not. There were two mutually contradictary questions.
2024-06-25 20:14:51 +0000 <ncf> they want to do things like x = Int; y :: x; y = 42, i think
2024-06-25 20:14:54 +0000 <monochrom> Therefore all answers are related! >:)
2024-06-25 20:15:10 +0000 <monochrom> Then asTypeOf is spot on.
2024-06-25 20:15:21 +0000 <ncf> ?? no it's not
2024-06-25 20:15:21 +0000 <lambdabot> no it's not
2024-06-25 20:15:29 +0000 <EvanR> X = Type isn't the same as x :: Type
2024-06-25 20:15:42 +0000 <EvanR> is vs is a
2024-06-25 20:16:01 +0000 <EvanR> but the answer was "no" so we're good xD
2024-06-25 20:17:45 +0000 <monochrom> OK I will settle for "no".
2024-06-25 20:19:09 +0000 <ncf> anyway, this makes me wonder: is it actually possible to refer to Int on the term level in haskell?
2024-06-25 20:19:30 +0000 <ncf> is there some kind of reified version of Int, i guess
2024-06-25 20:20:00 +0000 <monochrom> Does "expr :: Int" count?
2024-06-25 20:20:35 +0000 <monochrom> If foo::Int, then "bar `asTypeOf` foo" also helps.
2024-06-25 20:20:36 +0000 <EvanR> > typeOf (3 :: Int)
2024-06-25 20:20:37 +0000 <lambdabot> Int
2024-06-25 20:20:44 +0000 <EvanR> :t typeOf (3 :: Int)
2024-06-25 20:20:45 +0000 <lambdabot> TypeRep
2024-06-25 20:21:13 +0000 <ncf> no, i mean as in Int :: Type
2024-06-25 20:21:27 +0000 <EvanR> :k Int
2024-06-25 20:21:28 +0000 <lambdabot> *
2024-06-25 20:21:44 +0000 <EvanR> *'s don't exist at the value level
2024-06-25 20:21:48 +0000 <ncf> i guess the whole point of Type is that its elements are types
2024-06-25 20:21:56 +0000 <ncf> right
2024-06-25 20:22:06 +0000 <ncf> i was confused because of data kinds
2024-06-25 20:22:14 +0000 <ncf> but 'S is still not a term-level thing
2024-06-25 20:22:16 +0000 <ncf> S is
2024-06-25 20:22:29 +0000 <safinaskar> i'm trying to formalize Peano arithmetic in haskell types. here is what i'm trying to do: https://godbolt.org/z/9e5K3hY17
2024-06-25 20:22:57 +0000 <safinaskar> if I create lowercase "z", then I cannot refer to it later in types
2024-06-25 20:23:00 +0000 <ncf> why not agda?
2024-06-25 20:23:04 +0000 <monochrom> Right, I hate it that "data X = MkX" does not mean dependent typing, it just means there are two copies --- mutually unrelated even --- in two namespaces.
2024-06-25 20:23:12 +0000 <EvanR> use uppercase Z
2024-06-25 20:23:21 +0000 <safinaskar> but if I crate uppercase "Z" instead using "data Z :: Nat where", then i get compilation error
2024-06-25 20:23:22 +0000euleritian(~euleritia@dynamic-176-001-142-009.176.1.pool.telefonica.de) (Ping timeout: 246 seconds)
2024-06-25 20:23:36 +0000 <EvanR> data Nat = Z | S Nat
2024-06-25 20:23:48 +0000 <monochrom> Actually, I misspoke. I hate it when Haskellers mistake DataKinds for dependent typing. >:)
2024-06-25 20:23:52 +0000 <dolio> ncf: You can write `foo :: Type ; foo = Int`, and GHC recognizes what you're doing, but complains about it.
2024-06-25 20:24:09 +0000 <ncf> right
2024-06-25 20:24:23 +0000 <safinaskar> "data Z :: Nat where" gives "Data type has non-* return kind `Nat'" error
2024-06-25 20:24:37 +0000killy(~killy@staticline-31-183-151-196.toya.net.pl)
2024-06-25 20:24:42 +0000euleritian(~euleritia@dynamic-176-000-145-208.176.0.pool.telefonica.de)
2024-06-25 20:24:45 +0000 <EvanR> alternatively
2024-06-25 20:24:48 +0000 <EvanR> data Nat where
2024-06-25 20:24:51 +0000 <safinaskar> EvanR: "data Nat = Z | S Nat" - this is not what i want
2024-06-25 20:24:51 +0000 <EvanR> Z :: Nat
2024-06-25 20:24:55 +0000 <EvanR> S :: Nat -> Nat
2024-06-25 20:25:03 +0000 <safinaskar> EvanR: and this is not what i want, too
2024-06-25 20:25:04 +0000 <EvanR> then DataKinds comes in
2024-06-25 20:25:13 +0000 <safinaskar> EvanR: i want to define everything axiomatically
2024-06-25 20:25:22 +0000 <safinaskar> without relying on ADT/GADT machinery
2024-06-25 20:25:27 +0000 <monochrom> If that is not what you want, then I agree with ncf about why are you using Haskell instead of Agda.
2024-06-25 20:25:35 +0000 <EvanR> then you go back to START where lowercase are universally quantified type variables
2024-06-25 20:25:40 +0000 <dolio> You shouldn't even use Agda, you should use twelf or something.
2024-06-25 20:25:41 +0000 <EvanR> wrong language
2024-06-25 20:25:52 +0000 <monochrom> Although, I can't see how Agda, or Coq, or Lean, or anything, would accept you code either.
2024-06-25 20:25:53 +0000 <safinaskar> "why are you using Haskell instead of Agda" - for fun
2024-06-25 20:25:54 +0000 <safinaskar> :)
2024-06-25 20:26:01 +0000 <safinaskar> i'm just trying to explore haskell power
2024-06-25 20:26:11 +0000 <safinaskar> i want to know whether this is possible to write in haskell
2024-06-25 20:26:20 +0000 <safinaskar> maybe using some experimental features?
2024-06-25 20:26:24 +0000 <monochrom> OK Lean would accept it as "user adds axioms recklessly. not recommended."
2024-06-25 20:26:26 +0000 <EvanR> that you can't use lowercase for this, then not doing anything, is not a good test of the power
2024-06-25 20:26:50 +0000 <monochrom> This is not possible in Haskell.
2024-06-25 20:26:57 +0000 <safinaskar> EvanR: uppercase doesn't work either. "data Z :: Nat where" gives compilation error
2024-06-25 20:27:13 +0000 <EvanR> that's just the wrong syntax
2024-06-25 20:27:30 +0000 <monochrom> Both lowercase and uppercase are wrong syntax.
2024-06-25 20:27:31 +0000 <safinaskar> EvanR: "data Z :: Type where" works. "data Z :: Nat where" doesn't
2024-06-25 20:27:32 +0000 <EvanR> e.g. you can also use data families
2024-06-25 20:30:24 +0000 <EvanR> it would let you add more instances of a data family Nat, but since you only need 2... it doesn't really help
2024-06-25 20:30:42 +0000 <EvanR> you can list them all under DataKind Nat
2024-06-25 20:31:39 +0000walee_(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-25 20:32:10 +0000lxsameer(~lxsameer@Serene/lxsameer)
2024-06-25 20:32:59 +0000waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds)
2024-06-25 20:33:11 +0000 <monochrom> May I say that earlier you didn't come across as exploring, instead as entitlement, because there were too many (and only) "no not what I want".
2024-06-25 20:36:11 +0000walee_(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds)
2024-06-25 20:39:29 +0000 <safinaskar> dolio: wow. i'm glad someone here is aware about twelf
2024-06-25 20:39:39 +0000 <safinaskar> i like twelf (but i didn't use it)
2024-06-25 20:40:15 +0000 <safinaskar> monochrom: "Although, I can't see how Agda, or Coq, or Lean, or anything, would accept you code either" - it will. i'm 100% sure
2024-06-25 20:42:59 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 20:44:16 +0000 <int-e> (algebraic) data types in Haskell are closed; there's no reason to support that kind of syntax.
2024-06-25 20:46:44 +0000lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 268 seconds)
2024-06-25 20:47:54 +0000 <safinaskar> i will write now the same code in agda or rocq or lean or something and will show you
2024-06-25 20:47:58 +0000killy(~killy@staticline-31-183-151-196.toya.net.pl) (Ping timeout: 268 seconds)
2024-06-25 20:48:00 +0000 <safinaskar> to prove that this is possible
2024-06-25 20:48:20 +0000 <safinaskar> please, give me link to some agda or rocq (a.k.a. coq) or lean playground
2024-06-25 20:48:22 +0000 <safinaskar> or idris
2024-06-25 20:48:32 +0000waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-25 20:48:46 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 20:49:08 +0000 <ncf> what, formalising peano's axioms? i don't need a proof that this is possible lol
2024-06-25 20:50:03 +0000dcoutts(~duncan@2a00:23c6:1c8d:901:b94:4566:9d63:4848) (Ping timeout: 264 seconds)
2024-06-25 20:50:18 +0000 <safinaskar> i want not only to formalize peano axioms, but also to formalize them exactly the same way i want
2024-06-25 20:50:28 +0000 <safinaskar> to show you how exactly i want to formalize them in haskell
2024-06-25 20:50:43 +0000 <safinaskar> also, monochrom said this is impossible
2024-06-25 20:50:47 +0000 <safinaskar> i want to prove them wrong
2024-06-25 20:51:05 +0000 <ncf> impossible *in Haskell*
2024-06-25 20:51:20 +0000 <ncf> you're not going to prove that wrong by doing it in agda
2024-06-25 20:51:36 +0000sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2024-06-25 20:56:27 +0000noumenon(~noumenon@113.51-175-156.customer.lyse.net)
2024-06-25 20:57:05 +0000wbooze(~wbooze@2a02:908:1244:9a20:3ca9:9685:6335:ca5e)
2024-06-25 20:58:24 +0000Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal)
2024-06-25 21:01:04 +0000 <safinaskar> okay, here is lean 3 version: https://paste.tomsmeding.com/eboBcN4c
2024-06-25 21:01:19 +0000 <safinaskar> it works, i tested at https://leanprover-community.github.io/lean-web-editor/
2024-06-25 21:01:32 +0000 <safinaskar> i used lean 3, because i was unable to find lean 4 online playground
2024-06-25 21:01:39 +0000 <safinaskar> so, yes, it is possible
2024-06-25 21:01:44 +0000 <safinaskar> how to write the same in haskell?
2024-06-25 21:02:10 +0000 <safinaskar> monochrom: i did this
2024-06-25 21:04:22 +0000 <ncf> haskell has not become dependently typed in the past 40 minutes, sadly
2024-06-25 21:05:49 +0000 <safinaskar> yeah, it is sad
2024-06-25 21:07:03 +0000 <EvanR> haskell dependent types: always 40 years away
2024-06-25 21:08:02 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 21:11:44 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 21:12:49 +0000poscat0x04(~poscat@user/poscat)
2024-06-25 21:13:11 +0000poscat(~poscat@user/poscat) (Ping timeout: 264 seconds)
2024-06-25 21:14:19 +0000dcoutts(~duncan@2a00:23c6:1c8d:901:b94:4566:9d63:4848)
2024-06-25 21:14:50 +0000 <safinaskar> i have shirt, which states "haskell"
2024-06-25 21:17:09 +0000 <safinaskar> and moreover i have another T-shirt, which says... wait for it... "if b: B for any x: A, then (\x: A. b) : (Π x: A. B)"!!!!!!!!!
2024-06-25 21:17:23 +0000 <safinaskar> i'm very glad my friends presented my such T-shirt
2024-06-25 21:21:17 +0000 <EvanR> :t if b: B for any x: A, then (\x: A. b) : (Π x: A. B)
2024-06-25 21:21:18 +0000 <lambdabot> error: parse error on input ‘,’
2024-06-25 21:21:30 +0000 <EvanR> your shirt doesn't compile
2024-06-25 21:21:39 +0000 <safinaskar> EvanR: this is not haskell expression
2024-06-25 21:21:47 +0000 <EvanR> oh it's a different shirt
2024-06-25 21:21:49 +0000 <safinaskar> EvanR: this is fundamental law of pure type system
2024-06-25 21:22:00 +0000 <safinaskar> yes, these are two different shirts
2024-06-25 21:22:57 +0000 <safinaskar> the shirt features "abstraction" axiom from here: https://en.wikipedia.org/wiki/Pure_type_system
2024-06-25 21:25:48 +0000 <safinaskar> EvanR: "you can also use data families" - wow!!!!! it seems it worked!
2024-06-25 21:25:54 +0000 <EvanR> o_O
2024-06-25 21:28:24 +0000 <safinaskar> here is code: https://godbolt.org/z/51WvfW3eb !!!
2024-06-25 21:28:28 +0000 <safinaskar> it seems it worked!
2024-06-25 21:28:30 +0000 <safinaskar> did it?
2024-06-25 21:28:47 +0000waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Quit: WeeChat 4.1.2)
2024-06-25 21:28:55 +0000 <safinaskar> does this code really state induction axiom?
2024-06-25 21:28:55 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 21:29:51 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-25 21:30:34 +0000 <EvanR> the problem is probably in the word "really"
2024-06-25 21:30:38 +0000euleritian(~euleritia@dynamic-176-000-145-208.176.0.pool.telefonica.de) (Ping timeout: 252 seconds)
2024-06-25 21:31:03 +0000euleritian(~euleritia@dynamic-176-000-205-223.176.0.pool.telefonica.de)
2024-06-25 21:35:42 +0000takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-06-25 21:36:20 +0000noumenon(~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving)
2024-06-25 21:43:31 +0000target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2024-06-25 21:52:03 +0000Sgeo(~Sgeo@user/sgeo)
2024-06-25 21:59:37 +0000YoungFrog(~youngfrog@39.129-180-91.adsl-dyn.isp.belgacom.be) (Ping timeout: 246 seconds)
2024-06-25 22:02:34 +0000 <safinaskar> okay, it didn't work
2024-06-25 22:02:35 +0000 <safinaskar> https://godbolt.org/z/obdE6jnMM
2024-06-25 22:02:46 +0000 <safinaskar> i tried to actually prove something and i failed
2024-06-25 22:03:03 +0000 <safinaskar> because haskell seems not to have higher order unification
2024-06-25 22:03:05 +0000 <safinaskar> or it has?
2024-06-25 22:03:12 +0000 <safinaskar> is there some way to make this code work?
2024-06-25 22:04:21 +0000ystael(~ystael@user/ystael) (Ping timeout: 255 seconds)
2024-06-25 22:05:06 +0000szkl(uid110435@id-110435.uxbridge.irccloud.com)
2024-06-25 22:07:48 +0000 <EvanR> on 29 you tried to refer to the same variables introduced in the type signature
2024-06-25 22:07:54 +0000 <EvanR> that doesn't work without ScopedTypeVariables
2024-06-25 22:08:50 +0000Guest89(~Guest89@bras-base-mtrlpq4706w-grc-02-174-89-234-134.dsl.bell.ca)
2024-06-25 22:09:10 +0000 <ncf> that's included in ghc2021
2024-06-25 22:09:34 +0000Guest89(~Guest89@bras-base-mtrlpq4706w-grc-02-174-89-234-134.dsl.bell.ca) (Client Quit)
2024-06-25 22:09:35 +0000 <ncf> the problem is that there are no type-level abstractions, so you can express p = λ b. Equal (c a) (c b)
2024-06-25 22:10:46 +0000 <safinaskar> ncf: thanks
2024-06-25 22:10:54 +0000 <safinaskar> ncf: this is exactly i'm trying to express
2024-06-25 22:10:54 +0000 <ncf> can't**
2024-06-25 22:12:10 +0000 <ncf> you'd need a newtype probably
2024-06-25 22:13:16 +0000tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-25 22:15:57 +0000 <safinaskar> ha! it works! https://godbolt.org/z/Pxxjvq3oe
2024-06-25 22:16:05 +0000 <safinaskar> i fixed my code and now it works!
2024-06-25 22:16:13 +0000 <safinaskar> i was able to express that lambda!
2024-06-25 22:20:40 +0000 <ncf> note https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-Type-Equality.html
2024-06-25 22:21:51 +0000 <safinaskar> ncf: thanks
2024-06-25 22:21:56 +0000 <safinaskar> ncf: you are very helpful
2024-06-25 22:22:06 +0000 <safinaskar> ncf: but i did my way, because that is whole point
2024-06-25 22:24:05 +0000sp1ff(~user@c-73-11-70-111.hsd1.wa.comcast.net)
2024-06-25 22:25:44 +0000machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-25 22:29:46 +0000Foxxer(~Foxxer@152.250.71.122)
2024-06-25 22:29:47 +0000Foxxer(~Foxxer@152.250.71.122) (Remote host closed the connection)
2024-06-25 22:29:56 +0000michalz(~michalz@185.246.207.193) (Quit: ZNC 1.9.0 - https://znc.in)
2024-06-25 22:30:13 +0000Foxxer(~Foxxer@152.250.71.122)
2024-06-25 22:31:40 +0000Foxxer(~Foxxer@152.250.71.122) (Remote host closed the connection)
2024-06-25 22:33:33 +0000__monty__(~toonn@user/toonn) (Quit: leaving)
2024-06-25 22:42:11 +0000 <safinaskar> now i'm trying to prove (x + y = y + x) (or something similar) using all this machinery
2024-06-25 22:43:30 +0000sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 255 seconds)
2024-06-25 22:44:02 +0000Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
2024-06-25 22:44:29 +0000cheater(~Username@user/cheater) (Ping timeout: 256 seconds)
2024-06-25 22:44:31 +0000acidjnk_new3(~acidjnk@p200300d6e714dc90fd0a56c96235233a.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2024-06-25 22:44:36 +0000cheater(~Username@user/cheater)
2024-06-25 22:46:05 +0000 <EvanR> easy
2024-06-25 22:46:07 +0000joeyadams(~joeyadams@2607:fb91:1617:1400:929b:26f0:654:cc5a)
2024-06-25 22:46:08 +0000 <EvanR> just make an axiom for that
2024-06-25 22:46:23 +0000 <EvanR> call it ring theory
2024-06-25 22:49:55 +0000causal(~eric@50.35.88.207) (Quit: WeeChat 4.3.1)
2024-06-25 22:51:57 +0000noumenon(~noumenon@113.51-175-156.customer.lyse.net)
2024-06-25 23:00:20 +0000ft(~ft@p4fc2ab80.dip0.t-ipconnect.de)
2024-06-25 23:00:39 +0000 <safinaskar> ha! i proved (0 + x = x) using (x + 0 = x) and induction! https://godbolt.org/z/YMYrWW6Ee
2024-06-25 23:00:46 +0000 <safinaskar> in haskell
2024-06-25 23:00:57 +0000 <safinaskar> this means that induction actually works!
2024-06-25 23:01:13 +0000 <safinaskar> so yes, i was able to cope with all problems!
2024-06-25 23:01:52 +0000 <safinaskar> so, yes, it is possible to fake type-level lambdas!
2024-06-25 23:03:21 +0000 <EvanR> for your next trick, use haskell to prove FALSE
2024-06-25 23:04:09 +0000 <safinaskar> EvanR: unfortunately, this is easy, too. "false :: forall a. a" "false = undefined"
2024-06-25 23:04:13 +0000waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-25 23:04:25 +0000 <EvanR> and see that it is much more powerful than stuff like coq which cripples itself into only proving true stuff
2024-06-25 23:09:54 +0000 <safinaskar> how i will try to prove the same thing using C++ and Rust :)
2024-06-25 23:10:22 +0000 <safinaskar> i'm not sure about Rust, but in C++ this seems to be totally possible
2024-06-25 23:11:36 +0000 <safinaskar> for example, "f :: forall (a :: Type -> Type). Int" can be written in C++ so: "template <template <typename> typename T> int f()"
2024-06-25 23:34:18 +0000 <joeyadams> Records compile into somewhat large binaries, is this a known issue? For example, I have a module with 16 records (205 fields), and it produces a 490K .o file (versus 99K if I remove the records). If I derive generic Aeson instances, it becomes 2.3M, and takes several seconds to compile.
2024-06-25 23:35:44 +0000 <joeyadams> This means if I generate bindings for a database with 100 tables, I end up with an absurdly large binary. Not the end of the world, just slightly disappointing.
2024-06-25 23:43:27 +0000 <safinaskar> joeyadams: use rust. it compiles fast (compared to haskell)
2024-06-25 23:43:47 +0000 <safinaskar> joeyadams: aeson in rust world is called serde_json
2024-06-25 23:44:14 +0000 <safinaskar> joeyadams: instances for serde_json are generated automatically, too
2024-06-25 23:45:03 +0000 <joeyadams> Just curious, does serde_json use a generic system sort of like Haskell has, or is it more like C# where it's all run-time reflection?
2024-06-25 23:45:06 +0000 <safinaskar> joeyadams: binary sizes likely to be big, too. but compilation speed will be nice
2024-06-25 23:45:46 +0000 <joeyadams> So I just need to write a quick sed replace to turn my Haskell code into Rust, and I'll be set :-)
2024-06-25 23:45:55 +0000 <safinaskar> joeyadams: serde_json works in compile-time
2024-06-25 23:46:49 +0000 <safinaskar> joeyadams: first package called "serde" derives all needed instances in compile time using so-called proc macros (it is code, which executes in compile time and generates AST, similar to template haskell)
2024-06-25 23:46:56 +0000 <safinaskar> and then serde_json uses these instances
2024-06-25 23:48:19 +0000 <joeyadams> An important detail I left out: I had deriving Show on all my records. I took that off and that took off 300K.
2024-06-25 23:51:23 +0000 <joeyadams> But I am curious why derived instances might take up so much code. Deriving FromJSON/ToJSON for 15 records produces as much binary code as the whole Aeson library.
2024-06-25 23:51:39 +0000 <EvanR> Hi can you not respond to a haskell question by saying use rust
2024-06-25 23:51:40 +0000 <joeyadams> I should try writing the instances manually to see how big the code footprint is.
2024-06-25 23:52:06 +0000 <safinaskar> EvanR: okay :(
2024-06-25 23:53:00 +0000 <EvanR> joeyadams, did you try flags to reduce the binary size, did you try to strip the binary
2024-06-25 23:53:14 +0000 <EvanR> are you compiling in profiling support
2024-06-25 23:54:20 +0000 <joeyadams> I'm just using GHC 9.4.8 installed through ghcup, not sure what that compiled in. I also tried with later GHC versions and saw similar results (slow compiles and large binaries).
2024-06-25 23:55:08 +0000 <EvanR> template haskell and generics does have a compile time cost, but you were asking about binary size
2024-06-25 23:55:27 +0000 <EvanR> you can issue flags to optimize for speed or size... -Os ?
2024-06-25 23:56:06 +0000 <joeyadams> I looked into some flags a while back, it didn't help much. My results are with -O1. If I use ghc -O0 it makes the binary even bigger.
2024-06-25 23:56:16 +0000 <EvanR> what about -O2
2024-06-25 23:56:51 +0000 <EvanR> also you can try to strip the binary after the fact
2024-06-25 23:57:41 +0000 <joeyadams> Same size with -O2. Does GHC have something like -Os ?
2024-06-25 23:57:50 +0000 <EvanR> -Os
2024-06-25 23:58:31 +0000 <EvanR> guess not...
2024-06-25 23:58:52 +0000 <joeyadams> strip takes the program from 24M to 14M, and the .o file from 2.3M to 1.2M. Better, but still a lot.
2024-06-25 23:59:55 +0000 <joeyadams> (the "program" is just a single .hs file where I copied some of my records over and pruned them. It references aeson, uuid-types, scientific, text, and bytestring.