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