| 2024-05-07 00:00:06 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Ping timeout: 256 seconds) |
| 2024-05-07 00:00:50 +0200 | xdminsy | (~xdminsy@117.147.70.233) |
| 2024-05-07 00:00:57 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-05-07 00:12:41 +0200 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2024-05-07 00:15:09 +0200 | pavonia | (~user@user/siracusa) |
| 2024-05-07 00:24:31 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-05-07 00:30:48 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
| 2024-05-07 00:32:23 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2024-05-07 00:33:19 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-05-07 01:04:06 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc4498a318f2cc30029a.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2024-05-07 01:04:13 +0200 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
| 2024-05-07 01:06:54 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 255 seconds) |
| 2024-05-07 01:07:21 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 255 seconds) |
| 2024-05-07 01:07:21 +0200 | dontdieych_ | (~alarm@132.226.169.184) (Ping timeout: 255 seconds) |
| 2024-05-07 01:09:27 +0200 | dontdieych_ | (~alarm@132.226.169.184) |
| 2024-05-07 01:11:49 +0200 | xff0x | (~xff0x@2405:6580:b080:900:e758:caa1:b0a5:cc6f) (Ping timeout: 246 seconds) |
| 2024-05-07 01:13:39 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 268 seconds) |
| 2024-05-07 01:13:58 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a053:399f:88bd:931d) |
| 2024-05-07 01:14:14 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-05-07 01:15:48 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-05-07 01:25:25 +0200 | cheater | (~Username@user/cheater) (Read error: Connection reset by peer) |
| 2024-05-07 01:26:59 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 264 seconds) |
| 2024-05-07 01:27:02 +0200 | cheater | (~Username@user/cheater) |
| 2024-05-07 01:28:19 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-05-07 01:32:03 +0200 | mud | (~mud@user/kadoban) |
| 2024-05-07 01:34:08 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a053:399f:88bd:931d) (Remote host closed the connection) |
| 2024-05-07 01:34:27 +0200 | xff0x | (~xff0x@2405:6580:b080:900:35ed:753d:5333:e2a3) |
| 2024-05-07 01:52:30 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 2024-05-07 01:59:42 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Remote host closed the connection) |
| 2024-05-07 02:04:13 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-05-07 02:24:48 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 02:24:54 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Remote host closed the connection) |
| 2024-05-07 02:25:14 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
| 2024-05-07 02:35:23 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-05-07 02:39:32 +0200 | mud | (~mud@user/kadoban) (Quit: quit) |
| 2024-05-07 02:46:42 +0200 | califax | (~califax@user/califx) |
| 2024-05-07 02:48:17 +0200 | sgarcia | (sgarcia@swarm.znchost.com) (Quit: Hosted by www.ZNCHost.com) |
| 2024-05-07 02:51:11 +0200 | sgarcia | (sgarcia@swarm.znchost.com) |
| 2024-05-07 02:51:41 +0200 | onion | (~yin@user/zero) (Ping timeout: 240 seconds) |
| 2024-05-07 03:00:46 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 255 seconds) |
| 2024-05-07 03:08:36 +0200 | thales | (~thales@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) |
| 2024-05-07 03:08:57 +0200 | thales | (~thales@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) (Client Quit) |
| 2024-05-07 03:20:47 +0200 | otto_s | (~user@p4ff27405.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2024-05-07 03:22:31 +0200 | otto_s | (~user@p5de2f3d2.dip0.t-ipconnect.de) |
| 2024-05-07 03:22:39 +0200 | xff0x | (~xff0x@2405:6580:b080:900:35ed:753d:5333:e2a3) (Ping timeout: 260 seconds) |
| 2024-05-07 03:23:30 +0200 | dispater | (~dispater@mail.brprice.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 03:23:30 +0200 | orcus | (~orcus@mail.brprice.uk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 03:25:19 +0200 | dispater | (~dispater@mail.brprice.uk) |
| 2024-05-07 03:25:21 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-07 03:25:49 +0200 | orcus | (~orcus@mail.brprice.uk) |
| 2024-05-07 03:30:44 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-07 03:34:55 +0200 | thales | (~tram@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) |
| 2024-05-07 03:35:16 +0200 | thales | (~tram@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) (Client Quit) |
| 2024-05-07 03:35:28 +0200 | thales | (~tram@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) |
| 2024-05-07 03:36:06 +0200 | thales | (~tram@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) (Client Quit) |
| 2024-05-07 03:39:14 +0200 | tram | (~tram@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) |
| 2024-05-07 03:39:47 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:2ec9:5672:626b:934d) (Quit: WeeChat 4.2.1) |
| 2024-05-07 03:42:14 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:55f8:739e:3296:6d3) |
| 2024-05-07 03:43:56 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 256 seconds) |
| 2024-05-07 03:46:00 +0200 | tram | (~tram@2a02:586:7e3a:cbe3:5221:8c84:e9f6:b7e4) (Quit: Leaving.) |
| 2024-05-07 04:01:49 +0200 | petrichor | (~znc-user@user/petrichor) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 04:02:30 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Remote host closed the connection) |
| 2024-05-07 04:02:43 +0200 | petrichor | (~znc-user@user/petrichor) |
| 2024-05-07 04:07:46 +0200 | gastus_ | (~gastus@185.6.123.231) |
| 2024-05-07 04:11:23 +0200 | gastus | (~gastus@185.6.123.230) (Ping timeout: 264 seconds) |
| 2024-05-07 04:12:26 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-05-07 04:19:55 +0200 | YuutaW | (~YuutaW@2404:f4c0:f9c3:502::100:17b7) |
| 2024-05-07 04:21:05 +0200 | yuuta | (~YuutaW@mail.yuuta.moe) (Read error: Connection reset by peer) |
| 2024-05-07 04:22:07 +0200 | td_ | (~td@i53870908.versanet.de) (Ping timeout: 272 seconds) |
| 2024-05-07 04:23:25 +0200 | td_ | (~td@i53870936.versanet.de) |
| 2024-05-07 04:30:35 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-07 04:44:05 +0200 | terrorjack | (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 2024-05-07 04:45:58 +0200 | terrorjack | (~terrorjac@2a01:4f8:c17:87f8::) |
| 2024-05-07 04:50:11 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Quit: Lost terminal) |
| 2024-05-07 04:53:09 +0200 | amjoseph | (~amjoseph@static-198-44-128-146.cust.tzulo.com) (Ping timeout: 272 seconds) |
| 2024-05-07 04:56:17 +0200 | mahid | (~mahid@user/standingpad) |
| 2024-05-07 04:56:27 +0200 | mahid | (~mahid@user/standingpad) (WeeChat 4.2.2) |
| 2024-05-07 05:00:53 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-07 05:02:44 +0200 | amjoseph | (~amjoseph@static-198-44-128-146.cust.tzulo.com) |
| 2024-05-07 05:06:21 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
| 2024-05-07 05:10:14 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Quit: Lost terminal) |
| 2024-05-07 05:14:24 +0200 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) |
| 2024-05-07 05:19:53 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-07 05:21:35 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 264 seconds) |
| 2024-05-07 05:23:16 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-05-07 05:25:45 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-05-07 05:30:33 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21) (Ping timeout: 256 seconds) |
| 2024-05-07 05:34:09 +0200 | sgarcia_ | (sgarcia@swarm.znchost.com) |
| 2024-05-07 05:36:26 +0200 | sgarcia | (sgarcia@swarm.znchost.com) (Ping timeout: 252 seconds) |
| 2024-05-07 05:41:10 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Quit: Lost terminal) |
| 2024-05-07 05:44:23 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-07 05:48:28 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-05-07 05:48:59 +0200 | madariaga | (~madariaga@user/madariaga) (Quit: madariaga) |
| 2024-05-07 05:49:23 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 05:49:26 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 05:53:48 +0200 | aforemny | (~aforemny@2001:9e8:6cc5:8500:df7:1fe7:b16:9d8d) |
| 2024-05-07 05:55:28 +0200 | aforemny_ | (~aforemny@i59F516FD.versanet.de) (Ping timeout: 268 seconds) |
| 2024-05-07 05:58:18 +0200 | causal | (~eric@50.35.88.207) (Quit: WeeChat 4.1.1) |
| 2024-05-07 06:00:37 +0200 | phma | (phma@2001:5b0:211f:8958:6fb4:94a7:6ad6:39b3) (Read error: Connection reset by peer) |
| 2024-05-07 06:07:19 +0200 | phma | (phma@2001:5b0:211b:8518:5596:60a:4e27:e0fb) |
| 2024-05-07 06:13:33 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-07 06:14:28 +0200 | bgamari | (~bgamari@64.223.226.84) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 06:15:31 +0200 | mei | (~mei@user/mei) (Ping timeout: 268 seconds) |
| 2024-05-07 06:22:56 +0200 | bgamari | (~bgamari@64.223.226.84) |
| 2024-05-07 06:32:53 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 240 seconds) |
| 2024-05-07 06:41:25 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 268 seconds) |
| 2024-05-07 06:42:23 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-05-07 06:44:42 +0200 | euleritian | (~euleritia@dynamic-176-005-142-147.176.5.pool.telefonica.de) |
| 2024-05-07 06:51:27 +0200 | xal | (~xal@mx1.xal.systems) () |
| 2024-05-07 06:51:37 +0200 | Square3 | (~Square4@user/square) (Ping timeout: 255 seconds) |
| 2024-05-07 06:52:25 +0200 | xal | (~xal@mx1.xal.systems) |
| 2024-05-07 06:53:59 +0200 | Square3 | (~Square4@user/square) |
| 2024-05-07 06:59:27 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-05-07 07:01:46 +0200 | mei | (~mei@user/mei) |
| 2024-05-07 07:09:09 +0200 | Square3 | (~Square4@user/square) (Ping timeout: 255 seconds) |
| 2024-05-07 07:09:27 +0200 | philopsos | (~caecilius@user/philopsos) |
| 2024-05-07 07:17:15 +0200 | euleritian | (~euleritia@dynamic-176-005-142-147.176.5.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 07:17:21 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-05-07 07:17:33 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-05-07 07:17:51 +0200 | mokee | (~mokee@37.228.213.214) |
| 2024-05-07 07:19:00 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) |
| 2024-05-07 07:23:50 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-07 07:24:35 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Client Quit) |
| 2024-05-07 07:25:11 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-07 07:27:21 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 268 seconds) |
| 2024-05-07 07:27:35 +0200 | todi1 | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-07 07:29:32 +0200 | euleritian | (~euleritia@dynamic-176-005-142-147.176.5.pool.telefonica.de) |
| 2024-05-07 07:30:03 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-05-07 07:33:31 +0200 | todi1 | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2024-05-07 07:38:47 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc75c420c579c8a75166.dip0.t-ipconnect.de) |
| 2024-05-07 07:44:30 +0200 | michalz | (~michalz@185.246.207.200) |
| 2024-05-07 08:00:13 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) |
| 2024-05-07 08:06:10 +0200 | michalz | (~michalz@185.246.207.200) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 08:06:49 +0200 | Guest|8 | (~Guest|8@96-126-101-153.ip.linodeusercontent.com) |
| 2024-05-07 08:09:07 +0200 | michalz | (~michalz@185.246.207.222) |
| 2024-05-07 08:09:30 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:10:32 +0200 | Guest|8 | (~Guest|8@96-126-101-153.ip.linodeusercontent.com) (Client Quit) |
| 2024-05-07 08:11:16 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:12:25 +0200 | aforemny_ | (~aforemny@2001:9e8:6cc7:5500:cf46:1b2c:d3fc:27bb) |
| 2024-05-07 08:12:59 +0200 | aforemny | (~aforemny@2001:9e8:6cc5:8500:df7:1fe7:b16:9d8d) (Ping timeout: 268 seconds) |
| 2024-05-07 08:14:54 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:16:13 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:17:07 +0200 | aforemny_ | (~aforemny@2001:9e8:6cc7:5500:cf46:1b2c:d3fc:27bb) (Ping timeout: 255 seconds) |
| 2024-05-07 08:17:24 +0200 | aforemny | (~aforemny@i59F516DB.versanet.de) |
| 2024-05-07 08:20:02 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:21:36 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:21:59 +0200 | aforemny | (~aforemny@i59F516DB.versanet.de) (Ping timeout: 252 seconds) |
| 2024-05-07 08:23:10 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Remote host closed the connection) |
| 2024-05-07 08:23:49 +0200 | aforemny | (~aforemny@i59F516E3.versanet.de) |
| 2024-05-07 08:24:42 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:24:42 +0200 | son0p | (~ff@186.121.6.44) (Ping timeout: 268 seconds) |
| 2024-05-07 08:25:42 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) (Remote host closed the connection) |
| 2024-05-07 08:26:28 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:30:18 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:31:36 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:33:01 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 08:34:34 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 2024-05-07 08:34:58 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:36:24 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:40:06 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:41:31 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:45:14 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:46:05 +0200 | phma | (phma@2001:5b0:211b:8518:5596:60a:4e27:e0fb) (Read error: Connection reset by peer) |
| 2024-05-07 08:46:37 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:49:04 +0200 | phma | (phma@2001:5b0:211f:8748:d5d8:f6f:3f3d:8bcc) |
| 2024-05-07 08:50:22 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:51:34 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:52:36 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-05-07 08:55:02 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 08:56:34 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 08:57:50 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) |
| 2024-05-07 08:58:57 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 256 seconds) |
| 2024-05-07 09:00:10 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:01:26 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:03:19 +0200 | euleritian | (~euleritia@dynamic-176-005-142-147.176.5.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 09:03:37 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 09:05:04 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-05-07 09:05:18 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:06:22 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:07:04 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) (Remote host closed the connection) |
| 2024-05-07 09:07:26 +0200 | mokee | (~mokee@37.228.213.214) (Quit: off) |
| 2024-05-07 09:07:28 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) |
| 2024-05-07 09:08:11 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Quit: ZNC - https://znc.in) |
| 2024-05-07 09:09:32 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection) |
| 2024-05-07 09:10:23 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-05-07 09:11:30 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:15:06 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:16:30 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:17:07 +0200 | troydm | (~troydm@user/troydm) (Ping timeout: 268 seconds) |
| 2024-05-07 09:20:14 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:21:36 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:21:41 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 240 seconds) |
| 2024-05-07 09:25:22 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:25:35 +0200 | emmanuelux_ | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-05-07 09:25:46 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) |
| 2024-05-07 09:26:45 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:30:02 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:30:55 +0200 | troydm | (~troydm@user/troydm) |
| 2024-05-07 09:31:34 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:34:01 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-05-07 09:34:42 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:36:22 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:40:18 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:41:39 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:44:23 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) (Ping timeout: 264 seconds) |
| 2024-05-07 09:44:58 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:46:35 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:47:26 +0200 | danza | (~francesco@151.47.240.53) |
| 2024-05-07 09:50:06 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:52:41 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:52:58 +0200 | danza | (~francesco@151.47.240.53) (Ping timeout: 246 seconds) |
| 2024-05-07 09:54:31 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) |
| 2024-05-07 09:54:52 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) (Remote host closed the connection) |
| 2024-05-07 09:55:14 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 09:55:16 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) |
| 2024-05-07 09:56:37 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 09:58:26 +0200 | chele | (~chele@user/chele) |
| 2024-05-07 10:00:22 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:01:15 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) (Remote host closed the connection) |
| 2024-05-07 10:01:35 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) |
| 2024-05-07 10:01:51 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:02:50 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-05-07 10:05:02 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:06:57 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:09:04 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) (Remote host closed the connection) |
| 2024-05-07 10:09:32 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 10:09:42 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:11:26 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:12:55 +0200 | philopsos1 | (~caecilius@user/philopsos) (Quit: Lost terminal) |
| 2024-05-07 10:12:56 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) |
| 2024-05-07 10:13:53 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) (Read error: Connection reset by peer) |
| 2024-05-07 10:14:58 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) |
| 2024-05-07 10:15:18 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:16:36 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:19:58 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:21:35 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-05-07 10:21:38 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:25:06 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:26:40 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:26:53 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) (Remote host closed the connection) |
| 2024-05-07 10:27:31 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) |
| 2024-05-07 10:28:29 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-05-07 10:30:14 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:31:37 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:33:44 +0200 | son0p | (~ff@152.203.77.121) |
| 2024-05-07 10:34:27 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) (Read error: Connection reset by peer) |
| 2024-05-07 10:35:22 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:35:31 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) |
| 2024-05-07 10:36:29 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:40:30 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:41:31 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:42:47 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-05-07 10:44:01 +0200 | remedan | (~remedan@ip-78-102-118-253.bb.vodafone.cz) (Quit: Bye!) |
| 2024-05-07 10:45:10 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:46:22 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:49:00 +0200 | danse-nr3 | (~danse-nr3@151.47.240.53) (Ping timeout: 268 seconds) |
| 2024-05-07 10:49:25 +0200 | danse-nr3 | (~danse-nr3@151.57.103.37) |
| 2024-05-07 10:50:18 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:51:35 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 10:54:58 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 10:56:34 +0200 | stiell_ | (~stiell@gateway/tor-sasl/stiell) |
| 2024-05-07 11:00:06 +0200 | stiell | (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 2024-05-07 11:00:24 +0200 | ChanServ | +o litharge |
| 2024-05-07 11:00:26 +0200 | litharge | +b stiell*!~stiell@gateway/tor-sasl/stiell$##fix_your_connection |
| 2024-05-07 11:00:27 +0200 | stiell_ | litharge (You are banned from this channel (by ski)) |
| 2024-05-07 11:00:37 +0200 | litharge | -o litharge |
| 2024-05-07 11:13:30 +0200 | ft | (~ft@p3e9bc1bf.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-05-07 11:18:50 +0200 | remedan | (~remedan@ip-78-102-118-253.bb.vodafone.cz) |
| 2024-05-07 11:19:44 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 11:20:29 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 240 seconds) |
| 2024-05-07 11:32:14 +0200 | julie_pilgrim | (~julie_pil@user/julie-pilgrim/x-1240752) (Ping timeout: 250 seconds) |
| 2024-05-07 11:33:57 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-05-07 11:38:16 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-05-07 11:54:52 +0200 | JamesMowery3 | (~JamesMowe@ip98-171-80-211.ph.ph.cox.net) |
| 2024-05-07 11:56:51 +0200 | JamesMowery | (~JamesMowe@ip98-171-80-211.ph.ph.cox.net) (Ping timeout: 272 seconds) |
| 2024-05-07 11:56:51 +0200 | JamesMowery3 | JamesMowery |
| 2024-05-07 12:00:25 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:c45d:8c8a:5c4d:ef6b) |
| 2024-05-07 12:08:25 +0200 | noumenon | (~noumenon@113.51-175-156.customer.lyse.net) (Read error: Connection reset by peer) |
| 2024-05-07 12:13:56 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 256 seconds) |
| 2024-05-07 12:15:04 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc75c420c579c8a75166.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-05-07 12:15:37 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 12:18:29 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 12:19:39 +0200 | dos__^^ | (~user@user/dos/x-1723657) (Ping timeout: 268 seconds) |
| 2024-05-07 12:24:21 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21) |
| 2024-05-07 12:28:53 +0200 | gooba | (~gooba@90-231-13-185-no3430.tbcn.telia.com) (Ping timeout: 240 seconds) |
| 2024-05-07 12:35:04 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc75fd23906330cdb73e.dip0.t-ipconnect.de) |
| 2024-05-07 12:36:04 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 12:41:11 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 272 seconds) |
| 2024-05-07 12:48:20 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-05-07 12:52:37 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 12:53:31 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 2024-05-07 12:55:08 +0200 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) |
| 2024-05-07 12:56:21 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 2024-05-07 12:58:06 +0200 | Lord_of_Life_ | Lord_of_Life |
| 2024-05-07 13:12:58 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21) (Quit: WeeChat 4.2.2) |
| 2024-05-07 13:15:13 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a5ad:4ce6:a16c:2efd) |
| 2024-05-07 13:18:37 +0200 | agent314 | (~quassel@static-198-54-134-186.cust.tzulo.com) |
| 2024-05-07 13:30:00 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Read error: Connection reset by peer) |
| 2024-05-07 13:31:14 +0200 | tinjamin | (~tinjamin@banshee.h4x0r.space) (Quit: The Lounge - https://thelounge.chat) |
| 2024-05-07 13:32:19 +0200 | tinjamin | (~tinjamin@banshee.h4x0r.space) |
| 2024-05-07 13:34:16 +0200 | danse-nr3 | (~danse-nr3@151.57.103.37) (Ping timeout: 268 seconds) |
| 2024-05-07 13:38:43 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 13:43:38 +0200 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) |
| 2024-05-07 13:46:12 +0200 | dontdieych_ | (~alarm@132.226.169.184) (Quit: WeeChat 3.8) |
| 2024-05-07 13:50:16 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 13:58:55 +0200 | danse-nr3 | (~danse-nr3@151.57.103.37) |
| 2024-05-07 14:01:02 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 14:07:12 +0200 | nitrix | (~nitrix@user/meow/nitrix) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 14:08:47 +0200 | nitrix | (~nitrix@user/meow/nitrix) |
| 2024-05-07 14:10:45 +0200 | dtman34 | (~dtman34@c-75-72-163-222.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 2024-05-07 14:11:53 +0200 | ddellacosta | (~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 268 seconds) |
| 2024-05-07 14:20:21 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-07 14:28:22 +0200 | mechap | (~mechap@user/mechap) |
| 2024-05-07 14:29:50 +0200 | sp1ff | (~user@c-24-21-45-157.hsd1.wa.comcast.net) (Read error: Connection reset by peer) |
| 2024-05-07 14:32:31 +0200 | mechap | (~mechap@user/mechap) (Client Quit) |
| 2024-05-07 14:40:51 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2024-05-07 14:48:21 +0200 | amjoseph | (~amjoseph@static-198-44-128-146.cust.tzulo.com) (Read error: Connection reset by peer) |
| 2024-05-07 14:48:36 +0200 | amjoseph | (~amjoseph@static-198-44-128-146.cust.tzulo.com) |
| 2024-05-07 14:49:49 +0200 | danse-nr3 | (~danse-nr3@151.57.103.37) (Ping timeout: 268 seconds) |
| 2024-05-07 14:50:27 +0200 | falafel | (~falafel@211.184.50.36) |
| 2024-05-07 14:51:05 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) |
| 2024-05-07 14:52:29 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 240 seconds) |
| 2024-05-07 14:56:09 +0200 | <dminuoso> | litharge: Curious, what happened there? |
| 2024-05-07 14:57:58 +0200 | ocra8 | (ocra8@user/ocra8) |
| 2024-05-07 14:58:23 +0200 | <yushyin> | litharge is a bot, ask ski |
| 2024-05-07 14:58:44 +0200 | <dminuoso> | Yeah that ski mention in the reason confused me further. |
| 2024-05-07 14:58:52 +0200 | <yushyin> | ( https://libera.chat/guides/bots#litharge ) |
| 2024-05-07 14:59:06 +0200 | <tomsmeding> | dminuoso: https://ircbrowse.tomsmeding.com/browse/lchaskell?id=1271966#trid1271966 (scroll up from there) |
| 2024-05-07 14:59:33 +0200 | <tomsmeding> | looks like ski doesn't have their client hide joins/leaves of quiet people :) |
| 2024-05-07 14:59:35 +0200 | <dminuoso> | Oh. I must be spoiled with irc.look.smart_filter :-) |
| 2024-05-07 14:59:44 +0200 | <dminuoso> | To me this channel was dead quiet. |
| 2024-05-07 14:59:51 +0200 | <yushyin> | :D smart filter <3 |
| 2024-05-07 14:59:51 +0200 | <tomsmeding> | same |
| 2024-05-07 15:01:13 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 2024-05-07 15:03:36 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) |
| 2024-05-07 15:08:47 +0200 | tomsmeding | (~tomsmedin@static.21.109.88.23.clients.your-server.de) (Quit: ZNC 1.9.0 - https://znc.in) |
| 2024-05-07 15:10:04 +0200 | tomsmeding | (~tomsmedin@2a01:4f8:c0c:5e5e::2) |
| 2024-05-07 15:10:28 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2024-05-07 15:18:54 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-05-07 15:19:37 +0200 | <kuribas> | opqdonut: I see you are working on clojure reitit! |
| 2024-05-07 15:20:05 +0200 | <kuribas> | I was trying to get $refs to work in openapi (unsuccessful), then I saw your name appear. |
| 2024-05-07 15:21:59 +0200 | ircbrowse_tom | (~ircbrowse@user/tomsmeding/bot/ircbrowse-tom) |
| 2024-05-07 15:22:00 +0200 | Server | +Cnt |
| 2024-05-07 15:23:16 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-07 15:23:46 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:c45d:8c8a:5c4d:ef6b) (Remote host closed the connection) |
| 2024-05-07 15:23:59 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:f7fe:a5d:216b:79ee) |
| 2024-05-07 15:32:38 +0200 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Remote host closed the connection) |
| 2024-05-07 15:35:37 +0200 | <ski> | <Axman6> Any chance we can ban stiell with a message until their connection it sorted out? |
| 2024-05-07 15:35:43 +0200 | <ski> | (timeout one day) |
| 2024-05-07 15:36:52 +0200 | tabemann__ | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) (Quit: Leaving) |
| 2024-05-07 15:37:13 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 15:37:54 +0200 | <ski> | (a forward/redirect ban to ##fix_your_connection (which is forwardable to from any channel) is a common way to indicate this issue) |
| 2024-05-07 15:38:05 +0200 | <Franciman> | does haskell have multi types? |
| 2024-05-07 15:38:17 +0200 | <kuribas> | What are multi types? |
| 2024-05-07 15:38:17 +0200 | <dminuoso> | What is a multi type? |
| 2024-05-07 15:38:27 +0200 | <Franciman> | like intersection types, except non-idempotent |
| 2024-05-07 15:38:44 +0200 | <ski> | no intersection types |
| 2024-05-07 15:38:50 +0200 | <Franciman> | what about multi types then? |
| 2024-05-07 15:38:53 +0200 | <ski> | how would the non-idempotence work ? |
| 2024-05-07 15:38:56 +0200 | <ncf> | is that something you made up? |
| 2024-05-07 15:38:58 +0200 | <Franciman> | no |
| 2024-05-07 15:39:10 +0200 | <Franciman> | ski: you know how you can figure intersection types as "set" types? |
| 2024-05-07 15:39:26 +0200 | <Franciman> | so sigma \cap tau \cap delta is an intersection type, you can represent as a set {sigma, tau, delta} |
| 2024-05-07 15:39:30 +0200 | <tomsmeding> | Franciman: are you interested in whether Haskell2010 has multi types, whether GHC has them, or whether there is a library that emulates them? |
| 2024-05-07 15:39:48 +0200 | <Franciman> | union of all the three |
| 2024-05-07 15:39:51 +0200 | <tomsmeding> | (no, no, maybe) |
| 2024-05-07 15:39:54 +0200 | <Franciman> | i know haskell2010 does not, so the last ones |
| 2024-05-07 15:39:54 +0200 | <ncf> | what's the reference for multi types? |
| 2024-05-07 15:40:18 +0200 | <tomsmeding> | s/maybe/you could change the world here/ |
| 2024-05-07 15:40:25 +0200 | <ski> | `sigma',`cap',`delta' are types as well ? |
| 2024-05-07 15:40:33 +0200 | <Franciman> | \cap is the interseciton in latex, sorry |
| 2024-05-07 15:40:53 +0200 | <Franciman> | https://en.wikipedia.org/wiki/Intersection_type <- this |
| 2024-05-07 15:40:53 +0200 | <ski> | dunno what "you can represent as a set {sigma, tau, delta}" really means, here |
| 2024-05-07 15:41:13 +0200 | <Franciman> | if you remove the axiom that given an intersection type T, T \cap T = T |
| 2024-05-07 15:41:20 +0200 | <tomsmeding> | presumably \Gamma \vdash t : T, where T is a set of types instead of a single type |
| 2024-05-07 15:41:22 +0200 | <Franciman> | you get multi-types, it's a bit like going from sets to multisets |
| 2024-05-07 15:41:25 +0200 | <Franciman> | yes |
| 2024-05-07 15:41:31 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21) |
| 2024-05-07 15:41:33 +0200 | <tomsmeding> | s/set/list/ for multitypes, presumably |
| 2024-05-07 15:41:44 +0200 | <Franciman> | yes |
| 2024-05-07 15:41:50 +0200 | <tomsmeding> | what would unification do, just append the lists? |
| 2024-05-07 15:41:50 +0200 | <Franciman> | except you don't care about ordering |
| 2024-05-07 15:41:56 +0200 | <tomsmeding> | simplifying them in some magical way, perhaps? |
| 2024-05-07 15:41:59 +0200 | <Franciman> | so more accuretely it's a multi set |
| 2024-05-07 15:42:01 +0200 | <tomsmeding> | ah |
| 2024-05-07 15:42:16 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 246 seconds) |
| 2024-05-07 15:42:59 +0200 | <dminuoso> | Well, type-level lists are a thing. |
| 2024-05-07 15:43:05 +0200 | <dminuoso> | '[Int, Int, Double] |
| 2024-05-07 15:43:08 +0200 | <dminuoso> | Is that what you mean, Franciman? |
| 2024-05-07 15:43:13 +0200 | <Franciman> | and can you characterize termination with type level lists? |
| 2024-05-07 15:43:42 +0200 | <Franciman> | depending on the type system you use, you can characterize different types of terminations |
| 2024-05-07 15:43:44 +0200 | <dminuoso> | Not sure what you mean by "characterize termination with type level lists" |
| 2024-05-07 15:43:57 +0200 | <tomsmeding> | type-level lists are simply lists on the type level |
| 2024-05-07 15:44:09 +0200 | <tomsmeding> | you'd still have to write the machinery to interpret them as multitypes |
| 2024-05-07 15:44:14 +0200 | tabemann | (~tabemann@172-13-49-137.lightspeed.milwwi.sbcglobal.net) |
| 2024-05-07 15:44:23 +0200 | <Franciman> | i wonder whether we can encode all the rules |
| 2024-05-07 15:44:23 +0200 | <dminuoso> | Not entirely sure what "interpretation as multitype" even means |
| 2024-05-07 15:44:30 +0200 | <tomsmeding> | perhaps a HList with a suitable API would do |
| 2024-05-07 15:44:48 +0200 | <tomsmeding> | instead of a single value with multiple types, represent the thing as a list of n times the same value, each time with a different type |
| 2024-05-07 15:45:17 +0200 | <Franciman> | are yo ufamiliar with Dezani-Ciancaglini and Coppo's work? |
| 2024-05-07 15:45:19 +0200 | <tomsmeding> | and have an API that interacts with that heterogeneous list so that you can only do things that typecheck with all the types in the type-level index |
| 2024-05-07 15:45:48 +0200 | <tomsmeding> | dminuoso: Franciman is talking about a very different type system where the "kind" (I guess) of the typing judgement is not Env -> Term -> Type but instead Env -> Term -> MultiSet Type |
| 2024-05-07 15:46:25 +0200 | <ncf> | found this https://www.irif.fr/~gmanzone/ens/lambda/notes.pdf |
| 2024-05-07 15:46:38 +0200 | <tomsmeding> | Franciman: I strongly suspect the best answer you're going to get here is, "if you can't find the library on the internet, it probably doesn't exist" |
| 2024-05-07 15:46:52 +0200 | <tomsmeding> | GHC absolutely has no native support for anything in this direction |
| 2024-05-07 15:46:55 +0200 | <Franciman> | yes ncf nice reference |
| 2024-05-07 15:47:01 +0200 | <Franciman> | you could also enjoy |
| 2024-05-07 15:47:02 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-05-07 15:47:05 +0200 | <Franciman> | https://www.irif.fr/~kesner/papers/bucciarelli-kesner-ventura-igpl.pdf this |
| 2024-05-07 15:47:23 +0200 | Lears | (~Leary]@user/Leary/x-0910699) |
| 2024-05-07 15:47:50 +0200 | <ski> | Franciman : are these intersection types supposed to be (or support) "ad hoc" (e.g. being able to intersect `Double' and `Int'), or only being able to take the intersection of features that each of the component types support (like e.g. intersection of fields in record types, but also applied recursively through the structure of types) ? |
| 2024-05-07 15:47:51 +0200 | <ncf> | ha, i took a class by one of these guys (not on multi types, though) |
| 2024-05-07 15:48:30 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 2024-05-07 15:48:56 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) |
| 2024-05-07 15:49:08 +0200 | <Franciman> | ski: depending on the framework you work on |
| 2024-05-07 15:49:34 +0200 | <Franciman> | but if t is a term of type {T_1, T_2} |
| 2024-05-07 15:49:42 +0200 | <Franciman> | then you can deduce both t : T_1 and t : T_2 |
| 2024-05-07 15:49:49 +0200 | [Leary] | (~Leary]@user/Leary/x-0910699) (Ping timeout: 255 seconds) |
| 2024-05-07 15:50:24 +0200 | ski | would really not use set notation here, since it gives misleading connotations |
| 2024-05-07 15:50:30 +0200 | <Franciman> | why not? |
| 2024-05-07 15:50:33 +0200 | <Franciman> | it's exactly the same thing |
| 2024-05-07 15:50:37 +0200 | <Franciman> | thin kabout it |
| 2024-05-07 15:50:59 +0200 | <ski> | because `x in {a,b}' is equivalent to `x = a or x = b', set-theoretically |
| 2024-05-07 15:51:14 +0200 | <Franciman> | UHHHHHHHM okay |
| 2024-05-07 15:51:18 +0200 | <Franciman> | kinda strange minded, but i see it |
| 2024-05-07 15:52:17 +0200 | <ski> | if you write ⌜x : ⋀ {a,b}⌝, that would be okay, from that POV, imho |
| 2024-05-07 15:53:10 +0200 | <ski> | er, well, i suppose ⌜⋂⌝, rather than ⌜⋀⌝, actually |
| 2024-05-07 15:53:38 +0200 | micro | (~micro@user/micro) (Ping timeout: 268 seconds) |
| 2024-05-07 15:53:47 +0200 | <ncf> | so this seems like a restriction of linear logic to just ⊗ and ⊸, where ⊗ can only appear in domains |
| 2024-05-07 15:54:15 +0200 | <ski> | (and you could use multiset/bag brackets, instead of set brackets, so ⌜x : ⋂ ⟅a,b⟆⌝, to emphasize non-idempotence) |
| 2024-05-07 15:56:36 +0200 | <danse-nr3> | fanciest brackets i have seen in a while... |
| 2024-05-07 15:59:30 +0200 | <ski> | "this seems like a restriction of linear logic to just ⊗ and ⊸" -- the aforementioned paper ? |
| 2024-05-07 15:59:41 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2024-05-07 15:59:41 +0200 | <danse-nr3> | i don't know much about multi-types, but intersection types look like interfaces from what i quickly found? Aren't haskell classes something like that? |
| 2024-05-07 16:00:20 +0200 | <ncf> | ski: well i was looking at notes.pdf, i assume they describe the same system |
| 2024-05-07 16:01:16 +0200 | micro | (~micro@user/micro) |
| 2024-05-07 16:01:49 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) |
| 2024-05-07 16:03:22 +0200 | <ski> | Franciman : yea, anyway. the point of my question was really kinda asking about which kind of operational semantics you want .. do you want to pass around multiple values, for a term of an intersection type (and then picking out a part of the intersection corresponds to projecting out the desired value out of those, so more like ad hoc overloading, except also resolvable at run-time) ? or do you intend for |
| 2024-05-07 16:03:23 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 256 seconds) |
| 2024-05-07 16:03:28 +0200 | <ski> | the same run-time value to be simultaneously of all the relevant types (so more like type-erasure for polymorphism, or subsumption for subtyping) ? |
| 2024-05-07 16:05:05 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-07 16:05:55 +0200 | <ski> | Franciman : hm, also, if you have intersection of `tau' and `tau', how does that differ from simply `tau' (so wherein does the non-idempotence lie) ? |
| 2024-05-07 16:08:53 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-07 16:09:00 +0200 | <ski> | "The multi set semantics is in fact exactly the relational semantics of LL restricted to the image of the (CbN) encoding of λ-terms." sounds interesting |
| 2024-05-07 16:09:09 +0200 | <ski> | ("LL" referring to "Linear Logic") |
| 2024-05-07 16:09:35 +0200 | <danse-nr3> | we lost Franciman i am afraid... |
| 2024-05-07 16:09:59 +0200 | <ski> | they might just be swapping and thrashing a bit |
| 2024-05-07 16:10:03 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 16:11:46 +0200 | <ncf> | ski: it seems like the non-idempotence makes a difference because you additionally remove weakening and contraction |
| 2024-05-07 16:12:00 +0200 | ats49 | (~ats@185.57.29.142) |
| 2024-05-07 16:12:08 +0200 | <ncf> | so if a term has type [τ, τ] you can use it twice, basically |
| 2024-05-07 16:12:17 +0200 | <ncf> | s/term/function input/ |
| 2024-05-07 16:12:32 +0200 | <ncf> | s/can/must/? |
| 2024-05-07 16:13:46 +0200 | <ski> | i suppose must, with no weakening |
| 2024-05-07 16:13:57 +0200 | <ski> | modulo presence of modalities like "of course", of course |
| 2024-05-07 16:14:37 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 272 seconds) |
| 2024-05-07 16:14:59 +0200 | <ski> | well, i guess weakening does seem to be implicitly included in rules with zero premisses |
| 2024-05-07 16:15:11 +0200 | <ski> | (see `ax', page 4) |
| 2024-05-07 16:16:03 +0200 | <ncf> | that's the "set types" system |
| 2024-05-07 16:16:10 +0200 | <ski> | mhm |
| 2024-05-07 16:16:11 +0200 | <ncf> | ax rule for multi types is on page 8 |
| 2024-05-07 16:16:26 +0200 | ski | 's still skimming back and forth a bit |
| 2024-05-07 16:16:38 +0200 | <ski> | right |
| 2024-05-07 16:17:47 +0200 | <ski> | now i'm wondering whether contexts can include multiple typings for the same identifier (and whether the function abstraction just removes one of them) |
| 2024-05-07 16:19:03 +0200 | <ncf> | seems like contexts are assignments of multisets to variables |
| 2024-05-07 16:19:24 +0200 | <ncf> | so, no, but yes |
| 2024-05-07 16:19:31 +0200 | ats49 | (~ats@185.57.29.142) (Ping timeout: 250 seconds) |
| 2024-05-07 16:21:40 +0200 | <ski> | mm, so they're gathered together |
| 2024-05-07 16:22:40 +0200 | johnw | (~johnw@69.62.242.138) (Ping timeout: 255 seconds) |
| 2024-05-07 16:22:53 +0200 | johnw | (~johnw@69.62.242.138) |
| 2024-05-07 16:24:27 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) (Remote host closed the connection) |
| 2024-05-07 16:24:51 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) |
| 2024-05-07 16:25:29 +0200 | lg188 | (~lg188@82.18.98.230) (Ping timeout: 256 seconds) |
| 2024-05-07 16:28:13 +0200 | <Franciman> | sorry here i am |
| 2024-05-07 16:28:15 +0200 | <Franciman> | i was in the bathroom |
| 2024-05-07 16:28:28 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 16:28:30 +0200 | <Franciman> | ski: eheheh, you can use the non-idempotence to count the number of occurrences of a term |
| 2024-05-07 16:28:36 +0200 | <Franciman> | that's where things get kinda interesting :D |
| 2024-05-07 16:28:52 +0200 | <Franciman> | EXACTLY |
| 2024-05-07 16:28:59 +0200 | <Franciman> | multi-types is related to linear logic and resource management |
| 2024-05-07 16:29:27 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 16:29:39 +0200 | <ski> | i'm wondering about an example of a term with an intersection type of `sigma' and `tau', where those two are not identical types |
| 2024-05-07 16:29:46 +0200 | <Franciman> | yes ski |
| 2024-05-07 16:29:49 +0200 | <Franciman> | (\x. x x) |
| 2024-05-07 16:30:11 +0200 | <Franciman> | it has type [[sigma], [sigma]->tau] -> tau |
| 2024-05-07 16:30:25 +0200 | <Franciman> | so in there, x : [sigma, [sigma]-> tau] |
| 2024-05-07 16:30:27 +0200 | <ski> | (\x. x x) : tau where tau = tau -> omega |
| 2024-05-07 16:30:52 +0200 | <ski> | (this works with `ocaml -rectypes', if you try `fun x -> x x') |
| 2024-05-07 16:31:00 +0200 | <Franciman> | as the word says: fun! |
| 2024-05-07 16:33:38 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 2024-05-07 16:34:27 +0200 | <Franciman> | also, do get me for an expert, i'm just learning, and i was wondering whether i could use haskell to experiment |
| 2024-05-07 16:34:36 +0200 | <ski> | # fun x -> x x;; |
| 2024-05-07 16:34:38 +0200 | <ski> | - : ('a -> 'b as 'a) -> 'b = <fun> |
| 2024-05-07 16:34:52 +0200 | <ski> | # let foo : 'tau -> 'omega as 'tau = fun x -> x x;; |
| 2024-05-07 16:34:54 +0200 | <ski> | val foo : 'a -> 'omega as 'a = <fun> |
| 2024-05-07 16:35:28 +0200 | <ski> | you can experiment with a lot of things, in Haskell |
| 2024-05-07 16:35:42 +0200 | <ski> | e.g. writing your own type system or language prototypes |
| 2024-05-07 16:36:23 +0200 | <ski> | or fiddling around with trying to encode some effect of feature, in terms of existing Haskell language features or extensions |
| 2024-05-07 16:37:40 +0200 | <ski> | (experimenting with type systems stuff can also be fun to do, in e.g. lambdaProlog, Twelf, Agda, or somesuch) |
| 2024-05-07 16:40:03 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 16:40:28 +0200 | <ski> | (lambdaProlog is a logic programming language with support for lambda terms (including (incomplete) unification), you can use this to do HOAS (higher-order abstract syntax), including being able to match under the (meta-)lambdas. Twelf is like a dependently typed version of lambdaProlog, kinda. but you can still do ordinary logic programming in it, e.g. to search for proofs. you can also use its mode system |
| 2024-05-07 16:40:35 +0200 | <ski> | to prove meta-theorems. Agda is a dependently typed language based on functional programming, rather than logic programming) |
| 2024-05-07 16:40:36 +0200 | <Franciman> | lambdaProlog is damn kewl |
| 2024-05-07 16:40:41 +0200 | <ski> | it sure is |
| 2024-05-07 16:43:11 +0200 | <ski> | (Twelf also has HOAS support, including matching, in case that wasn't clear from what i said. in Agda, you can't match on functions (apart from calling them), since they're computational .. except that sometimes you do know statically/definitionally something about them. lambdaProlog (and Twelf) doesn't have (full) computational terms, there's only beta- and eta- conversion for functions, there's no `case', |
| 2024-05-07 16:43:17 +0200 | <ski> | no recursion for functions. you do your computation with predicates/relations, instead) |
| 2024-05-07 16:44:49 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 2024-05-07 16:46:17 +0200 | dtman34 | (~dtman34@2601:447:d001:ed50:f596:52e1:73ca:629d) |
| 2024-05-07 16:48:17 +0200 | <ski> | (lambdaProlog (and Twelf) also has, from a logic programming standpoint, support for locally assuming extra clauses for predicates, and locally introducing new constants (skolems) of given types. e.g. when you traverse an AST with a bound variable, you locally introduce a new constant, substituting it for the bound variable in the AST, and commonly also locally assume some extra clauses for the constant, |
| 2024-05-07 16:48:23 +0200 | <ski> | e.g. it being assigned a given (object type) (if doing type checking/inference), before traversing into the body of the binder. these local constants and assumptions then automatically vanish after the completion of that, unlike using assert[az]/1,retract/1,gensym/1 in Prolog) |
| 2024-05-07 16:51:08 +0200 | <ski> | (from a programming standpoint, these features are a kind of dynamic scope thing, and can be used for somewhat similar effect you could use dynamic scope for in other languages. it's just that they also have a perfectly sensible logical/declarative semantics here (meaning of implication, and of universal quantification)) |
| 2024-05-07 16:53:23 +0200 | lg188 | (~lg188@82.18.98.230) |
| 2024-05-07 16:57:18 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) |
| 2024-05-07 16:59:31 +0200 | img | (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 17:00:26 +0200 | <lortabac> | ski: that's the feature I miss the most in Prolog |
| 2024-05-07 17:00:29 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Ping timeout: 240 seconds) |
| 2024-05-07 17:00:34 +0200 | <lortabac> | I didn't know lambdaProlog had it |
| 2024-05-07 17:00:39 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-05-07 17:01:04 +0200 | <lortabac> | having to define everything at top-level is annoying sometimes |
| 2024-05-07 17:01:28 +0200 | img | (~img@user/img) |
| 2024-05-07 17:01:45 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) (Ping timeout: 256 seconds) |
| 2024-05-07 17:01:52 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-07 17:04:29 +0200 | lg188 | (~lg188@82.18.98.230) (Ping timeout: 252 seconds) |
| 2024-05-07 17:07:44 +0200 | lg188 | (~lg188@82.18.98.230) |
| 2024-05-07 17:08:02 +0200 | lg188 | (~lg188@82.18.98.230) (Client Quit) |
| 2024-05-07 17:08:28 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) |
| 2024-05-07 17:10:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 2024-05-07 17:10:08 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 17:10:16 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 260 seconds) |
| 2024-05-07 17:13:49 +0200 | Mach | (~Mach@86.127.202.233) |
| 2024-05-07 17:14:24 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 255 seconds) |
| 2024-05-07 17:21:43 +0200 | falafel | (~falafel@211.184.50.36) (Ping timeout: 260 seconds) |
| 2024-05-07 17:27:09 +0200 | <kuribas> | Can you program in these languages? |
| 2024-05-07 17:27:21 +0200 | <kuribas> | Or are they more theorem provers/research languages? |
| 2024-05-07 17:27:38 +0200 | <kuribas> | A statically typed prolog sounds appealing :) |
| 2024-05-07 17:27:54 +0200 | agent314 | (~quassel@static-198-54-134-186.cust.tzulo.com) (Ping timeout: 255 seconds) |
| 2024-05-07 17:35:38 +0200 | agent314 | (~quassel@static-198-54-134-186.cust.tzulo.com) |
| 2024-05-07 17:36:48 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 17:37:06 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 17:37:25 +0200 | Square3 | (~Square4@user/square) |
| 2024-05-07 17:41:20 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-07 17:41:33 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2024-05-07 17:42:28 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) |
| 2024-05-07 17:45:35 +0200 | danse-nr3 | (~danse-nr3@151.43.102.160) (Ping timeout: 264 seconds) |
| 2024-05-07 17:45:52 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2024-05-07 17:47:22 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 17:47:40 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 17:48:52 +0200 | nschoe | (~nschoe@2a01:e0a:8e:a190:6f57:1144:3b82:7ce1) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-05-07 17:49:09 +0200 | nschoe | (~nschoe@82-65-202-30.subs.proxad.net) |
| 2024-05-07 17:58:19 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 17:58:35 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 17:59:21 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 18:00:35 +0200 | agent314 | (~quassel@static-198-54-134-186.cust.tzulo.com) (Ping timeout: 252 seconds) |
| 2024-05-07 18:03:43 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 260 seconds) |
| 2024-05-07 18:08:14 +0200 | glguy | (g@libera/staff/glguy) (Quit: Quit) |
| 2024-05-07 18:09:26 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-05-07 18:09:54 +0200 | glguy | (g@libera/staff/glguy) |
| 2024-05-07 18:13:45 +0200 | philopsos | (~caecilius@user/philopsos) |
| 2024-05-07 18:14:53 +0200 | <ski> | kuribas : you can program in lambdaProlog, it has I/O and stuff. Twelf doesn't have any built-in I/O though, apart from the interactor (though i str seeing some program used to wrap that, feeding the interactor with queries, then parsing the result substitutions and doing something with them) |
| 2024-05-07 18:17:15 +0200 | darius87 | (~darius@93.126.130.253) |
| 2024-05-07 18:17:19 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 268 seconds) |
| 2024-05-07 18:18:09 +0200 | <ski> | kuribas : for statically typed Prolog, Mercury might be closer, though. it has predicates/relations as well as functions (both can be higher-order), statical types, statical modes (& insts) and determinisms, (parameterizable) algebraic data types, parametric polymorphism, type classes (not higher-order, though), existentials (actual existential quantification, also output type class constraints) |
| 2024-05-07 18:20:00 +0200 | <ski> | oh, and it's purely declarative, no side-effects (well, it also has an impurity tracking system, but it's mainly used for FFI stuff, before wrapping in a pure interface), it does I/O and mutable data structures through uniqueness (similar to Clean, except that Mercury tracks this in insts (instantiation states), not in types), you thread an I/O state through your I/O interactions |
| 2024-05-07 18:20:03 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-05-07 18:20:12 +0200 | <ski> | see <https://www.mercurylang.org/> and #mercury |
| 2024-05-07 18:21:13 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |
| 2024-05-07 18:21:50 +0200 | <ski> | @tell lortabac well, having locally (lexically/scoped) definitions isn't quite the same thing as what i was talking about in lambdaProlog (although you can also lexically scope some clauses defining a predicate, over (part of) another predicate clause, if you wish to) |
| 2024-05-07 18:21:50 +0200 | <lambdabot> | Consider it noted. |
| 2024-05-07 18:22:35 +0200 | darius87 | (~darius@93.126.130.253) (Quit: Client closed) |
| 2024-05-07 18:24:16 +0200 | <ski> | lambdaProlog has .. more or less, algebraic datatypes (but you don't declare the constructors together with the type, in a single declaration. and you can, later, declare more constructors, if you want to. although, with the module system of Teyjus (a compiler for lambdaProlog, compiling to a bytecode for a WAM-like machine, similar to many Prolog implementations), iirc, you can restrict who (if anyone) can |
| 2024-05-07 18:24:22 +0200 | <ski> | later add more constructors (or new clauses for a predicate, for that matter) |
| 2024-05-07 18:24:35 +0200 | <ski> | it also has parametric polymorphism, but no dependent types |
| 2024-05-07 18:26:47 +0200 | <ski> | if one consider the HOAS representation (including some kind of unification of lambda terms, up to alpha, beta, and eta conversion) a killer feature of lambdaProlog (and Twelf), then that's the reason it also has implicational goals, and universal quantification goals, because without the latter two, the first one is not as useful |
| 2024-05-07 18:28:17 +0200 | philopsos | (~caecilius@user/philopsos) (Quit: Lost terminal) |
| 2024-05-07 18:28:19 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-05-07 18:28:27 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 2024-05-07 18:28:41 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) |
| 2024-05-07 18:28:42 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:f7fe:a5d:216b:79ee) (Remote host closed the connection) |
| 2024-05-07 18:28:47 +0200 | <ski> | however, iirc, there's an implementation of (a restriction of) Lolli (called LolliMon, iirc), which uses a more Prolog-like syntax (uncurried rather than curried predicates), which doesn't have lambda-terms, but does have implication and universal quantification goals, so evidently people considered the latter two useful even without the former |
| 2024-05-07 18:29:18 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 18:29:35 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Quit: ERC (IRC client for Emacs 27.1)) |
| 2024-05-07 18:29:37 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 18:29:54 +0200 | <ski> | (Lolli is a version of lambdaProlog using linear logic. it is dynamically typed) |
| 2024-05-07 18:30:03 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-05-07 18:30:55 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 18:31:17 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-07 18:31:25 +0200 | <ski> | lambdaProlog <https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/>,Lolli <https://www.lix.polytechnique.fr/Labo/Dale.Miller/lolli/> |
| 2024-05-07 18:31:49 +0200 | <ski> | Twelf <https://twelf.org/> |
| 2024-05-07 18:39:07 +0200 | tzh | (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 2024-05-07 18:40:07 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 18:42:11 +0200 | philopsos | (~caecilius@user/philopsos) |
| 2024-05-07 18:44:29 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 240 seconds) |
| 2024-05-07 18:49:29 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-07 18:52:53 +0200 | dostoyevsky2 | (~sck@user/dostoyevsky2) (Ping timeout: 240 seconds) |
| 2024-05-07 18:53:18 +0200 | rosco | (~rosco@yp-146-6.tm.net.my) (Quit: Lost terminal) |
| 2024-05-07 18:57:09 +0200 | dostoyevsky2 | (~sck@user/dostoyevsky2) |
| 2024-05-07 19:01:06 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 19:01:14 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Ping timeout: 260 seconds) |
| 2024-05-07 19:01:42 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-07 19:04:23 +0200 | Square3 | (~Square4@user/square) (Ping timeout: 252 seconds) |
| 2024-05-07 19:05:32 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 260 seconds) |
| 2024-05-07 19:15:20 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 260 seconds) |
| 2024-05-07 19:15:27 +0200 | xal | (~xal@mx1.xal.systems) () |
| 2024-05-07 19:16:14 +0200 | Square | (~Square@user/square) |
| 2024-05-07 19:16:28 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-05-07 19:17:59 +0200 | AlexZenon | (~alzenon@178.34.162.125) (Ping timeout: 264 seconds) |
| 2024-05-07 19:18:49 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-05-07 19:19:14 +0200 | danza | (~francesco@151.47.243.64) |
| 2024-05-07 19:19:57 +0200 | Mach | (~Mach@86.127.202.233) (Ping timeout: 255 seconds) |
| 2024-05-07 19:20:44 +0200 | xal | (~xal@mx1.xal.systems) |
| 2024-05-07 19:20:49 +0200 | xal | (~xal@mx1.xal.systems) (Client Quit) |
| 2024-05-07 19:21:57 +0200 | xal | (~xal@mx1.xal.systems) |
| 2024-05-07 19:21:59 +0200 | Rodney_ | (~Rodney@176.254.244.83) (Ping timeout: 252 seconds) |
| 2024-05-07 19:22:01 +0200 | danza | (~francesco@151.47.243.64) (Remote host closed the connection) |
| 2024-05-07 19:22:15 +0200 | AlexZenon | (~alzenon@178.34.162.125) |
| 2024-05-07 19:22:30 +0200 | danza | (~francesco@151.47.243.64) |
| 2024-05-07 19:23:24 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 19:23:33 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 2024-05-07 19:24:32 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 268 seconds) |
| 2024-05-07 19:25:20 +0200 | danza | (~francesco@151.47.243.64) (Remote host closed the connection) |
| 2024-05-07 19:25:44 +0200 | danza | (~francesco@151.47.243.64) |
| 2024-05-07 19:28:14 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 268 seconds) |
| 2024-05-07 19:33:11 +0200 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2024-05-07 19:34:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-05-07 19:38:56 +0200 | gentauro | (~gentauro@user/gentauro) |
| 2024-05-07 19:40:16 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 19:41:23 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 19:41:23 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 19:42:20 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2024-05-07 19:45:13 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 19:45:31 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 272 seconds) |
| 2024-05-07 19:46:03 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-05-07 19:47:36 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 19:47:48 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 19:49:26 +0200 | danza | (~francesco@151.47.243.64) (Remote host closed the connection) |
| 2024-05-07 19:49:48 +0200 | danza | (~francesco@151.47.243.64) |
| 2024-05-07 19:49:57 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 2024-05-07 19:50:22 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) |
| 2024-05-07 19:50:55 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 19:51:12 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 19:51:33 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 19:52:11 +0200 | aforemny | (~aforemny@i59F516E3.versanet.de) (Ping timeout: 264 seconds) |
| 2024-05-07 19:52:50 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 19:52:55 +0200 | danza | (~francesco@151.47.243.64) (Max SendQ exceeded) |
| 2024-05-07 19:53:29 +0200 | danza | (~francesco@151.47.243.64) |
| 2024-05-07 19:53:51 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 19:54:19 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 19:54:20 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 19:54:33 +0200 | aforemny | (~aforemny@2001:9e8:6ccb:f700:5472:d92b:ff7e:d848) |
| 2024-05-07 19:54:35 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-05-07 19:55:05 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 19:56:31 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 19:58:31 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 19:58:50 +0200 | danza | (~francesco@151.47.243.64) (Ping timeout: 252 seconds) |
| 2024-05-07 19:59:17 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 240 seconds) |
| 2024-05-07 19:59:40 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 20:00:05 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:00:29 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 240 seconds) |
| 2024-05-07 20:00:29 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:03:21 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-07 20:03:56 +0200 | infinity0 | (~infinity0@pwned.gg) (Remote host closed the connection) |
| 2024-05-07 20:04:20 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 252 seconds) |
| 2024-05-07 20:04:48 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-05-07 20:05:25 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 20:06:03 +0200 | infinity0 | (~infinity0@pwned.gg) |
| 2024-05-07 20:06:17 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:06:19 +0200 | qqq | (~qqq@92.43.167.61) |
| 2024-05-07 20:08:13 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 20:12:40 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 20:12:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:13:15 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 268 seconds) |
| 2024-05-07 20:14:41 +0200 | todi1 | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-07 20:14:51 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 20:16:00 +0200 | aforemny_ | (~aforemny@2001:9e8:6ccc:2700:d136:8946:ee2b:ef44) |
| 2024-05-07 20:16:16 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 20:16:48 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 20:17:15 +0200 | aforemny | (~aforemny@2001:9e8:6ccb:f700:5472:d92b:ff7e:d848) (Ping timeout: 256 seconds) |
| 2024-05-07 20:18:30 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:19:57 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-05-07 20:19:57 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:19:58 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 2024-05-07 20:20:23 +0200 | todi1 | todi |
| 2024-05-07 20:22:21 +0200 | mei | (~mei@user/mei) |
| 2024-05-07 20:25:46 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:27:09 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:27:43 +0200 | aforemny | (~aforemny@i59F516ED.versanet.de) |
| 2024-05-07 20:28:03 +0200 | aforemny_ | (~aforemny@2001:9e8:6ccc:2700:d136:8946:ee2b:ef44) (Ping timeout: 268 seconds) |
| 2024-05-07 20:29:30 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-05-07 20:30:17 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-07 20:30:18 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-05-07 20:33:00 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:33:59 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 20:34:14 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-05-07 20:36:41 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2024-05-07 20:36:41 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:37:12 +0200 | disgrunt | (~disgrunt@129.176.64.49) |
| 2024-05-07 20:37:36 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) |
| 2024-05-07 20:38:51 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 268 seconds) |
| 2024-05-07 20:38:53 +0200 | <disgrunt> | This is less a Haskell question and more a general knowledge of lambda calculus (hopefully to understand and implement a calculus of constructions): Is there a good book that can teach the theory and notation to a skilled procedural language programmer? |
| 2024-05-07 20:40:41 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 20:40:51 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-05-07 20:42:14 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:42:47 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:43:31 +0200 | ft | (~ft@p3e9bc1bf.dip0.t-ipconnect.de) |
| 2024-05-07 20:43:57 +0200 | phma | (phma@2001:5b0:211f:8748:d5d8:f6f:3f3d:8bcc) (Read error: Connection reset by peer) |
| 2024-05-07 20:47:39 +0200 | euleritian | (~euleritia@dynamic-176-004-187-187.176.4.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-07 20:47:57 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-07 20:48:27 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:49:59 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:50:45 +0200 | <monochrom> | Go straight to setting yourself up for calculi of constructions: Read the official book for Coq or the official book for Lean. |
| 2024-05-07 20:51:07 +0200 | <monochrom> | or the official book for Agda. |
| 2024-05-07 20:52:19 +0200 | <ncf> | maybe https://kar.kent.ac.uk/20998/1/ttfp.pdf |
| 2024-05-07 20:52:35 +0200 | <monochrom> | Because every book that says "lambda calculus" in the title is heading to somewhere else right after the basic (the first 10%). |
| 2024-05-07 20:53:53 +0200 | <disgrunt> | monochrom: I'm interested in implementing something like Coq or Lean and not using it. |
| 2024-05-07 20:54:46 +0200 | <monochrom> | But you first learn what it should look like to users (the specification) before there is anything to implement for. |
| 2024-05-07 20:55:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 20:55:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 20:55:48 +0200 | <monochrom> | And they teach calculi of constructions. |
| 2024-05-07 20:56:09 +0200 | <disgrunt> | Thanks all for the input. |
| 2024-05-07 20:57:02 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 2024-05-07 20:59:41 +0200 | <mauke> | petition to rename "calculus" to "pebble" |
| 2024-05-07 21:00:22 +0200 | <monochrom> | Pebbles of construction will brick your home router! >:) |
| 2024-05-07 21:00:32 +0200 | <glguy> | Sorry, we're not currently accepting rename requests for calculus |
| 2024-05-07 21:01:52 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 21:01:52 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 21:02:25 +0200 | <monochrom> | Hell, s/10%/1%/ |
| 2024-05-07 21:04:34 +0200 | <mauke> | also, "lambda" is just greek for L, so lambda calculus => the L pebble |
| 2024-05-07 21:04:51 +0200 | <monochrom> | No, lowercase l :) |
| 2024-05-07 21:05:22 +0200 | <int-e> | mauke: so how is life in your house of pebbles? |
| 2024-05-07 21:05:31 +0200 | <kaol> | Anyone have more than 32GB RAM? I'd be interested to hear how much more is enough to run the 25m dataset on my little program. https://gitlab.com/kaol/recommender-als |
| 2024-05-07 21:06:14 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 21:06:29 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 21:06:41 +0200 | chele | (~chele@user/chele) (Ping timeout: 256 seconds) |
| 2024-05-07 21:07:16 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 21:08:05 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 21:08:33 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 21:08:40 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 2024-05-07 21:08:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer) |
| 2024-05-07 21:09:21 +0200 | FinnElija | (~finn_elij@user/finn-elija/x-0085643) |
| 2024-05-07 21:10:49 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 21:13:05 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 252 seconds) |
| 2024-05-07 21:13:57 +0200 | <meejah> | shapr does ;) |
| 2024-05-07 21:15:06 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 256 seconds) |
| 2024-05-07 21:16:20 +0200 | disgrunt | (~disgrunt@129.176.64.49) (Quit: Boom.) |
| 2024-05-07 21:17:02 +0200 | sp1ff | (~user@c-24-21-45-157.hsd1.wa.comcast.net) |
| 2024-05-07 21:19:02 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-05-07 21:20:30 +0200 | madeleine-sydney | (~madeleine@c-71-229-185-228.hsd1.co.comcast.net) |
| 2024-05-07 21:23:35 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 21:31:14 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-05-07 21:32:44 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-05-07 21:35:36 +0200 | <energizer> | is there a value x that trying to do anything with it other than `isx x` will fail? even identity or putting it in a list |
| 2024-05-07 21:35:38 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-05-07 21:36:08 +0200 | <tomsmeding> | is not the whole point of polymorphism that you can instantiate a type variable with _anything_ |
| 2024-05-07 21:36:28 +0200 | <tomsmeding> | I mean, I guess an unboxed value would count as "cannot put it in a list" |
| 2024-05-07 21:36:39 +0200 | <tomsmeding> | but that's incidental, you can write a list type of unboxed integers and then you can put one in there |
| 2024-05-07 21:37:23 +0200 | <ncf> | what's isx? |
| 2024-05-07 21:38:23 +0200 | <mauke> | six but spelled sideways |
| 2024-05-07 21:38:23 +0200 | <energizer> | is x |
| 2024-05-07 21:40:08 +0200 | <energizer> | what's the difference between this x and `undefined`? |
| 2024-05-07 21:40:21 +0200 | <tomsmeding> | I can put 'undefined' in a list |
| 2024-05-07 21:42:00 +0200 | <mauke> | > length [undefined, undefined] |
| 2024-05-07 21:42:01 +0200 | <lambdabot> | 2 |
| 2024-05-07 21:42:44 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-05-07 21:42:55 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 21:47:34 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 255 seconds) |
| 2024-05-07 21:49:50 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-07 21:50:03 +0200 | Rodney_ | (~Rodney@176.254.244.83) |
| 2024-05-07 21:50:24 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-05-07 21:51:19 +0200 | <EvanR> | it sounds like x isn't much of a value |
| 2024-05-07 21:51:26 +0200 | phma | (~phma@2001:5b0:212a:9dd8:b0f:f357:db6e:4d49) |
| 2024-05-07 21:51:28 +0200 | <EvanR> | since it seems to know about the context it is used in |
| 2024-05-07 21:53:15 +0200 | <EvanR> | like a $20 bill that you somehow can't spent except on a specific commodity |
| 2024-05-07 21:54:19 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 255 seconds) |
| 2024-05-07 21:54:20 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 21:56:34 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-05-07 22:01:05 +0200 | <monochrom> | My question is: What is the motivation? There is a better question behind this. |
| 2024-05-07 22:03:01 +0200 | <monochrom> | Alternatively, let's use minimalism. Don't even provide x and isx. Then no one can use them wrong. |
| 2024-05-07 22:03:29 +0200 | <monochrom> | More people should use the subtraction method. Delete more code. |
| 2024-05-07 22:04:29 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 22:04:33 +0200 | <EvanR> | that would not satisfy one of the goals "x exists" |
| 2024-05-07 22:04:52 +0200 | <EvanR> | constructively speaking |
| 2024-05-07 22:05:06 +0200 | <glguy> | Maybe we need universities to run introduction to deprogramming courses |
| 2024-05-07 22:05:10 +0200 | <monochrom> | You can always remember x. Then it exists in your mind, and no one can take it away. Or use it wrong. :) |
| 2024-05-07 22:05:58 +0200 | <monochrom> | But s/$20 bill/$20 coupon/ and that one is a pretty common thing IRL. :) |
| 2024-05-07 22:06:57 +0200 | <monochrom> | In which case the better analogy is "$20 coupon but you can only put it in your left pocket not the right pocket" which is WTF and that would be right, WTF. |
| 2024-05-07 22:07:00 +0200 | <EvanR> | yeah but imagine if it was a real legal tender $20 USD note, or canadian if necessary, it just doesn't work |
| 2024-05-07 22:07:32 +0200 | <monochrom> | Oh I'm just sharpening the analogy. I'm with you. :) |
| 2024-05-07 22:07:40 +0200 | <EvanR> | as if anyone you presented it to could see some identifying mark and it was a vast conspiracy |
| 2024-05-07 22:08:32 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 22:08:36 +0200 | <EvanR> | oh yeah, only goes in left pocket is a good one |
| 2024-05-07 22:08:49 +0200 | causal | (~eric@50.35.88.207) |
| 2024-05-07 22:08:50 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-05-07 22:09:42 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) |
| 2024-05-07 22:11:07 +0200 | <cheater> | energizer: it's easy to create something like this in the following way |
| 2024-05-07 22:11:22 +0200 | <cheater> | 1. start a new module |
| 2024-05-07 22:11:27 +0200 | <cheater> | 2. add x :: MySpecialType |
| 2024-05-07 22:11:40 +0200 | <cheater> | 3. add isx :: MySpecialType -> Bool |
| 2024-05-07 22:11:59 +0200 | <cheater> | 4. export x, isx, and not MySpecialType |
| 2024-05-07 22:12:10 +0200 | <tomsmeding> | then you can still put x in a list |
| 2024-05-07 22:12:18 +0200 | <cheater> | right |
| 2024-05-07 22:12:24 +0200 | <cheater> | i was just getting to that |
| 2024-05-07 22:12:29 +0200 | <cheater> | so like |
| 2024-05-07 22:12:44 +0200 | <monochrom> | It is perhaps acceptable. This is why the better answer is asking back "what is the motivation?" like I did. |
| 2024-05-07 22:12:45 +0200 | <cheater> | wouldn't making MySpecialType a different kind than Type be a good way of stopping that from happening? |
| 2024-05-07 22:13:03 +0200 | <tomsmeding> | covered that with unboxed ints above |
| 2024-05-07 22:13:05 +0200 | <tomsmeding> | I concur with monochrom |
| 2024-05-07 22:13:08 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 260 seconds) |
| 2024-05-07 22:13:19 +0200 | <cheater> | right |
| 2024-05-07 22:13:21 +0200 | <EvanR> | make a custom kind and don't export the kind xD |
| 2024-05-07 22:13:27 +0200 | <cheater> | hmm |
| 2024-05-07 22:13:30 +0200 | <cheater> | is that a thing? |
| 2024-05-07 22:13:37 +0200 | <tomsmeding> | then I make a polykinded list type lol |
| 2024-05-07 22:13:37 +0200 | <cheater> | could this work? |
| 2024-05-07 22:13:39 +0200 | <EvanR> | then you can't even create your own custom kind list |
| 2024-05-07 22:13:43 +0200 | <EvanR> | oh |
| 2024-05-07 22:13:48 +0200 | phma | (~phma@2001:5b0:212a:9dd8:b0f:f357:db6e:4d49) (Read error: Connection reset by peer) |
| 2024-05-07 22:14:57 +0200 | <EvanR> | x is a value which can only be used with the function isx and this sentence defining itself |
| 2024-05-07 22:15:34 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 22:15:36 +0200 | <EvanR> | (this should put an end to the convo) |
| 2024-05-07 22:16:03 +0200 | <EvanR> | (you can't even undefine ..... it) |
| 2024-05-07 22:16:21 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 22:18:47 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 22:19:10 +0200 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) (Ping timeout: 246 seconds) |
| 2024-05-07 22:23:17 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 22:23:51 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 272 seconds) |
| 2024-05-07 22:27:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-07 22:32:25 +0200 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) |
| 2024-05-07 22:34:27 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21) (Remote host closed the connection) |
| 2024-05-07 22:37:34 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 22:39:21 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-07 22:39:41 +0200 | phma | (phma@2001:5b0:211b:8f38:94dd:3277:4b6:fb28) |
| 2024-05-07 22:40:46 +0200 | forell | (~forell@user/forell) (Ping timeout: 264 seconds) |
| 2024-05-07 22:41:19 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 2024-05-07 22:41:41 +0200 | madariaga | (~madariaga@user/madariaga) (Ping timeout: 240 seconds) |
| 2024-05-07 22:41:53 +0200 | forell | (~forell@user/forell) |
| 2024-05-07 22:51:30 +0200 | Square3 | (~Square4@user/square) |
| 2024-05-07 22:52:05 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |
| 2024-05-07 22:54:35 +0200 | Square | (~Square@user/square) (Ping timeout: 264 seconds) |
| 2024-05-07 22:57:04 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-07 22:57:13 +0200 | ray_caster | (~ray_caste@2001:2043:5d2e:300:6c11:a14c:9e59:df7c) |
| 2024-05-07 22:57:35 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 252 seconds) |
| 2024-05-07 22:58:47 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 22:59:24 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 23:00:29 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 23:01:23 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 23:04:42 +0200 | madariaga | (~madariaga@user/madariaga) |
| 2024-05-07 23:05:47 +0200 | ray_caster | (~ray_caste@2001:2043:5d2e:300:6c11:a14c:9e59:df7c) (Good Bye) |
| 2024-05-07 23:07:12 +0200 | madariaga | (~madariaga@user/madariaga) (Client Quit) |
| 2024-05-07 23:08:42 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-07 23:11:09 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-05-07 23:11:21 +0200 | demon-cat | (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2024-05-07 23:14:35 +0200 | wroathe | (~wroathe@24-152-179-157.fttp.usinternet.com) |
| 2024-05-07 23:14:35 +0200 | wroathe | (~wroathe@24-152-179-157.fttp.usinternet.com) (Changing host) |
| 2024-05-07 23:14:35 +0200 | wroathe | (~wroathe@user/wroathe) |
| 2024-05-07 23:15:22 +0200 | wroathe | (~wroathe@user/wroathe) (Client Quit) |
| 2024-05-07 23:15:44 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 252 seconds) |
| 2024-05-07 23:17:00 +0200 | wroathe | (~wroathe@24-152-179-157.fttp.usinternet.com) |
| 2024-05-07 23:17:00 +0200 | wroathe | (~wroathe@24-152-179-157.fttp.usinternet.com) (Changing host) |
| 2024-05-07 23:17:00 +0200 | wroathe | (~wroathe@user/wroathe) |