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