| 2024-06-20 00:17:55 +0200 | Midjak | (~MarciZ@82.66.147.146) (Quit: Leaving) |
| 2024-06-20 00:22:46 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 00:30:03 +0200 | <dolio> | I'm not particularly convinced that you're showing that 'dependent types are overkill' when you list multiple features that people want to use dependent types for, and have to be separately grafted onto other languages. |
| 2024-06-20 00:31:09 +0200 | <geekosaur> | that you can use feature X to do thing Y doesn't mean it's the best way to do thing Y |
| 2024-06-20 00:31:59 +0200 | <monochrom> | Good points, both of you. :) |
| 2024-06-20 00:32:01 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-06-20 00:32:07 +0200 | <dolio> | Well, I didn't make the examples. |
| 2024-06-20 00:34:17 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-06-20 00:35:40 +0200 | Eoco | (~ian@128.101.131.218) (Quit: WeeChat 4.1.1) |
| 2024-06-20 00:41:33 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc52cdce3fd1d2726986.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2024-06-20 00:43:04 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Read error: Connection reset by peer) |
| 2024-06-20 00:43:34 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 2024-06-20 00:44:21 +0200 | danse-nr3 | (~danse-nr3@151.35.139.58) (Read error: Connection reset by peer) |
| 2024-06-20 00:45:24 +0200 | danse-nr3 | (~danse-nr3@151.37.122.33) |
| 2024-06-20 00:46:47 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-06-20 00:48:57 +0200 | euleritian | (~euleritia@dynamic-176-001-131-134.176.1.pool.telefonica.de) |
| 2024-06-20 00:53:57 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 268 seconds) |
| 2024-06-20 00:54:15 +0200 | glguy | (g@libera/staff/glguy) (Quit: Quit) |
| 2024-06-20 00:56:40 +0200 | glguy | (g@libera/staff/glguy) |
| 2024-06-20 00:57:50 +0200 | Square2 | (~Square4@user/square) |
| 2024-06-20 00:58:53 +0200 | mud | (~mud@user/kadoban) (Ping timeout: 268 seconds) |
| 2024-06-20 01:01:03 +0200 | Square | (~Square@user/square) (Ping timeout: 255 seconds) |
| 2024-06-20 01:02:02 +0200 | glguy | (g@libera/staff/glguy) (Remote host closed the connection) |
| 2024-06-20 01:03:16 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-06-20 01:03:30 +0200 | glguy | (g@libera/staff/glguy) |
| 2024-06-20 01:03:35 +0200 | danse-nr3 | (~danse-nr3@151.37.122.33) (Ping timeout: 264 seconds) |
| 2024-06-20 01:03:38 +0200 | danza | (~francesco@151.37.122.33) |
| 2024-06-20 01:04:52 +0200 | mud | (~mud@user/kadoban) |
| 2024-06-20 01:08:09 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) |
| 2024-06-20 01:08:45 +0200 | danza | (~francesco@151.37.122.33) (Ping timeout: 268 seconds) |
| 2024-06-20 01:19:39 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection) |
| 2024-06-20 01:24:04 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) |
| 2024-06-20 01:25:04 +0200 | danza | (~francesco@151.37.122.33) |
| 2024-06-20 01:25:24 +0200 | <talismanick> | Is suppressing the "type inference for inner bindings fragile" warning with MonoLocalBinds generally safe? |
| 2024-06-20 01:26:08 +0200 | <talismanick> | or, more precisely, intent- and correctness-preserving |
| 2024-06-20 01:38:16 +0200 | joeyadams | (~joeyadams@2603:6010:5100:2ed:be5c:bfac:9926:c006) |
| 2024-06-20 01:52:14 +0200 | johnw | (~johnw@69.62.242.138) (Ping timeout: 268 seconds) |
| 2024-06-20 01:52:22 +0200 | johnw_ | (~johnw@69.62.242.138) |
| 2024-06-20 01:56:29 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 240 seconds) |
| 2024-06-20 01:59:32 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-06-20 02:00:20 +0200 | hgolden_ | (~hgolden@syn-172-251-233-141.res.spectrum.com) (Remote host closed the connection) |
| 2024-06-20 02:09:38 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2024-06-20 02:10:01 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-06-20 02:10:11 +0200 | euleritian | (~euleritia@dynamic-176-001-131-134.176.1.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2024-06-20 02:12:19 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit) |
| 2024-06-20 02:12:42 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-06-20 02:15:37 +0200 | euleritian | (~euleritia@dynamic-176-002-140-016.176.2.pool.telefonica.de) |
| 2024-06-20 02:22:44 +0200 | whatsupdoc | (uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-20 02:23:41 +0200 | falafel | (~falafel@2a0c:5a87:3103:ec01::62b8) (Ping timeout: 240 seconds) |
| 2024-06-20 02:24:44 +0200 | euleritian | (~euleritia@dynamic-176-002-140-016.176.2.pool.telefonica.de) (Ping timeout: 256 seconds) |
| 2024-06-20 02:26:01 +0200 | euleritian | (~euleritia@dynamic-176-000-200-205.176.0.pool.telefonica.de) |
| 2024-06-20 02:37:47 +0200 | henry40408 | (~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds)) |
| 2024-06-20 02:38:15 +0200 | henry40408 | (~henry4040@175.182.111.183) |
| 2024-06-20 02:38:33 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Quit: Lost terminal) |
| 2024-06-20 02:38:53 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-20 02:42:35 +0200 | euleritian | (~euleritia@dynamic-176-000-200-205.176.0.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 2024-06-20 02:43:29 +0200 | CrunchyFlakes | (~CrunchyFl@146.52.130.128) (Read error: Connection reset by peer) |
| 2024-06-20 02:44:36 +0200 | euleritian | (~euleritia@dynamic-176-006-000-101.176.6.pool.telefonica.de) |
| 2024-06-20 02:45:51 +0200 | CrunchyFlakes | (~CrunchyFl@146.52.130.128) |
| 2024-06-20 02:47:10 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 246 seconds) |
| 2024-06-20 02:50:10 +0200 | segfaultfizzbuzz | (~segfaultf@23-93-189-95.fiber.dynamic.sonic.net) (Remote host closed the connection) |
| 2024-06-20 02:53:28 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 2024-06-20 03:00:03 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-06-20 03:05:39 +0200 | euleritian | (~euleritia@dynamic-176-006-000-101.176.6.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 2024-06-20 03:07:02 +0200 | euleritian | (~euleritia@dynamic-176-006-011-015.176.6.pool.telefonica.de) |
| 2024-06-20 03:09:40 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2024-06-20 03:14:16 +0200 | bionade24 | (~quassel@2a03:4000:33:45b::1) (Remote host closed the connection) |
| 2024-06-20 03:15:25 +0200 | bionade24 | (~quassel@2a03:4000:33:45b::1) |
| 2024-06-20 03:23:39 +0200 | danza | (~francesco@151.37.122.33) (Ping timeout: 264 seconds) |
| 2024-06-20 03:26:54 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection) |
| 2024-06-20 03:32:47 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Quit: ChaiTRex) |
| 2024-06-20 03:36:10 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) |
| 2024-06-20 03:41:01 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) |
| 2024-06-20 03:42:31 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) (Client Quit) |
| 2024-06-20 03:50:59 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 264 seconds) |
| 2024-06-20 03:51:30 +0200 | talismanick | (~user@2601:644:937c:ed10::ae5) |
| 2024-06-20 03:53:11 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-06-20 03:53:56 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 2024-06-20 04:01:41 +0200 | euleritian | (~euleritia@dynamic-176-006-011-015.176.6.pool.telefonica.de) (Ping timeout: 240 seconds) |
| 2024-06-20 04:02:06 +0200 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-06-20 04:03:29 +0200 | petrichor | (~znc-user@user/petrichor) |
| 2024-06-20 04:04:11 +0200 | xff0x | (~xff0x@ai068022.d.east.v6connect.net) (Ping timeout: 264 seconds) |
| 2024-06-20 04:06:31 +0200 | euleritian | (~euleritia@dynamic-176-007-145-030.176.7.pool.telefonica.de) |
| 2024-06-20 04:12:22 +0200 | <monochrom> | Intent requires true AI (not even today's LLM). But if type checking succeeds, it's sound, i.e., as correct as the type system can tell. |
| 2024-06-20 04:13:47 +0200 | <geekosaur> | right, that warning says that you may get unexpected type checking failures because type inference might not work |
| 2024-06-20 04:13:59 +0200 | <geekosaur> | but if it does typecheck, you're fine |
| 2024-06-20 04:14:15 +0200 | <geekosaur> | (or you can just give everything explicit types) |
| 2024-06-20 04:25:10 +0200 | zzz | (~yin@user/zero) (Ping timeout: 268 seconds) |
| 2024-06-20 04:29:48 +0200 | <probie> | Re give everything explicit types: I sometimes wish I had some way to say "should be inferred as having type [α-equivalent to] τ" |
| 2024-06-20 04:33:08 +0200 | <probie> | That way I could write something like `stutter ::[inferred] [a] -> [a]; stutter = foldr (\x xs -> x:x:xs) []` and the compiler can warn me that I've picked a type more specific than what would have been inferred |
| 2024-06-20 04:38:33 +0200 | causal | (~eric@50.35.88.207) |
| 2024-06-20 04:44:53 +0200 | euleritian | (~euleritia@dynamic-176-007-145-030.176.7.pool.telefonica.de) (Ping timeout: 240 seconds) |
| 2024-06-20 04:46:07 +0200 | euleritian | (~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) |
| 2024-06-20 04:53:43 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-06-20 04:56:00 +0200 | td_ | (~td@i53870921.versanet.de) (Ping timeout: 268 seconds) |
| 2024-06-20 04:57:43 +0200 | td_ | (~td@i5387090C.versanet.de) |
| 2024-06-20 04:58:53 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-06-20 05:02:10 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-06-20 05:08:59 +0200 | sam113101 | (~sam@24.157.253.231) (Remote host closed the connection) |
| 2024-06-20 05:15:38 +0200 | xdminsy | (~xdminsy@117.147.70.231) (Quit: Konversation terminated!) |
| 2024-06-20 05:33:40 +0200 | sam113101 | (~sam@24.157.253.231) |
| 2024-06-20 05:43:17 +0200 | aforemny_ | (~aforemny@i59F516D3.versanet.de) |
| 2024-06-20 05:44:39 +0200 | aforemny | (~aforemny@2001:9e8:6cc0:df00:949a:33df:9d68:3e31) (Ping timeout: 264 seconds) |
| 2024-06-20 06:07:21 +0200 | Square2 | (~Square4@user/square) (Read error: Connection reset by peer) |
| 2024-06-20 06:08:23 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds) |
| 2024-06-20 06:09:07 +0200 | iqubic | (~sophia@2601:602:9502:c70:f6b8:a053:cf21:deda) (Ping timeout: 246 seconds) |
| 2024-06-20 06:27:49 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-20 06:31:42 +0200 | sam113101 | (~sam@24.157.253.231) (Remote host closed the connection) |
| 2024-06-20 06:34:27 +0200 | sam113101 | (~sam@24.157.253.231) |
| 2024-06-20 06:42:57 +0200 | michalz | (~michalz@185.246.207.221) |
| 2024-06-20 06:45:10 +0200 | euleritian | (~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-20 06:45:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-20 06:50:50 +0200 | xdminsy | (~xdminsy@117.147.70.231) |
| 2024-06-20 06:51:56 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 268 seconds) |
| 2024-06-20 06:58:17 +0200 | wlhn | (~wenzel@dl46fx8hbfttwvhb-h1ly-3.rev.dnainternet.fi) |
| 2024-06-20 07:00:32 +0200 | darmario | (~MrFox___@user/darmario) |
| 2024-06-20 07:07:49 +0200 | rosco | (~rosco@175.136.155.137) |
| 2024-06-20 07:09:58 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-06-20 07:12:45 +0200 | riatre | (~quassel@2001:310:6000:f::5198:1) (Quit: http://quassel-irc.org) |
| 2024-06-20 07:13:04 +0200 | darmario | (~MrFox___@user/darmario) (Quit: Leaving) |
| 2024-06-20 07:21:18 +0200 | simendsjo | (~user@84.209.170.3) (Ping timeout: 255 seconds) |
| 2024-06-20 07:34:32 +0200 | michalz | (~michalz@185.246.207.221) (Quit: ZNC 1.9.0 - https://znc.in) |
| 2024-06-20 07:37:17 +0200 | michalz | (~michalz@185.246.207.218) |
| 2024-06-20 07:44:37 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc085da20c6dea9e24be.dip0.t-ipconnect.de) |
| 2024-06-20 07:45:16 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-06-20 07:46:05 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-06-20 07:51:08 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 268 seconds) |
| 2024-06-20 08:16:31 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) |
| 2024-06-20 08:18:03 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) (Client Quit) |
| 2024-06-20 08:18:53 +0200 | iqubic | (~sophia@2601:602:9502:c70:6afe:7af5:5891:b32f) |
| 2024-06-20 08:22:02 +0200 | riatre | (~quassel@2001:310:6000:f::5198:1) |
| 2024-06-20 08:27:16 +0200 | joeyadams | (~joeyadams@2603:6010:5100:2ed:be5c:bfac:9926:c006) (Quit: Leaving) |
| 2024-06-20 08:32:03 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 264 seconds) |
| 2024-06-20 08:32:03 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) |
| 2024-06-20 08:33:52 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-06-20 08:36:27 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 08:38:33 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-06-20 08:40:13 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-06-20 08:40:29 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-06-20 08:43:13 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 256 seconds) |
| 2024-06-20 08:45:38 +0200 | euleritian | (~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) |
| 2024-06-20 08:46:02 +0200 | euleritian | (~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-20 08:46:04 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) |
| 2024-06-20 08:47:46 +0200 | euleritian | (~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) |
| 2024-06-20 08:49:47 +0200 | euleritian | (~euleritia@dynamic-176-007-156-210.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-20 08:50:05 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-06-20 08:52:11 +0200 | ft | (~ft@p3e9bcb39.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-06-20 08:54:26 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 252 seconds) |
| 2024-06-20 08:55:05 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-06-20 09:08:31 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:309b:a5ab:1320:adb2) (Ping timeout: 268 seconds) |
| 2024-06-20 09:09:54 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 256 seconds) |
| 2024-06-20 09:09:55 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:89e:9b05:41f1:3af8) |
| 2024-06-20 09:13:43 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 2024-06-20 09:15:18 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) (Quit: Quit) |
| 2024-06-20 09:30:02 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 09:38:40 +0200 | danse-nr3 | (~danse-nr3@151.57.10.250) |
| 2024-06-20 09:44:00 +0200 | manwithluck | (manwithluc@gateway/vpn/protonvpn/manwithluck) |
| 2024-06-20 09:48:00 +0200 | dcoutts__ | (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 255 seconds) |
| 2024-06-20 09:52:11 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 2024-06-20 09:55:59 +0200 | <tomsmeding> | a tag to check that this is not only a valid type, but is actually a _most general_ type for the definition? |
| 2024-06-20 09:56:01 +0200 | <tomsmeding> | interesting |
| 2024-06-20 09:58:47 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-20 10:02:28 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-06-20 10:04:43 +0200 | rosco | (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 2024-06-20 10:12:33 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-06-20 10:16:21 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-06-20 10:17:21 +0200 | <dminuoso> | That seems a bit weird. Isn't the goal of Damas Milner type inference to already give you "the most general type"? |
| 2024-06-20 10:17:59 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) (Ping timeout: 264 seconds) |
| 2024-06-20 10:18:16 +0200 | rosco | (~rosco@175.136.155.137) |
| 2024-06-20 10:18:31 +0200 | <dminuoso> | How would the type checker know of "a more general type" to begin with? |
| 2024-06-20 10:19:00 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) (Quit: Leaving) |
| 2024-06-20 10:19:28 +0200 | <dminuoso> | I mean "should be inferred as having type [α-equivalent to] τ" can be stated by `x :: τ` |
| 2024-06-20 10:20:24 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) |
| 2024-06-20 10:21:15 +0200 | <dminuoso> | Ohh I think as I was writing about it, I understood. |
| 2024-06-20 10:22:21 +0200 | <dminuoso> | So a kind of `x :: τ; x :: _` as if it were? |
| 2024-06-20 10:22:28 +0200 | <ncf> | they want an synthesized-then-checked type ascription, presumably |
| 2024-06-20 10:22:53 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-06-20 10:24:01 +0200 | Luj | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 2024-06-20 10:24:50 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) |
| 2024-06-20 10:24:56 +0200 | <ncf> | Γ ⊢ x => τ Γ ⊢ x <= τ |
| 2024-06-20 10:24:57 +0200 | <ncf> | ----------------- as opposed to ----------------- |
| 2024-06-20 10:24:58 +0200 | <ncf> | Γ ⊢ (x :: τ) => τ Γ ⊢ (x :: τ) => τ |
| 2024-06-20 10:26:48 +0200 | <ChrisTrac> | hi, I'm playing with GHC.Exts.withDict and am wondering if there's a way to instantiate a class with multiple methods? I'm using QuickCheck, and want to define `Gen a` values rather than instantiating `Arbitrary`; but lots of existing generators have `Arbitrary a` constraints that I can't satisfy. |
| 2024-06-20 10:29:09 +0200 | <ChrisTrac> | (the usual alternative is to define a load of newtypes, but I've got LOTS of nested datatypes that makes that a pain; but they're Generic so I can auto-generate a lot of Gen values easily) |
| 2024-06-20 10:30:28 +0200 | <tomsmeding> | dminuoso: they want that `x ::[inferred] Int ; x = 42` would fail because that's less general than `x :: Num a => a` |
| 2024-06-20 10:31:06 +0200 | <tomsmeding> | ChrisTrac: have you considered using hedgehog instead? :) |
| 2024-06-20 10:31:28 +0200 | <tomsmeding> | it's designed around providing explicit generators, instead of relying on an Arbitrary type class |
| 2024-06-20 10:32:17 +0200 | <ChrisTrac> | heh, I'm actually more of a fan of falsify; this project already uses QuickCheck in parts, so I'm after a path of least-resistance |
| 2024-06-20 10:32:44 +0200 | <tomsmeding> | generating type class evidence out of thin air is always a dangerous endeavour |
| 2024-06-20 10:33:17 +0200 | <ChrisTrac> | yeah, unsafeCoerce can do it; but that's worse than just writing a mountain of instances IMHO |
| 2024-06-20 10:33:23 +0200 | <tomsmeding> | I don't think there's a supported way apart from withDict |
| 2024-06-20 10:33:33 +0200 | <tomsmeding> | (which only works for single-method classes) |
| 2024-06-20 10:33:55 +0200 | <tomsmeding> | (and even withDict is not meant to be used lightly) |
| 2024-06-20 10:34:53 +0200 | <ChrisTrac> | I tried making my own single-method `class Arb a where arb :: Gen a`, which works fine for withDict; but I can't use that to satisfy an existing Arbitrary constraint :( |
| 2024-06-20 10:36:45 +0200 | euleritian | (~euleritia@77.22.252.56) (Read error: Connection reset by peer) |
| 2024-06-20 10:37:08 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-20 10:39:31 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-06-20 10:40:01 +0200 | <Leary> | ChrisTrac: You can if you get nasty. If you write `newtype FromArb a = FromArb a; instance Arb a => Arbitrary (FromArb a)`, then you can turn `Gen a ->` into `Arb a =>` with `withDict`, which gives you `Arbitrary (FromArb a)`, which you can capture with `data Dict c = c => Dict`, and safely `unsafeCoerce` to `Dict (Arbitrary a)`. |
| 2024-06-20 10:40:21 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-20 10:40:59 +0200 | <danse-nr3> | hmm "safely unsafeCoerce" |
| 2024-06-20 10:41:44 +0200 | <ChrisTrac> | Leary: Yeah, it seems like there's inevitably an `unsafeCoerce` (whether directly, or indirectly via a library like `constraints`) |
| 2024-06-20 10:42:33 +0200 | <Leary> | In my opinion, `withDict` is actually more dangerous than `unsafeCoerce` where you know the representation matches. |
| 2024-06-20 10:44:09 +0200 | <tomsmeding> | and how do we all know that ghc will pick the Arbitrary constraint we're trying to pass, and not some other floating around? |
| 2024-06-20 10:44:11 +0200 | <ChrisTrac> | Leary: how so? I thought withDict just fails to find an instance (a compile error), whilst unsafeCoerce can cause segfaults, etc. |
| 2024-06-20 10:44:47 +0200 | dcoutts__ | (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) |
| 2024-06-20 10:45:27 +0200 | <ChrisTrac> | tomsmeding: in this case it's "morally coherent", in that I don't care which is picked (I just want one, any one) |
| 2024-06-20 10:46:54 +0200 | <Leary> | I'll re-emphasise: /where you know the representation matches/ |
| 2024-06-20 10:47:43 +0200 | <danse-nr3> | `withDict` seems an advanced function indeed, was not familiar with it |
| 2024-06-20 10:47:57 +0200 | <Leary> | Using it to erase a newtype obviously cannot cause a segfault; it's more like reaching for internals that weren't exposed. |
| 2024-06-20 10:48:58 +0200 | <tomsmeding> | and "knowing that the representation matches" is not? :p |
| 2024-06-20 10:49:52 +0200 | <tomsmeding> | (I'm not saying that you can't do what you're suggesting -- I'm just saying that depending on knowledge about internal representation, for which you can't even explicitly tell the compiler that you're depending on it, is dangerous) |
| 2024-06-20 10:52:43 +0200 | <Leary> | `newtype`s are language-guaranteed to share the same representation as the type they wrap? |
| 2024-06-20 10:52:46 +0200 | <ChrisTrac> | I think coercing between representational types (e.g. newtype wrappers) is fine; coercing between GHC's current dictionary representations is where it gets hairy (i.e. where we're depending on the Core structure) |
| 2024-06-20 10:53:47 +0200 | <danse-nr3> | but then... whey would you coerce between newtype wrappers? |
| 2024-06-20 10:53:51 +0200 | <danse-nr3> | *why |
| 2024-06-20 10:54:13 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-06-20 10:54:18 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-06-20 10:54:50 +0200 | <ChrisTrac> | danse-nr3: classic examples are Monoid instances for `Sum Int`, `Product Int`, `Min Int`, `Max Int`, etc. (where all those wrappers are newtypes) |
| 2024-06-20 10:56:42 +0200 | <Leary> | ChrisTrac: What I'm suggesting is only `unsafeCoerce :: Dict (Arbitrary (FromArb a)) -> Dict (Arbitrary a)`. This doesn't depend on anything the language doesn't guarantee; it's only a threat to coherence, same as `withDict`. |
| 2024-06-20 10:56:52 +0200 | <danse-nr3> | i get it can be handy, i guess i would prefer to find a way that plays well with the type system |
| 2024-06-20 10:57:54 +0200 | <tomsmeding> | Leary: hm, I guess -- as long as you know that all methods of Arbitrary use the type variable at most representationally |
| 2024-06-20 10:59:03 +0200 | <tomsmeding> | how do I get ghci to print roles for a newtype again? |
| 2024-06-20 10:59:04 +0200 | <Leary> | Right, that's a point worthy of note. |
| 2024-06-20 10:59:42 +0200 | <ChrisTrac> | danse-nr3: say you `getSum (mappend (map Sum myBigListOfInts))`, the `Sum` and `getSum` are no-ops, so zero-overhead; but we might end up running `map` over the list, wasting resources (depends on optimisations; even if lists get optimised away, more complicated structures might not). We can replace the `map Sum` with coerce to ensure it's |
| 2024-06-20 10:59:43 +0200 | <ChrisTrac> | definitely a no-op (and the type-checker will ensure it's safe) |
| 2024-06-20 11:00:00 +0200 | AlexNoo_ | AlexNoo |
| 2024-06-20 11:00:01 +0200 | <tomsmeding> | but that's _coerce_, not _unsafeCoerce_ |
| 2024-06-20 11:00:14 +0200 | <tomsmeding> | with unsafeCoerce it's up to you to check that there is indeed representational equality |
| 2024-06-20 11:00:29 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-06-20 11:00:29 +0200 | <tomsmeding> | the language does not, really, guarantee anything about the representation of dictionaries in something like the Dict type |
| 2024-06-20 11:00:38 +0200 | chele | (~chele@user/chele) |
| 2024-06-20 11:01:25 +0200 | <tomsmeding> | so with the Leary's unsafeCoerce trick we're still depending on the fact that whatever that runtime representation of type class evidence is, this representation is the same for representationally equal type parameters |
| 2024-06-20 11:01:33 +0200 | <tomsmeding> | Haskell2010 does not guarantee that |
| 2024-06-20 11:01:43 +0200 | <tomsmeding> | it's _true_ in GHC |
| 2024-06-20 11:03:27 +0200 | <tomsmeding> | and the fact that I can't think of a different, still sensible implementation notwithstanding :p |
| 2024-06-20 11:05:37 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Ping timeout: 250 seconds) |
| 2024-06-20 11:15:47 +0200 | <danse-nr3> | interesting. `coerce` does not even feel that coercing :) |
| 2024-06-20 11:15:58 +0200 | danse-nr3 | wonders whether a `cast` exists |
| 2024-06-20 11:16:01 +0200 | <danse-nr3> | @hoogle cast |
| 2024-06-20 11:16:02 +0200 | <lambdabot> | Data.Typeable cast :: forall a b . (Typeable a, Typeable b) => a -> Maybe b |
| 2024-06-20 11:16:02 +0200 | <lambdabot> | Protolude cast :: (Typeable a, Typeable b) => a -> Maybe b |
| 2024-06-20 11:16:02 +0200 | <lambdabot> | BasePrelude cast :: (Typeable a, Typeable b) => a -> Maybe b |
| 2024-06-20 11:16:19 +0200 | <danse-nr3> | @hoogle coerce |
| 2024-06-20 11:16:20 +0200 | <lambdabot> | Data.Coerce coerce :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) . Coercible a b => a -> b |
| 2024-06-20 11:16:20 +0200 | <lambdabot> | GHC.Exts coerce :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) . Coercible a b => a -> b |
| 2024-06-20 11:16:20 +0200 | <lambdabot> | Control.Lens.Internal.Coerce coerce :: Coercible a b => a -> b |
| 2024-06-20 11:19:32 +0200 | <mauke> | @hoogle reify |
| 2024-06-20 11:19:33 +0200 | <lambdabot> | Language.Haskell.TH reify :: Name -> Q Info |
| 2024-06-20 11:19:33 +0200 | <lambdabot> | Language.Haskell.TH.Syntax reify :: Name -> Q Info |
| 2024-06-20 11:19:33 +0200 | <lambdabot> | Hedgehog.Internal.State reify :: HTraversable t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete) |
| 2024-06-20 11:19:37 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) |
| 2024-06-20 11:23:51 +0200 | <tomsmeding> | @hoogle reflect |
| 2024-06-20 11:23:52 +0200 | <lambdabot> | Pipes.Core reflect :: Functor m => Proxy a' a b' b m r -> Proxy b b' a a' m r |
| 2024-06-20 11:23:52 +0200 | <lambdabot> | Data.Reflection reflect :: Reifies s a => proxy s -> a |
| 2024-06-20 11:23:52 +0200 | <lambdabot> | Control.Monad.Logic.Class reflect :: MonadLogic m => Maybe (a, m a) -> m a |
| 2024-06-20 11:24:17 +0200 | danse-nr3 | raises eyebrow |
| 2024-06-20 11:24:31 +0200 | <tomsmeding> | ¯\_(ツ)_/¯ |
| 2024-06-20 11:24:37 +0200 | <danse-nr3> | =D |
| 2024-06-20 11:27:45 +0200 | kuribas | (~user@ptr-17d51emfywuvjswcfv8.18120a2.ip6.access.telenet.be) |
| 2024-06-20 11:28:39 +0200 | gawen | (~gawen@user/gawen) (Quit: cya) |
| 2024-06-20 11:34:42 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Quit: Client closed) |
| 2024-06-20 11:36:20 +0200 | gawen | (~gawen@user/gawen) |
| 2024-06-20 11:42:37 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 2024-06-20 11:43:36 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) |
| 2024-06-20 11:43:38 +0200 | <mreh> | I'm rather inspired by servant and beam to create some kind of depently typed eDSL to generate (limited for now) OpenGL pipelines. |
| 2024-06-20 11:44:04 +0200 | <mreh> | The amount of boilerplate I have to write doing OpenGL currently. |
| 2024-06-20 11:45:06 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-06-20 11:45:21 +0200 | gehmehgeh | gmg |
| 2024-06-20 11:46:24 +0200 | gmg | (~user@user/gehmehgeh) (Client Quit) |
| 2024-06-20 11:49:18 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-06-20 11:52:03 +0200 | TonyStone | (~TonyStone@user/TonyStone) (Ping timeout: 260 seconds) |
| 2024-06-20 11:57:25 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) |
| 2024-06-20 11:59:58 +0200 | dequbed | (~dequbed@banana-new.kilobyte22.de) |
| 2024-06-20 12:01:09 +0200 | madhavanmiui | (~madhavanm@2409:40f4:ae:dd09:8000::) (Client Quit) |
| 2024-06-20 12:03:32 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2024-06-20 12:04:40 +0200 | TonyStone | (~TonyStone@user/TonyStone) |
| 2024-06-20 12:05:20 +0200 | <danse-nr3> | does nothing like that already exist mreh? |
| 2024-06-20 12:05:33 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-06-20 12:06:36 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 255 seconds) |
| 2024-06-20 12:06:38 +0200 | gehmehgeh | gmg |
| 2024-06-20 12:06:41 +0200 | gawen | (~gawen@user/gawen) (Quit: cya) |
| 2024-06-20 12:10:27 +0200 | <mreh> | danse-nr3: There are DSLs and eDSLs, but I don't think they can exclude many runtime errors, say for example I don't have a vertex buffer object bound with the right kind of data in it with the right attribute pointer for my vertex shader. |
| 2024-06-20 12:11:38 +0200 | <danse-nr3> | oh had overlooked the "dependently typed" part. Good luck then |
| 2024-06-20 12:12:12 +0200 | <mreh> | The eDSLs I've found are also not well documented. Lambdacube looks good, but I didn't fancy it since it's its own language with its own toolchain. |
| 2024-06-20 12:13:01 +0200 | <danse-nr3> | i assume good doc is also a matter of how much collaboration one can get on their project |
| 2024-06-20 12:13:15 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc085da20c6dea9e24be.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2024-06-20 12:13:59 +0200 | <mreh> | danse-nr3: probably. They're also mostly all around 10 years old and dependent types and OpenGL have come along a lot since then. |
| 2024-06-20 12:14:23 +0200 | gawen | (~gawen@user/gawen) |
| 2024-06-20 12:14:28 +0200 | <danse-nr3> | but we've got "fearless refactoring" |
| 2024-06-20 12:14:44 +0200 | danse-nr3 | is not trying to get mreh collaborating on an existing project at all |
| 2024-06-20 12:14:51 +0200 | ChrisTrac91 | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) |
| 2024-06-20 12:15:00 +0200 | <mreh> | danse-nr3: go on :) |
| 2024-06-20 12:15:05 +0200 | <danse-nr3> | :P |
| 2024-06-20 12:15:28 +0200 | <mreh> | do you have something of your own in mind? |
| 2024-06-20 12:15:54 +0200 | <danse-nr3> | nope, i just saw a lot of projects start, get no traction and eventually be abandoned |
| 2024-06-20 12:16:45 +0200 | <mreh> | yeah, I know right. I'm going to be the primary user of it |
| 2024-06-20 12:17:04 +0200 | <mreh> | so there will be an enthusiastic development team behind it |
| 2024-06-20 12:17:59 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Ping timeout: 250 seconds) |
| 2024-06-20 12:18:33 +0200 | <mreh> | lack of traction in the case of the others is probably because of no doc and incompleteness |
| 2024-06-20 12:18:47 +0200 | <danse-nr3> | an enthusiastic team of 1 you mean? (: |
| 2024-06-20 12:18:55 +0200 | <mreh> | danse-nr3: damn right |
| 2024-06-20 12:19:07 +0200 | <mreh> | even lambdacube is hard to get into |
| 2024-06-20 12:19:51 +0200 | <danse-nr3> | enthusiastic & a bit lonely. Not uncommon in haskell land but also not necessarily the only way |
| 2024-06-20 12:21:12 +0200 | <mreh> | there seems to be a bit of a haskell boom going on right now |
| 2024-06-20 12:21:28 +0200 | ChrisTrac91 | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Ping timeout: 250 seconds) |
| 2024-06-20 12:21:28 +0200 | <danse-nr3> | "a bit of a boom"? |
| 2024-06-20 12:22:22 +0200 | <mreh> | I see lots of mainstream influencers talking about it |
| 2024-06-20 12:28:12 +0200 | cfricke | (~cfricke@user/cfricke) (Ping timeout: 255 seconds) |
| 2024-06-20 12:30:51 +0200 | noumenon | (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 2024-06-20 12:34:29 +0200 | danse-nr3 | (~danse-nr3@151.57.10.250) (Ping timeout: 268 seconds) |
| 2024-06-20 12:35:06 +0200 | sprout | (~quassel@2a02-a448-3a80-0-758a-35d7-4890-aab6.fixed6.kpn.net) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2024-06-20 12:35:29 +0200 | sprout | (~quassel@2a02-a448-3a80-0-d1d9-fee0-140e-a81b.fixed6.kpn.net) |
| 2024-06-20 12:41:53 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-06-20 12:53:42 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:b0fb:c3f5:4666:ad2f) |
| 2024-06-20 12:55:15 +0200 | piele_ | (~piele@tbonesteak.creativeserver.net) (Remote host closed the connection) |
| 2024-06-20 12:56:28 +0200 | piele | (~piele@tbonesteak.creativeserver.net) |
| 2024-06-20 13:04:44 +0200 | xff0x | (~xff0x@ai068022.d.east.v6connect.net) |
| 2024-06-20 13:07:05 +0200 | mmohammadi9812 | (~mohammad@85.185.34.203) |
| 2024-06-20 13:09:31 +0200 | danza | (~francesco@151.43.26.19) |
| 2024-06-20 13:22:58 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) |
| 2024-06-20 13:24:56 +0200 | CiaoSen | (~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03) |
| 2024-06-20 13:26:53 +0200 | danza | (~francesco@151.43.26.19) (Ping timeout: 240 seconds) |
| 2024-06-20 13:28:34 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-06-20 13:33:19 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-06-20 13:34:21 +0200 | ChrisTrac | (~ChrisTrac@cpc116330-smal16-2-0-cust397.19-1.cable.virginm.net) (Quit: Client closed) |
| 2024-06-20 13:40:28 +0200 | CiaoSen | (~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 2024-06-20 13:45:33 +0200 | andrewboltachev | (~andrey@178.141.121.180) |
| 2024-06-20 13:46:16 +0200 | <andrewboltachev> | Hi. Do I understand correctly that `mtl` is much more recommended to use than `trnasformers`? |
| 2024-06-20 13:46:44 +0200 | danse-nr3 | (~danse-nr3@151.43.38.52) |
| 2024-06-20 13:47:47 +0200 | <andrewboltachev> | I have a challenge of adding one more monad to here (StateT): https://github.com/andrewboltachev/matcher/blob/master/src/Logicore/Matcher/Core.hs#L468 so will transition to MTL make such things easier? |
| 2024-06-20 13:54:58 +0200 | dcoutts__ | (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2024-06-20 13:57:33 +0200 | <mreh> | transformers is a dependency of mtl |
| 2024-06-20 13:58:08 +0200 | <mreh> | andrewboltachev: ^ |
| 2024-06-20 13:59:53 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2024-06-20 14:00:32 +0200 | <mreh> | you have to use transformers if you need to write Haskell98, otherwise mtl has some nice features |
| 2024-06-20 14:01:12 +0200 | <mreh> | since mtl uses some Language extensions, it's GHC only I believe |
| 2024-06-20 14:01:55 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-06-20 14:04:34 +0200 | dcoutts__ | (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) |
| 2024-06-20 14:06:49 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc085da20c6dea9e24be.dip0.t-ipconnect.de) |
| 2024-06-20 14:07:34 +0200 | <mreh> | simply put, mtl doesn't require you to litter your code with `lift` when using transformer stacks |
| 2024-06-20 14:10:12 +0200 | <andrewboltachev> | mreh: yes, this seems clear. I have things like that when I need to "ask" (so, not even lift): https://github.com/andrewboltachev/matcher/blob/master/src/Logicore/Matcher/Core.hs#L946 |
| 2024-06-20 14:12:21 +0200 | <mreh> | yeah, so MatchStatusT could derive the class MonadReader if you were using mtl |
| 2024-06-20 14:12:37 +0200 | <mreh> | you could make MatchStatusT a type synonym and get that for free |
| 2024-06-20 14:13:10 +0200 | <mreh> | or use newtype deriving |
| 2024-06-20 14:14:09 +0200 | <mreh> | that would also apply to the other typeclasses, like Monad, Functor, Applicative... |
| 2024-06-20 14:15:20 +0200 | <mreh> | nothing to do with mtl in the latter case, but something I noticed about the code |
| 2024-06-20 14:16:19 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-06-20 14:21:17 +0200 | Buggys | (Buggys@shelltalk.net) (Quit: IRCNow and Forever!) |
| 2024-06-20 14:26:35 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-06-20 14:31:35 +0200 | Pixi | (~Pixi@user/pixi) (Ping timeout: 252 seconds) |
| 2024-06-20 14:32:29 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Quit: Lost terminal) |
| 2024-06-20 14:35:40 +0200 | mmohammadi9812 | (~mohammad@85.185.34.203) (Ping timeout: 268 seconds) |
| 2024-06-20 14:37:13 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2024-06-20 14:38:49 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 2024-06-20 14:45:47 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 2024-06-20 14:50:57 +0200 | <andrewboltachev> | mreh: I guess this one is also should be called MatchStatusM (by convention)? |
| 2024-06-20 14:51:09 +0200 | <andrewboltachev> | the type synonym |
| 2024-06-20 14:51:46 +0200 | Pixi | (~Pixi@user/pixi) |
| 2024-06-20 14:52:27 +0200 | <mreh> | andrewboltachev: not sure I follow you |
| 2024-06-20 14:53:40 +0200 | <andrewboltachev> | you said above: you could make MatchStatusT a type synonym and get that for free |
| 2024-06-20 14:54:21 +0200 | <andrewboltachev> | I know that sonetimes that "top-level monads" are defined as type synonyms and also called like AppM, ResponderM etc |
| 2024-06-20 14:55:18 +0200 | <andrewboltachev> | I always thought that that "M" means sth special |
| 2024-06-20 14:55:34 +0200 | <mreh> | oh right yeah, it just means Monad usually! |
| 2024-06-20 14:57:05 +0200 | <andrewboltachev> | well I think I've got the idea of what mtl is now |
| 2024-06-20 14:57:49 +0200 | <mreh> | why not call it something like `Match`? |
| 2024-06-20 14:58:43 +0200 | <andrewboltachev> | might be |
| 2024-06-20 14:59:32 +0200 | <edwardk> | andrewboltachev: 'transformers' is the base upon which 'mtl' is built. if you dont want to use mtl, but want to use some other mechanism, like, say, the ill-advised monads-tf package or whatever, or some effect system that might just use the mtl to write out the code of a handler or two, then this lets you share the base transformers, while retaining the option of dispatching classes in a different way. |
| 2024-06-20 15:00:23 +0200 | <edwardk> | the main scenario where this split is useful is that you might import only transformers if you want to provide instances for your own class for its data types, rather than import all of mtl. |
| 2024-06-20 15:00:31 +0200 | <edwardk> | but this is pretty much a tiny wibble |
| 2024-06-20 15:01:20 +0200 | <andrewboltachev> | so the idea is that I shouldn't implement MatchStatusT's MonadTrans instance? |
| 2024-06-20 15:01:36 +0200 | <edwardk> | no. you should implement all the things |
| 2024-06-20 15:02:41 +0200 | <edwardk> | let's look at that type for a sec. |
| 2024-06-20 15:02:45 +0200 | <edwardk> | newtype MatchStatusT m a = MatchStatusT { runMatchStatusT :: ReaderT MatcherEnv m (MatchStatus a) } |
| 2024-06-20 15:03:10 +0200 | <edwardk> | ok, so you have a readerT, and some match status thing. i've literally never read this code before so give me a sec. |
| 2024-06-20 15:03:42 +0200 | <edwardk> | data MatchStatus a = MatchSuccess a| MatchFailure T.Text| NoMatch T.Text deriving (Eq, Show) |
| 2024-06-20 15:04:28 +0200 | <edwardk> | ok, so that is purely an error type. so this is basicaly ReaderT MatcherEnv (EitherT MatchFailure m) a |
| 2024-06-20 15:04:38 +0200 | <edwardk> | for some notion of match failure that covers the two cases in matchstatus |
| 2024-06-20 15:05:07 +0200 | <andrewboltachev> | so, yes. it's like Either but with extra state |
| 2024-06-20 15:05:33 +0200 | <mreh> | did you intend MatchStatus to be at the bottom of the stack? |
| 2024-06-20 15:05:36 +0200 | <edwardk> | now you have a couple of options. if you want the _user_ to be reaching into that MatcherEnv using ask/asks you can implement MonadReader for MatchStatusT. if you want the _user_ to be responding to failures and extracting that information you can implement MonadError |
| 2024-06-20 15:06:29 +0200 | <edwardk> | and mreh has a good point. MatchStatus = MatchStatusT Identity is what one would expect, but you used it for the MatchResult type more or less |
| 2024-06-20 15:07:45 +0200 | <edwardk> | if the stuff in the MatcherEnv is for 'you' and you expect it to be tricky for users to maintain its invariants it may make sense not to implement the MonadReader instance for it. because then you can implement MonadReader e (MatchStatusT m) for whatever m offers! |
| 2024-06-20 15:07:49 +0200 | <andrewboltachev> | mreh: I'm not even sure |
| 2024-06-20 15:08:19 +0200 | <edwardk> | the user can then ask/asks/local that rather than get tripped up by the fact that you have some administrative environmental stuff out in MatchStatusT |
| 2024-06-20 15:08:50 +0200 | <mreh> | also should MatchStatusT even be a transformer? another question I would ask myself |
| 2024-06-20 15:09:03 +0200 | <mreh> | you might already know the answer |
| 2024-06-20 15:09:11 +0200 | <edwardk> | do you want users 'matching with monadic side-effects?' |
| 2024-06-20 15:09:12 +0200 | <mreh> | (just asking :) |
| 2024-06-20 15:09:28 +0200 | <edwardk> | e.g. running IO-actions that might launch missiles while you haven't even resolved the match |
| 2024-06-20 15:09:51 +0200 | <edwardk> | what is the semantics you want to assign to matching, basically |
| 2024-06-20 15:09:51 +0200 | <andrewboltachev> | print :-) |
| 2024-06-20 15:10:03 +0200 | <mreh> | "my JSON doesn't match, time to turn on the coffee machine" |
| 2024-06-20 15:10:10 +0200 | <andrewboltachev> | so btw |
| 2024-06-20 15:10:17 +0200 | <edwardk> | you can include that in the mix, just be warned you're loading a footgun |
| 2024-06-20 15:11:10 +0200 | <andrewboltachev> | https://www.dropbox.com/scl/fi/iyutvisq8v6arlj5ppuf8/2024-06-20-16-10-33.png?rlkey=ej84tfvumvfoh3w… |
| 2024-06-20 15:11:47 +0200 | <andrewboltachev> | this is a "python code schema" that I made encoded as python code to match python code and extract patterns from it |
| 2024-06-20 15:12:33 +0200 | <edwardk> | looks like you're building up a 'bigger and bigger' stuck term for all the elimination forms being applied to some initial stuck object, like one does in a normalization by evaluation interpreter |
| 2024-06-20 15:13:15 +0200 | <andrewboltachev> | I also dealt with Figma files for example (yet the type is clear so there's not so much to match) but just as an example of big data structure (100s of MB) - I read/write some preliminary results into Redis for example |
| 2024-06-20 15:13:28 +0200 | <edwardk> | want to see what a lambda does? pass this sort of thing in as an argument and see what the lambda does to the argument. |
| 2024-06-20 15:13:58 +0200 | <andrewboltachev> | uhm |
| 2024-06-20 15:15:05 +0200 | <edwardk> | andrewboltachev: https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf is a walkthrough of building something kind of similar for a simple lambda calculus implemented in haskell |
| 2024-06-20 15:16:34 +0200 | <andrewboltachev> | interesting. I still thought that I'm building more like a... lens |
| 2024-06-20 15:17:19 +0200 | <mreh> | you're talking to the right man |
| 2024-06-20 15:18:39 +0200 | <edwardk> | if what you wrote is what i think you wrote, its like a big sticky ball of tar that any attempt to invoke it as a function gets turned into a bigger ball of tar that represents 'hey this is the result of calling that previous thing with this argument' or invoking && on it captures 'hey this is the result of calling && with some other argument on that base thing'. so if it gets returned as part of the result of a function it 'traces' what |
| 2024-06-20 15:18:39 +0200 | <edwardk> | was done relative to the input to the function. |
| 2024-06-20 15:19:14 +0200 | <edwardk> | chuck the ball of tar in, see what comes out stuck to it |
| 2024-06-20 15:19:28 +0200 | <edwardk> | this is the essence of NBE ;) |
| 2024-06-20 15:20:03 +0200 | <edwardk> | mreh: hah |
| 2024-06-20 15:20:14 +0200 | <andrewboltachev> | aha. but the trick is, there's always some more theory |
| 2024-06-20 15:20:59 +0200 | <andrewboltachev> | I'm in my spare time going through "Elementary categories elementary toposes" book and it doesn't seem to end very soon. 287 pages but ~500 theorems or so |
| 2024-06-20 15:21:48 +0200 | <edwardk> | andrewboltachev: that's the good part. without more theory you are stuck inventing it all from scratch and you can miss good stuff! ;) |
| 2024-06-20 15:22:25 +0200 | <andrewboltachev> | well, thanks :-) I'll keep that |
| 2024-06-20 15:23:31 +0200 | <andrewboltachev> | pretty much the biggest theoretical discovery I made is that: (MatchStringExact "abc") (i.e. the "type" that only has one object) is a final object |
| 2024-06-20 15:24:13 +0200 | <edwardk> | what are your morphisms? |
| 2024-06-20 15:24:43 +0200 | <andrewboltachev> | well that's just like in Set |
| 2024-06-20 15:25:03 +0200 | <edwardk> | so these are functions that take sets of strings to sets of strings? |
| 2024-06-20 15:25:57 +0200 | <andrewboltachev> | Say, all the types of JSON (Aeson) |
| 2024-06-20 15:26:14 +0200 | Pixi` | (~Pixi@user/pixi) |
| 2024-06-20 15:26:15 +0200 | <andrewboltachev> | (MatchStringExact "abc") is a set of one string |
| 2024-06-20 15:27:04 +0200 | <edwardk> | or do you have something like a 'is more specific than' thing where a -> b shows json objet that would parse into 'a' should parse in 'b', which behaves kind of like set^op. |
| 2024-06-20 15:27:46 +0200 | <edwardk> | the ltter is more like a powerset, which pushes you contravariant, and then breaks your current intution |
| 2024-06-20 15:27:46 +0200 | <andrewboltachev> | this function that I have: https://github.com/andrewboltachev/matcher/blob/master/src/Logicore/Matcher/Core.hs#L1766 given a grammar (MatchPattern) is meant to eliminate the "static" part of that grammar... |
| 2024-06-20 15:28:08 +0200 | <andrewboltachev> | static part of data* |
| 2024-06-20 15:28:23 +0200 | Pixi` | (~Pixi@user/pixi) (Read error: Connection reset by peer) |
| 2024-06-20 15:28:48 +0200 | Pixi` | (~Pixi@user/pixi) |
| 2024-06-20 15:29:03 +0200 | Pixi | (~Pixi@user/pixi) (Ping timeout: 260 seconds) |
| 2024-06-20 15:29:25 +0200 | <andrewboltachev> | https://dpaste.com/DWWJLDHCC#wrap |
| 2024-06-20 15:29:42 +0200 | <andrewboltachev> | that "w" aka whitespace is eliminated |
| 2024-06-20 15:30:31 +0200 | Pixi__ | (~Pixi@user/pixi) |
| 2024-06-20 15:32:30 +0200 | <andrewboltachev> | ah, sorry, this is the correct example: https://dpaste.com/4FPGJMZ7J#wrap |
| 2024-06-20 15:34:17 +0200 | Pixi` | (~Pixi@user/pixi) (Ping timeout: 252 seconds) |
| 2024-06-20 15:34:29 +0200 | <andrewboltachev> | idea is that "b" is already "terminal object", so we can throw it away, and deal with "a" (provide another value for it) and then re-create the whole structure. the whitespace-like stuff is another beast I'm trying to support |
| 2024-06-20 15:35:46 +0200 | <andrewboltachev> | so product of terminal objects is itself a terminal object ('cause when you multiply by 1 you got the same number) |
| 2024-06-20 15:36:37 +0200 | <andrewboltachev> | and that's exactly what I have to eliminate (to write this function called `matchResultToThinValueFAlgebra` correctly) |
| 2024-06-20 15:37:30 +0200 | <andrewboltachev> | thanks for help and support mreh edwardk :-) |
| 2024-06-20 15:39:42 +0200 | caubert_ | (~caubert@user/caubert) (Read error: Connection reset by peer) |
| 2024-06-20 15:40:02 +0200 | caubert | (~caubert@user/caubert) |
| 2024-06-20 15:49:33 +0200 | ocra8 | (~ocra8@user/ocra8) |
| 2024-06-20 16:00:13 +0200 | ystael | (~ystael@user/ystael) |
| 2024-06-20 16:07:43 +0200 | <mreh> | andrewboltachev: np |
| 2024-06-20 16:14:25 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-06-20 16:18:13 +0200 | andrewboltachev | (~andrey@178.141.121.180) (Quit: Leaving.) |
| 2024-06-20 16:19:26 +0200 | euleritian | (~euleritia@dynamic-176-007-169-090.176.7.pool.telefonica.de) |
| 2024-06-20 16:22:03 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-06-20 16:35:15 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 2024-06-20 16:41:44 +0200 | enoq | (~enoq@2a05:1141:1e6:3b00:c958:a45e:c4e0:3650) |
| 2024-06-20 16:42:30 +0200 | <enoq> | hi, so I was watching a Kotlin talk recently where they've mentioned that sum types have undecidability problems; is this inherent to sum types or just related to how OO languages design their type hyrarchies? |
| 2024-06-20 16:45:18 +0200 | euleritian | (~euleritia@dynamic-176-007-169-090.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-20 16:45:32 +0200 | mmohammadi9812 | (~mohammad@85.185.34.203) |
| 2024-06-20 16:45:34 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-20 16:47:16 +0200 | soverysour | (~soverysou@188.27.2.34) |
| 2024-06-20 16:47:16 +0200 | soverysour | (~soverysou@188.27.2.34) (Changing host) |
| 2024-06-20 16:47:16 +0200 | soverysour | (~soverysou@user/soverysour) |
| 2024-06-20 16:49:54 +0200 | <danse-nr3> | sounds to me something related more to object-oriented hierarchies, but it's difficult to tell without more detail |
| 2024-06-20 16:51:37 +0200 | <dolio> | Undecidability of what? |
| 2024-06-20 16:51:52 +0200 | <tomsmeding> | haskell has no problems with sum types, but then haskell is not an OO language |
| 2024-06-20 16:56:43 +0200 | <sprout> | most interesting type systems are undecidable |
| 2024-06-20 16:56:50 +0200 | sprout | looks at system f |
| 2024-06-20 16:57:12 +0200 | yin | (~yin@user/zero) |
| 2024-06-20 17:06:35 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-06-20 17:08:49 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-06-20 17:08:54 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 268 seconds) |
| 2024-06-20 17:09:56 +0200 | Pixi__ | (~Pixi@user/pixi) (Quit: Leaving) |
| 2024-06-20 17:13:53 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) (Remote host closed the connection) |
| 2024-06-20 17:14:48 +0200 | chiselfuse | (~chiselfus@user/chiselfuse) |
| 2024-06-20 17:16:26 +0200 | <drdo> | enoq: decidability of what exactly? |
| 2024-06-20 17:17:23 +0200 | <enoq> | I think they've mentioned something about polynomial runtime |
| 2024-06-20 17:19:33 +0200 | <EvanR> | kotlin conf 2024 brochure says this apparently to elaborate on what "kotlin's type system is undecdiable" means: we can reliably cause the type-checker to stack overflow |
| 2024-06-20 17:20:01 +0200 | <EvanR> | and it is unsound because "we can trick it into thinking a String is an Int" |
| 2024-06-20 17:20:15 +0200 | <dolio> | That's a bit non-standard. |
| 2024-06-20 17:21:01 +0200 | EvanR | loads up some isomorphic javascript and escapes through it |
| 2024-06-20 17:22:19 +0200 | Pixi | (~Pixi@user/pixi) |
| 2024-06-20 17:24:28 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-06-20 17:25:10 +0200 | danse-nr3 | (~danse-nr3@151.43.38.52) (Read error: Connection reset by peer) |
| 2024-06-20 17:25:23 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 17:25:24 +0200 | <EvanR> | if something can be decided in polynomial time, that's highly non-undecidable |
| 2024-06-20 17:26:23 +0200 | danse-nr3 | (~danse-nr3@151.43.0.225) |
| 2024-06-20 17:26:37 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-06-20 17:27:51 +0200 | <drdo> | EvanR: did you throw that double negative in to confuse the intuitionists? |
| 2024-06-20 17:29:19 +0200 | <dolio> | Intuitionists are the ones who aren't confused about double negatives. :) |
| 2024-06-20 17:33:29 +0200 | <EvanR> | let the rhetorical purpose there be a free construction of the mind |
| 2024-06-20 17:37:57 +0200 | <dminuoso> | Regarding type safety, if we take the TaPL definition, then "safety = progress + preservation", and confusing a String for an Int probably is a preservation violation |
| 2024-06-20 17:39:11 +0200 | <danse-nr3> | resorting to the definition probably unnecessary in order to consider that unsafe |
| 2024-06-20 17:39:25 +0200 | <danse-nr3> | well to /a/ definition |
| 2024-06-20 17:40:26 +0200 | <dminuoso> | Well, I think to state "x is unsafe" requires some definition of what we mean by "unsafe" really. |
| 2024-06-20 17:40:55 +0200 | <danse-nr3> | then i'll say "x is frown upon". Even works better these days |
| 2024-06-20 17:41:10 +0200 | <danse-nr3> | *frowned |
| 2024-06-20 17:42:47 +0200 | <EvanR> | they say it's unsound, which sounds like a logic thing not a programming thing |
| 2024-06-20 17:43:12 +0200 | <EvanR> | like unsafe |
| 2024-06-20 17:43:58 +0200 | <dminuoso> | EvanR: Again according to TaPL at least, soundness is in some circles a synonym for safety |
| 2024-06-20 17:44:05 +0200 | <EvanR> | but I can imagine using suitable logic you can use the assumption that String = Int to prove 0 = 1 or False |
| 2024-06-20 17:45:38 +0200 | igghibu | (~igghibu@193.19.202.131) |
| 2024-06-20 17:46:23 +0200 | igghibu | (~igghibu@193.19.202.131) (Remote host closed the connection) |
| 2024-06-20 17:46:52 +0200 | <dolio> | Type soundness is a programming thing. |
| 2024-06-20 17:48:51 +0200 | <dolio> | In GHC, getting a String where you're expecting Ints might causes a segfault or something. In Kotlin it probably only causes some kind of runtime exception, but it's probably harder to debug than most errors. |
| 2024-06-20 17:49:24 +0200 | <dolio> | It might not even be obvious where the problem is. |
| 2024-06-20 17:50:09 +0200 | <dolio> | Segfault is if you're lucky in GHC, I guess. It might just do something wrong and leave you wondering why. |
| 2024-06-20 17:55:59 +0200 | <dminuoso> | Bugs like Pentium FDIV make you wonder how many subtle errors are left in silicon, microcode, kernel code, or compilers that have not been detected but keep influencing your programs, perhaps especially in case of FDIV in ways that are hard to even notice. |
| 2024-06-20 17:57:03 +0200 | rosco | (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 2024-06-20 17:57:17 +0200 | soverysour | (~soverysou@user/soverysour) (Ping timeout: 240 seconds) |
| 2024-06-20 18:00:03 +0200 | Buggys | (Buggys@shelltalk.net) |
| 2024-06-20 18:01:12 +0200 | <johnw_> | what if FDIV results in Zombies being harder to kill in Left for Dead, so we simply evolved to become better zombie killers... |
| 2024-06-20 18:08:29 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 240 seconds) |
| 2024-06-20 18:09:17 +0200 | soverysour | (~soverysou@user/soverysour) |
| 2024-06-20 18:10:39 +0200 | lxsameer | (lxsameer@Serene/lxsameer) |
| 2024-06-20 18:15:57 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-06-20 18:16:40 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) |
| 2024-06-20 18:17:51 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Ping timeout: 255 seconds) |
| 2024-06-20 18:18:48 +0200 | Buggys | (Buggys@shelltalk.net) (Quit: IRCNow and Forever!) |
| 2024-06-20 18:19:15 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-06-20 18:20:08 +0200 | kyborg2011 | (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 2024-06-20 18:21:00 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-06-20 18:24:07 +0200 | lxsameer | (lxsameer@Serene/lxsameer) (Ping timeout: 246 seconds) |
| 2024-06-20 18:24:41 +0200 | igghibu | (~igghibu@193.19.202.131) |
| 2024-06-20 18:25:48 +0200 | danse-nr3 | (~danse-nr3@151.43.0.225) (Ping timeout: 256 seconds) |
| 2024-06-20 18:25:57 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 18:26:08 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-06-20 18:26:09 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-06-20 18:26:11 +0200 | CiaoSen | (~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03) |
| 2024-06-20 18:29:03 +0200 | igghibu | (~igghibu@193.19.202.131) (Remote host closed the connection) |
| 2024-06-20 18:30:02 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-06-20 18:30:22 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-06-20 18:30:51 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 18:30:54 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-06-20 18:35:22 +0200 | danse-nr3 | (~danse-nr3@151.43.0.225) |
| 2024-06-20 18:39:31 +0200 | dcoutts__ | (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 246 seconds) |
| 2024-06-20 18:40:51 +0200 | CiaoSen | (~Jura@2a05:5800:2a6:de00:e6b9:7aff:fe80:3d03) (Ping timeout: 260 seconds) |
| 2024-06-20 18:41:17 +0200 | madhavanmiui | (~madhavanm@2409:40f4:28:9c68:8000::) |
| 2024-06-20 18:41:24 +0200 | igghibu | (~igghibu@146.70.225.113) |
| 2024-06-20 18:42:15 +0200 | mmohammadi9812 | (~mohammad@85.185.34.203) (Ping timeout: 260 seconds) |
| 2024-06-20 18:43:15 +0200 | yin | (~yin@user/zero) (Ping timeout: 268 seconds) |
| 2024-06-20 18:43:23 +0200 | igghibu | (~igghibu@146.70.225.113) (Remote host closed the connection) |
| 2024-06-20 18:43:40 +0200 | igghibu | (~igghibu@146.70.225.113) |
| 2024-06-20 18:43:44 +0200 | madhavanmiui | (~madhavanm@2409:40f4:28:9c68:8000::) (Client Quit) |
| 2024-06-20 18:47:30 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:b0fb:c3f5:4666:ad2f) (Remote host closed the connection) |
| 2024-06-20 18:47:40 +0200 | bontaq | (~user@ool-45779c03.dyn.optonline.net) |
| 2024-06-20 18:55:51 +0200 | yin | (~yin@user/zero) |
| 2024-06-20 19:02:56 +0200 | ft | (~ft@p3e9bcb39.dip0.t-ipconnect.de) |
| 2024-06-20 19:03:52 +0200 | igghibu | (~igghibu@146.70.225.113) (Remote host closed the connection) |
| 2024-06-20 19:08:50 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-06-20 19:10:19 +0200 | soverysour | (~soverysou@user/soverysour) (Ping timeout: 246 seconds) |
| 2024-06-20 19:13:24 +0200 | Square | (~Square@user/square) |
| 2024-06-20 19:14:05 +0200 | yin | (~yin@user/zero) (Remote host closed the connection) |
| 2024-06-20 19:15:29 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 19:15:44 +0200 | enoq | (~enoq@2a05:1141:1e6:3b00:c958:a45e:c4e0:3650) (Quit: Leaving) |
| 2024-06-20 19:29:30 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-06-20 19:31:57 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-20 19:32:37 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 19:43:36 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 19:46:12 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-06-20 19:47:27 +0200 | simendsjo | (~user@84.209.170.3) |
| 2024-06-20 19:49:37 +0200 | philopsos1 | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) |
| 2024-06-20 19:52:32 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 19:52:33 +0200 | danse-nr3 | (~danse-nr3@151.43.0.225) (Quit: Leaving) |
| 2024-06-20 19:53:14 +0200 | philopsos1 | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) (Client Quit) |
| 2024-06-20 19:58:09 +0200 | philopsos1 | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) |
| 2024-06-20 20:01:02 +0200 | philopsos1 | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) (Client Quit) |
| 2024-06-20 20:01:29 +0200 | philopsos1 | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) |
| 2024-06-20 20:02:10 +0200 | philopsos1 | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) (Changing host) |
| 2024-06-20 20:02:10 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-20 20:02:49 +0200 | philopsos1 | (~caecilius@user/philopsos) (Client Quit) |
| 2024-06-20 20:03:25 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-20 20:08:29 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2024-06-20 20:10:09 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 272 seconds) |
| 2024-06-20 20:11:26 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2024-06-20 20:13:57 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Quit: Lost terminal) |
| 2024-06-20 20:14:32 +0200 | philopsos | (~caecilius@user/philopsos) (Quit: Lost terminal) |
| 2024-06-20 20:15:10 +0200 | soverysour | (~soverysou@188.27.2.34) |
| 2024-06-20 20:15:10 +0200 | soverysour | (~soverysou@188.27.2.34) (Changing host) |
| 2024-06-20 20:15:10 +0200 | soverysour | (~soverysou@user/soverysour) |
| 2024-06-20 20:17:40 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-06-20 20:19:00 +0200 | mmohammadi9812 | (~mohammad@85.185.34.203) |
| 2024-06-20 20:19:48 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 20:21:23 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |
| 2024-06-20 20:23:46 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 20:31:19 +0200 | ocra8 | (~ocra8@user/ocra8) (Quit: WeeChat 4.3.2) |
| 2024-06-20 20:40:25 +0200 | jrm | (~jrm@user/jrm) (Ping timeout: 268 seconds) |
| 2024-06-20 20:42:12 +0200 | target_i | (~target_i@user/target-i/x-6023099) |
| 2024-06-20 20:42:29 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-06-20 20:43:30 +0200 | jrm | (~jrm@user/jrm) |
| 2024-06-20 20:44:27 +0200 | wlhn | (~wenzel@dl46fx8hbfttwvhb-h1ly-3.rev.dnainternet.fi) (Quit: Leaving) |
| 2024-06-20 20:48:36 +0200 | soverysour | (~soverysou@user/soverysour) (Ping timeout: 255 seconds) |
| 2024-06-20 21:06:35 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds) |
| 2024-06-20 21:08:34 +0200 | lxsameer | (lxsameer@Serene/lxsameer) |
| 2024-06-20 21:17:01 +0200 | lxsameer | (lxsameer@Serene/lxsameer) (Ping timeout: 256 seconds) |
| 2024-06-20 21:18:59 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-06-20 21:19:16 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 2024-06-20 21:20:24 +0200 | <hadronized> | I have a silly question; is there a range (expected range?) of the time a typicall GC collection can take? |
| 2024-06-20 21:20:30 +0200 | <hadronized> | is there a upper boundary? |
| 2024-06-20 21:21:00 +0200 | <hadronized> | like, if there are tons of free objects, is the GC interruptable to prevent having stopping the world for too long? and if not, is there a way to know the average-worst performance? |
| 2024-06-20 21:21:08 +0200 | <hadronized> | is it within 1ms? 10ms? 100ms? |
| 2024-06-20 21:22:53 +0200 | <EvanR> | there is --copying-gc and --nonmoving-gc which will get different latency characteristics |
| 2024-06-20 21:23:31 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-20 21:23:41 +0200 | <EvanR> | the default copying gc will worst case take time proportional to how many live objects there are |
| 2024-06-20 21:24:20 +0200 | <EvanR> | use profiling to see how much the time actually is |
| 2024-06-20 21:27:42 +0200 | <tomsmeding> | also consider using the `+RTS -S` rts flag; it prints statistics about GC runtime when the process exits |
| 2024-06-20 21:27:47 +0200 | <hadronized> | I just wanted to have a rough idea of what to expect |
| 2024-06-20 21:28:14 +0200 | <EvanR> | write a program and tell us how it goes xD |
| 2024-06-20 21:28:15 +0200 | <tomsmeding> | hadronized: it depends completely on the size of your heap |
| 2024-06-20 21:28:30 +0200 | <tomsmeding> | if you never have more than 100 KB of data alive at a time, GC will be trivial |
| 2024-06-20 21:28:51 +0200 | <tomsmeding> | if you have 30 GB of live data, GC will be very expensive, see if you can use compact regions or similar to alleviate trouble |
| 2024-06-20 21:29:12 +0200 | <hadronized> | yeah |
| 2024-06-20 21:29:26 +0200 | <tomsmeding> | (that is, live data that the GC has to traverse; a huge ByteString doesn't count because the GC sees "ok, here's a ByteString" and moves on) |
| 2024-06-20 21:29:27 +0200 | <hadronized> | I’m trying to think whether it would be usable to make some graphics code to make a video game etc. |
| 2024-06-20 21:29:35 +0200 | <hadronized> | since I really want to go back to what I used to do ~years ago (luminance)o |
| 2024-06-20 21:29:36 +0200 | <hadronized> | -o |
| 2024-06-20 21:30:35 +0200 | <tomsmeding> | the nonmoving GC would be better for that because it tries to keep GC latency low, at the expense of throughput (i.e. total amount of time spent in GC is higher, but most of it happens in parallel with your code) |
| 2024-06-20 21:30:48 +0200 | <EvanR> | video games are possible, check out #haskell-game xD |
| 2024-06-20 21:31:00 +0200 | <hadronized> | is lambdacube still a thing? |
| 2024-06-20 21:31:03 +0200 | <EvanR> | intense CPU based graphics code, might be possible for very low rez framebuffer |
| 2024-06-20 21:31:23 +0200 | <tomsmeding> | if you want to make a game with large amounts of data in-memory and a consistent, high frame rate, perhaps haskell is not the optimal language to make that in |
| 2024-06-20 21:32:21 +0200 | <tomsmeding> | GC can easily take 10ms if you have GBs of data |
| 2024-06-20 21:32:34 +0200 | andrewboltachev | (~andrey@178.141.121.180) |
| 2024-06-20 21:32:39 +0200 | <tomsmeding> | probably more |
| 2024-06-20 21:32:41 +0200 | <EvanR> | there are ECS engines... I heard good things about Apecs |
| 2024-06-20 21:32:51 +0200 | <EvanR> | probably overkill for your first attempt at a haskell game |
| 2024-06-20 21:33:25 +0200 | <EvanR> | GB of truly dynamic data seems a bit nuts, usually games have huge amounts of static stuff loaded once |
| 2024-06-20 21:33:34 +0200 | <EvanR> | triple A games |
| 2024-06-20 21:33:43 +0200 | <hadronized> | yeah that sounds like a lot of data |
| 2024-06-20 21:34:15 +0200 | <hadronized> | but if you have memory that sticks around (not garbage), even with tons of it, the GC shouldn’t have too much problem with that, right? |
| 2024-06-20 21:34:17 +0200 | <EvanR> | I think performance isn't going to be first hurdle to writing games |
| 2024-06-20 21:34:20 +0200 | <EvanR> | in haskell |
| 2024-06-20 21:36:33 +0200 | <tomsmeding> | hadronized: the GC is going to traverse all that data every time, except if 1. it's memory of which the GC knows that it doesn't contain pointers, such as a ByteString, or 2. it's in a compact region (https://hackage.haskell.org/package/compact) |
| 2024-06-20 21:37:04 +0200 | <tomsmeding> | if you use the (default) copying GC, (1.) has the further side condition that that memory must be pinned, otherwise it'll be copied anyway; a ByteString is pinned, but a Vector is not, for example |
| 2024-06-20 21:37:46 +0200 | <talismanick> | Can `data Tree a = Tip a | Bin (Tree a) (Tree a)` be reformulated to avoid proving typeclass laws by cases + induction? Something to do with recursion schemes? |
| 2024-06-20 21:38:38 +0200 | <tomsmeding> | which type classes? |
| 2024-06-20 21:38:58 +0200 | <EvanR> | hadronized, for each ton of non garbage, the major collection cycle requires 1 millisecond per ton of time xD |
| 2024-06-20 21:38:59 +0200 | <talismanick> | tomsmeding: Applicative thus far, but also Monad |
| 2024-06-20 21:39:29 +0200 | <talismanick> | I wrote `(Tip f) <*> t = f <$> t` and `(Bin l r) <*> t = Bin (l <*> t) (r <*> t)` |
| 2024-06-20 21:39:52 +0200 | <tomsmeding> | that's correct, I think |
| 2024-06-20 21:40:11 +0200 | <talismanick> | proving interchange was easy enough with induction, but composition is a doozy |
| 2024-06-20 21:40:12 +0200 | <tomsmeding> | general advice with this is: write pure (easy) and (>>=) (harder, but less chance of making mistakes), then define (<*>) = ap |
| 2024-06-20 21:40:47 +0200 | <talismanick> | bind was `Tip x >>= f = f x` and `Bin l r >>= f = Bin (l >>= f) (r >>= f)` |
| 2024-06-20 21:40:47 +0200 | <tomsmeding> | you'll find that there's really only one way to write (>>=) for your Tree |
| 2024-06-20 21:40:54 +0200 | <tomsmeding> | indeed |
| 2024-06-20 21:41:38 +0200 | <tomsmeding> | if you expand the definition of 'ap' and the calls to your (>>=) that it contains, you'll find out that it's equivalent to the (<*>) that you wrote |
| 2024-06-20 21:42:00 +0200 | <talismanick> | so just prove the monad laws and leave it at that? |
| 2024-06-20 21:42:27 +0200 | <tomsmeding> | there's no "standard" way to generate Monad instances for general tree-like data types (this is why there is no -XDeriveMonad), so it'll be hard to find some general construction that makes it come "for free" |
| 2024-06-20 21:42:39 +0200 | <tomsmeding> | but this particular data type is very standard; you might be able to find it in a library |
| 2024-06-20 21:42:41 +0200 | <hadronized> | it’s a bit discouraging :( |
| 2024-06-20 21:42:59 +0200 | <EvanR> | hadronized, are you imagining bad gc performance for some reason? |
| 2024-06-20 21:43:01 +0200 | <EvanR> | that's not healthy |
| 2024-06-20 21:43:03 +0200 | <tomsmeding> | talismanick: yes, I'd just prove the monad laws for your (>>=); they imply the applicative laws |
| 2024-06-20 21:43:07 +0200 | <hadronized> | EvanR: yeah |
| 2024-06-20 21:43:11 +0200 | <EvanR> | lol |
| 2024-06-20 21:43:16 +0200 | <talismanick> | tomsmeding: I don't mean a way to derive Monad (because that depends on Applicative, which depends on a choice of monoid) |
| 2024-06-20 21:43:23 +0200 | <hadronized> | I mean, a decent video game today has to run at the v-sync of your screen |
| 2024-06-20 21:43:25 +0200 | <EvanR> | that's like people can't write any C code because they thing malloc will be too slow |
| 2024-06-20 21:43:26 +0200 | <talismanick> | I mean a way to factor out recursion/induction when proving laws |
| 2024-06-20 21:43:29 +0200 | <hadronized> | my screen, for instance, runs at 165Hz |
| 2024-06-20 21:43:52 +0200 | <hadronized> | so a whole frame has to be rendered in less than 6ms |
| 2024-06-20 21:44:00 +0200 | <hadronized> | if a GC pause can take 10ms, that’s already done |
| 2024-06-20 21:44:02 +0200 | <EvanR> | I recommend using opengl somehow so you utilize the GPU for graphics |
| 2024-06-20 21:44:24 +0200 | <EvanR> | esp at 165 fps |
| 2024-06-20 21:44:28 +0200 | <hadronized> | EvanR: I wrote luminance in Haskell years ago, and luminance in Rust using OpenGL, WebGL, Vulkan, etc. |
| 2024-06-20 21:44:40 +0200 | <hadronized> | so yeah, I’m not saying the problem will be due to graphics technology |
| 2024-06-20 21:44:41 +0200 | <tomsmeding> | talismanick: I mean, you can factor your data type as `newtype Fix f = In (f (Fix f)); data TreeF a r = TipF a | BinF r r; type Tree a = Fix (TreeF a)` |
| 2024-06-20 21:44:44 +0200 | <hadronized> | but everything that revolve around it |
| 2024-06-20 21:44:52 +0200 | <talismanick> | although it would be nice to be able to write "given this monoid, derive the corresponding Applicative/Monad instances" |
| 2024-06-20 21:45:08 +0200 | <tomsmeding> | talismanick: what monoid do you mean? `join`? |
| 2024-06-20 21:45:27 +0200 | <tomsmeding> | there are sometimes less valid Monad instances than there are valid Applicative instances for a type |
| 2024-06-20 21:45:32 +0200 | m5zs7k | (aquares@web10.mydevil.net) (Ping timeout: 252 seconds) |
| 2024-06-20 21:45:33 +0200 | <tomsmeding> | so bunching them together like that doesn't sound right |
| 2024-06-20 21:45:38 +0200 | <tomsmeding> | (to wit: [a]) |
| 2024-06-20 21:45:57 +0200 | <talismanick> | yeah, zipping is applicative but not monadic |
| 2024-06-20 21:46:22 +0200 | <talismanick> | but I thought every monad instance depends on some underlying applicative, which itself depends on some underlying choice of monoid |
| 2024-06-20 21:46:24 +0200 | <EvanR> | hadronized, yeah a hypothetical unsubstantiated data point was 10ms for a major collection because you have gigabytes of live heap for some reason |
| 2024-06-20 21:46:42 +0200 | <tomsmeding> | talismanick: what monoid are you talking about there? (My category-fu is limited) |
| 2024-06-20 21:46:42 +0200 | <EvanR> | note that most collections aren't major collections |
| 2024-06-20 21:47:02 +0200 | <EvanR> | you can also time major collections yourself if there's a convenient place to do it, e.g. between levels |
| 2024-06-20 21:47:20 +0200 | <tomsmeding> | if that happens often enough |
| 2024-06-20 21:47:29 +0200 | <talismanick> | www.staff.city.ac.uk/~ross/papers/Applicative.pdf |
| 2024-06-20 21:47:46 +0200 | m5zs7k | (aquares@web10.mydevil.net) |
| 2024-06-20 21:47:52 +0200 | <ncf> | starting to understand why Escardó says the Applicative => Monad thing was a pedagogical disaster... |
| 2024-06-20 21:47:54 +0200 | <EvanR> | sure you just wouldn't want to switch levels then wait until sometime into the next level for a major GC "pause" (if there is one) |
| 2024-06-20 21:47:59 +0200 | <talismanick> | see section 4, "Monoids are phantom Applicative functors" |
| 2024-06-20 21:48:56 +0200 | <ncf> | a monad does not "depend" on a choice of underlying applicative; every Monad induces two Applicative structures, and there is a law that says that if a type implements Monad then it also has to implement Applicative with the first of those induced structures |
| 2024-06-20 21:49:06 +0200 | <tomsmeding> | talismanick: doesn't that say that every Monoid induces an Applicative, not that every Applicative is based on a Monoid? |
| 2024-06-20 21:49:28 +0200 | <ncf> | that section is just explaining the Monoid m => Applicative (Const m) instance |
| 2024-06-20 21:49:41 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 2024-06-20 21:49:57 +0200 | <ncf> | every monoid gives rise to an applicative this way (and to a monad via Writer), but that does not mean that every applicative (or monad) has an underlying Monoid |
| 2024-06-20 21:50:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 21:50:10 +0200 | <ncf> | (it does have an underlying monoid object in some monoidal category but that's another story) |
| 2024-06-20 21:50:16 +0200 | <talismanick> | isn't every applicative isomorphic to a monoidal functor? |
| 2024-06-20 21:50:19 +0200 | <ncf> | yes |
| 2024-06-20 21:50:27 +0200 | <tomsmeding> | that's a different monoid, though |
| 2024-06-20 21:50:32 +0200 | <talismanick> | ah, I see |
| 2024-06-20 21:50:33 +0200 | <tomsmeding> | that's `join` |
| 2024-06-20 21:50:38 +0200 | <tomsmeding> | :t join |
| 2024-06-20 21:50:39 +0200 | <lambdabot> | Monad m => m (m a) -> m a |
| 2024-06-20 21:50:48 +0200 | <ncf> | join has little to do with monoidal functors |
| 2024-06-20 21:50:52 +0200 | <tomsmeding> | oh oops |
| 2024-06-20 21:51:22 +0200 | tomsmeding | will refrain from saying further falsehoods about category theory :p |
| 2024-06-20 21:51:50 +0200 | <EvanR> | hadronized, you could also try existing commercial computer games that were written in haskell and see if run at 165 fps, if you're still skeptical |
| 2024-06-20 21:52:10 +0200 | <hadronized> | is there any?! |
| 2024-06-20 21:52:15 +0200 | <EvanR> | lol |
| 2024-06-20 21:53:03 +0200 | <EvanR> | hmm https://magiccookies2.haskell.games/ |
| 2024-06-20 21:53:38 +0200 | <talismanick> | https://keera.co.uk/posts/2014/10/15/from-60-fps-to-500/ |
| 2024-06-20 21:54:38 +0200 | talismanick | sees reference to gamedev in Haskell, greps chat log for references to FRP |
| 2024-06-20 21:56:16 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 22:00:13 +0200 | va10323 | (~v324@2802:8010:a008:4700:4e6a:6189:b174:1928) |
| 2024-06-20 22:00:58 +0200 | _xor | (~xor@ip-208-102-243-175.dynamic.fuse.net) (Quit: Ping timeout (120 seconds)) |
| 2024-06-20 22:01:12 +0200 | _xor | (~xor@ip-208-102-243-175.dynamic.fuse.net) |
| 2024-06-20 22:04:59 +0200 | va10323 | (~v324@2802:8010:a008:4700:4e6a:6189:b174:1928) (Quit: Leaving) |
| 2024-06-20 22:13:49 +0200 | <cheater> | i wish codex was up to date |
| 2024-06-20 22:13:53 +0200 | <cheater> | cuz it's really good actually |
| 2024-06-20 22:21:23 +0200 | rlj | (~rlj@194-218-34-180.customer.telia.com) |
| 2024-06-20 22:22:12 +0200 | rlj | (~rlj@194-218-34-180.customer.telia.com) (Client Quit) |
| 2024-06-20 22:25:39 +0200 | Guest|39 | (~Guest|39@160.178.51.69) |
| 2024-06-20 22:27:10 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-20 22:37:59 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving) |
| 2024-06-20 22:39:24 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-20 22:40:25 +0200 | tcard | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2024-06-20 22:46:38 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-06-20 22:46:57 +0200 | ystael | (~ystael@user/ystael) (Quit: Lost terminal) |
| 2024-06-20 22:50:23 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds) |
| 2024-06-20 22:52:27 +0200 | simendsjo | (~user@84.209.170.3) (Ping timeout: 264 seconds) |
| 2024-06-20 22:53:05 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-20 22:53:47 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-06-20 22:55:29 +0200 | Guest|39 | (~Guest|39@160.178.51.69) (Ping timeout: 256 seconds) |
| 2024-06-20 22:58:33 +0200 | Guest|86 | (~Guest|86@161.230.86.113) |
| 2024-06-20 22:59:36 +0200 | ystael | (~ystael@user/ystael) |
| 2024-06-20 23:01:55 +0200 | Guest|86 | (~Guest|86@161.230.86.113) (Client Quit) |
| 2024-06-20 23:02:33 +0200 | Guest|86 | (~Guest|86@161.230.86.113) |
| 2024-06-20 23:02:39 +0200 | AlexZenon | (~alzenon@178.34.162.224) (Ping timeout: 260 seconds) |
| 2024-06-20 23:03:41 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-06-20 23:05:53 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-06-20 23:07:39 +0200 | mmohammadi9812 | (~mohammad@85.185.34.203) (Ping timeout: 255 seconds) |
| 2024-06-20 23:08:03 +0200 | AlexZenon | (~alzenon@178.34.162.224) |
| 2024-06-20 23:10:54 +0200 | saus | (~saus@pool-98-114-45-229.phlapa.fios.verizon.net) |
| 2024-06-20 23:12:23 +0200 | andrei_n | (~andrei_n@user/andrei-n:62396) (Quit: Leaving) |
| 2024-06-20 23:13:23 +0200 | AlexZenon | (~alzenon@178.34.162.224) (Ping timeout: 260 seconds) |
| 2024-06-20 23:14:04 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 2024-06-20 23:17:48 +0200 | AlexZenon | (~alzenon@178.34.162.224) |
| 2024-06-20 23:23:08 +0200 | philopsos1 | (~caecilius@user/philopsos) (Quit: Lost terminal) |
| 2024-06-20 23:23:27 +0200 | michalz | (~michalz@185.246.207.218) (Quit: ZNC 1.9.0 - https://znc.in) |
| 2024-06-20 23:24:05 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-20 23:24:13 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) |
| 2024-06-20 23:24:27 +0200 | Guest|86 | (~Guest|86@161.230.86.113) (Quit: Connection closed) |
| 2024-06-20 23:24:43 +0200 | philopsos1 | (~caecilius@user/philopsos) (Client Quit) |
| 2024-06-20 23:26:06 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-20 23:28:00 +0200 | EvanR | (~EvanR@user/evanr) (Quit: Leaving) |
| 2024-06-20 23:32:30 +0200 | EvanR | (~EvanR@user/evanr) |
| 2024-06-20 23:34:54 +0200 | saus | (~saus@pool-98-114-45-229.phlapa.fios.verizon.net) (Quit: Client closed) |
| 2024-06-20 23:46:42 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-06-20 23:55:58 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
