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