Logs on 2024-06-19 (liberachat/#haskell)
| 00:14:57 | → | dysthesis joins (~dysthesis@user/dysthesis) |
| 00:17:43 | × | xff0x quits (~xff0x@2405:6580:b080:900:fd6a:2265:c425:f820) (Ping timeout: 272 seconds) |
| 00:22:22 | → | jcarpenter2 joins (~lol@2603:3016:1e01:b960:a570:a53a:e862:a200) |
| 00:24:12 | × | Roc quits (~Roc@ip-213-49-101-14.dsl.scarlet.be) (Quit: Client closed) |
| 00:27:53 | × | myme quits (~myme@2a01:799:d5c:5f00:33d4:3d73:88f6:3af4) (Quit: WeeChat 4.2.2) |
| 00:32:09 | × | henry40408 quits (~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds)) |
| 00:32:33 | → | henry40408 joins (~henry4040@175.182.111.183) |
| 00:46:27 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 256 seconds) |
| 00:56:58 | → | madhavanmiui joins (~madhavanm@2409:40f4:1d:7cf9:8000::) |
| 01:03:32 | × | pointlessslippe1 quits (~pointless@212.82.82.3) (Ping timeout: 268 seconds) |
| 01:09:48 | × | madhavanmiui quits (~madhavanm@2409:40f4:1d:7cf9:8000::) (Quit: Quit) |
| 01:13:47 | → | pointlessslippe1 joins (~pointless@212.82.82.3) |
| 01:27:35 | × | erty` quits (~user@122.161.50.232) (Ping timeout: 268 seconds) |
| 01:35:56 | × | dysthesis quits (~dysthesis@user/dysthesis) (Quit: dysthesis) |
| 01:38:45 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 01:57:15 | × | henry40408 quits (~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds)) |
| 01:57:43 | → | henry40408 joins (~henry4040@175.182.111.183) |
| 02:02:52 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 246 seconds) |
| 02:05:02 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 02:09:24 | → | causal joins (~eric@50.35.88.207) |
| 02:11:26 | → | Leary joins (~Leary@user/Leary/x-0910699) |
| 02:19:12 | × | euleritian quits (~euleritia@dynamic-176-003-069-120.176.3.pool.telefonica.de) (Read error: Connection reset by peer) |
| 02:19:29 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 02:36:54 | → | rosco joins (~rosco@175.136.155.137) |
| 02:48:53 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 240 seconds) |
| 02:57:15 | × | td_ quits (~td@i53870936.versanet.de) (Ping timeout: 264 seconds) |
| 02:59:00 | → | td_ joins (~td@i53870921.versanet.de) |
| 03:17:35 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 03:24:08 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 268 seconds) |
| 03:38:26 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 03:44:11 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 268 seconds) |
| 03:45:39 | → | aforemny joins (~aforemny@2001:9e8:6cc0:df00:949a:33df:9d68:3e31) |
| 03:46:07 | × | aforemny_ quits (~aforemny@2001:9e8:6cdf:6100:2338:8f16:3564:eee6) (Ping timeout: 246 seconds) |
| 03:57:57 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 04:01:27 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds) |
| 04:02:53 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 04:04:50 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 268 seconds) |
| 04:29:46 | → | michalz joins (~michalz@185.246.207.193) |
| 04:30:37 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 04:32:24 | × | pwug quits (~pwug@user/pwug) (Quit: Leaving) |
| 04:36:36 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 268 seconds) |
| 04:38:39 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 272 seconds) |
| 04:41:08 | × | joeyadams quits (~joeyadams@2603:6010:5100:2ed:674f:8bcc:dd31:934b) (Quit: Leaving) |
| 04:47:50 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 04:53:23 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 264 seconds) |
| 04:58:17 | × | rosco quits (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 04:59:27 | × | michalz quits (~michalz@185.246.207.193) (Quit: ZNC 1.9.0 - https://znc.in) |
| 05:02:16 | → | michalz joins (~michalz@185.246.207.205) |
| 05:05:52 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 05:08:30 | → | nyc joins (~quassel@2603:7000:a106:2fb5::1f12) |
| 05:08:54 | × | nyc quits (~quassel@2603:7000:a106:2fb5::1f12) (Changing host) |
| 05:08:54 | → | nyc joins (~quassel@user/nyc) |
| 05:12:13 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 246 seconds) |
| 05:22:25 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 05:23:16 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 05:26:39 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 05:27:15 | → | dmj` joins (uid72307@id-72307.hampstead.irccloud.com) |
| 05:28:38 | → | euleritian joins (~euleritia@dynamic-176-002-074-154.176.2.pool.telefonica.de) |
| 05:31:12 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 255 seconds) |
| 05:32:23 | → | cfricke joins (~cfricke@user/cfricke) |
| 05:34:11 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 264 seconds) |
| 05:35:41 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 05:36:18 | × | califax quits (~califax@user/califx) (Ping timeout: 260 seconds) |
| 05:37:13 | → | califax joins (~califax@user/califx) |
| 05:37:48 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:42:16 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 05:43:36 | → | philopsos1 joins (~caecilius@user/philopsos) |
| 05:45:40 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 05:45:43 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 05:49:44 | → | acidjnk_new joins (~acidjnk@p200300d6e714dc520c8312600ef4c57c.dip0.t-ipconnect.de) |
| 05:50:05 | → | CiaoSen joins (~Jura@2a05:5800:2d2:8900:e6b9:7aff:fe80:3d03) |
| 05:51:14 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 256 seconds) |
| 06:01:33 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 06:06:29 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 240 seconds) |
| 06:16:39 | → | oneeyedalien joins (~oneeyedal@user/oneeyedalien) |
| 06:16:53 | → | danse-nr3 joins (~danse-nr3@151.57.152.233) |
| 06:20:26 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 06:21:44 | × | philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 268 seconds) |
| 06:25:43 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 246 seconds) |
| 06:27:16 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 06:33:18 | × | Square2 quits (~Square4@user/square) (Ping timeout: 255 seconds) |
| 06:38:14 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 06:39:19 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 06:42:06 | × | oneeyedalien quits (~oneeyedal@user/oneeyedalien) (Quit: Leaving) |
| 06:43:47 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 264 seconds) |
| 06:46:27 | × | kyborg2011_ quits (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 06:46:57 | × | bliminse quits (~bliminse@user/bliminse) (Quit: leaving) |
| 06:52:27 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 264 seconds) |
| 06:53:58 | → | xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 06:58:04 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 07:01:35 | × | euleritian quits (~euleritia@dynamic-176-002-074-154.176.2.pool.telefonica.de) (Ping timeout: 260 seconds) |
| 07:01:48 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 07:03:17 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 240 seconds) |
| 07:08:55 | → | rosco joins (rosco@gateway/vpn/airvpn/rosco) |
| 07:15:00 | → | bliminse joins (~bliminse@user/bliminse) |
| 07:16:52 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 07:22:04 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 246 seconds) |
| 07:22:40 | → | myme joins (~myme@2a01:799:d5c:5f00:33d4:3d73:88f6:3af4) |
| 07:22:52 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 07:24:09 | → | Midjak joins (~MarciZ@82.66.147.146) |
| 07:24:51 | × | jle` quits (~jle`@2603:8001:3b02:84d4:8e83:44df:afb0:80e1) (Ping timeout: 264 seconds) |
| 07:24:51 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:25:21 | → | jle` joins (~jle`@2603:8001:3b02:84d4:309b:a5ab:1320:adb2) |
| 07:27:06 | × | nyc quits (~quassel@user/nyc) (Ping timeout: 268 seconds) |
| 07:32:01 | × | rosco quits (rosco@gateway/vpn/airvpn/rosco) (Quit: Lost terminal) |
| 07:38:06 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 07:42:23 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 252 seconds) |
| 07:46:16 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 07:48:09 | × | CrunchyFlakes quits (~CrunchyFl@146.52.130.128) (Read error: Connection reset by peer) |
| 07:50:34 | → | CrunchyFlakes joins (~CrunchyFl@146.52.130.128) |
| 07:55:27 | × | lbseale quits (~quassel@user/ep1ctetus) (Ping timeout: 264 seconds) |
| 07:55:36 | → | nyc joins (~quassel@2603:7000:a106:2fb5::1f12) |
| 07:56:20 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 07:56:53 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 08:00:24 | × | Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep) |
| 08:01:17 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 240 seconds) |
| 08:03:54 | → | Midjak joins (~MarciZ@82.66.147.146) |
| 08:03:58 | → | lbseale joins (~quassel@user/ep1ctetus) |
| 08:09:09 | × | Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep) |
| 08:14:43 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 08:20:19 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 272 seconds) |
| 08:23:09 | → | Midjak joins (~MarciZ@82.66.147.146) |
| 08:24:27 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 268 seconds) |
| 08:25:32 | → | chele joins (~chele@user/chele) |
| 08:28:12 | × | Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep) |
| 08:29:13 | → | akegalj joins (~akegalj@95.168.118.12) |
| 08:34:31 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 08:36:39 | × | danse-nr3 quits (~danse-nr3@151.57.152.233) (Ping timeout: 256 seconds) |
| 08:38:41 | → | __monty__ joins (~toonn@user/toonn) |
| 08:40:29 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 268 seconds) |
| 08:40:44 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 08:52:48 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 08:55:55 | × | dcoutts__ quits (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 260 seconds) |
| 08:58:11 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 264 seconds) |
| 08:59:21 | → | danse-nr3 joins (~danse-nr3@151.57.152.233) |
| 09:00:50 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 09:10:49 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 09:11:39 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 09:11:43 | → | poscat0x04 joins (~poscat@user/poscat) |
| 09:13:51 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 09:14:59 | × | poscat quits (~poscat@user/poscat) (Ping timeout: 264 seconds) |
| 09:15:08 | → | poscat- joins (~poscat@user/poscat) |
| 09:15:18 | → | soverysour joins (~soverysou@86.122.85.40) |
| 09:15:18 | × | soverysour quits (~soverysou@86.122.85.40) (Changing host) |
| 09:15:18 | → | soverysour joins (~soverysou@user/soverysour) |
| 09:16:06 | × | gehmehgeh quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 09:16:41 | × | poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 272 seconds) |
| 09:18:22 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 09:19:03 | × | ft quits (~ft@p3e9bcb39.dip0.t-ipconnect.de) (Quit: leaving) |
| 09:20:23 | × | soverysour quits (~soverysou@user/soverysour) (Ping timeout: 264 seconds) |
| 09:22:51 | → | dcoutts__ joins (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) |
| 09:23:58 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 268 seconds) |
| 09:26:34 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:31:23 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:38:50 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 09:40:25 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 09:43:31 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 260 seconds) |
| 09:45:05 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 09:54:56 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 09:56:39 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:00:05 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Ping timeout: 240 seconds) |
| 10:00:49 | → | barthandelous01 joins (~calebbrze@216.158.140.68) |
| 10:01:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:05:58 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 10:06:15 | × | danse-nr3 quits (~danse-nr3@151.57.152.233) (Read error: Connection reset by peer) |
| 10:06:40 | → | danse-nr3 joins (~danse-nr3@151.43.196.110) |
| 10:07:35 | × | xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
| 10:10:31 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 10:18:33 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 10:20:03 | → | zmt01 joins (~zmt00@user/zmt00) |
| 10:21:03 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 256 seconds) |
| 10:21:10 | → | swamp_ joins (~zmt00@user/zmt00) |
| 10:24:56 | × | zmt01 quits (~zmt00@user/zmt00) (Ping timeout: 256 seconds) |
| 10:26:16 | × | xdminsy quits (~xdminsy@117.147.70.231) (Read error: Connection reset by peer) |
| 10:26:42 | → | xdminsy joins (~xdminsy@117.147.70.231) |
| 10:27:30 | → | zmt01 joins (~zmt00@user/zmt00) |
| 10:31:11 | × | swamp_ quits (~zmt00@user/zmt00) (Ping timeout: 268 seconds) |
| 10:39:57 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 10:44:26 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 10:44:47 | → | euleritian joins (~euleritia@dynamic-176-006-179-020.176.6.pool.telefonica.de) |
| 10:47:32 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Remote host closed the connection) |
| 10:47:41 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 10:53:10 | gehmehgeh | is now known as gmg |
| 10:56:03 | → | rosco joins (~rosco@175.136.155.137) |
| 10:57:03 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 10:59:17 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 272 seconds) |
| 11:04:45 | → | xff0x joins (~xff0x@ai068022.d.east.v6connect.net) |
| 11:05:04 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 11:08:52 | × | destituion quits (~destituio@2a02:2121:306:89fe:ede:e4a:e882:ff5) (Ping timeout: 246 seconds) |
| 11:09:22 | → | destituion joins (~destituio@85.221.111.174) |
| 11:10:00 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 11:20:09 | → | poxel joins (~lennart@user/poxel) |
| 11:23:30 | × | dmj` quits (uid72307@id-72307.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 11:29:55 | → | verde joins (~user@user/verde) |
| 11:30:54 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 11:36:57 | × | mxs quits (~mxs@user/mxs) (Quit: The Lounge - https://thelounge.chat) |
| 11:46:31 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 11:47:42 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Client Quit) |
| 12:10:25 | × | danse-nr3 quits (~danse-nr3@151.43.196.110) (Remote host closed the connection) |
| 12:10:42 | × | euleritian quits (~euleritia@dynamic-176-006-179-020.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 12:10:49 | → | danse-nr3 joins (~danse-nr3@151.43.196.110) |
| 12:11:48 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 12:13:18 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 12:14:06 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 12:14:48 | → | soverysour joins (~soverysou@86.122.85.40) |
| 12:14:48 | × | soverysour quits (~soverysou@86.122.85.40) (Changing host) |
| 12:14:48 | → | soverysour joins (~soverysou@user/soverysour) |
| 12:15:27 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 12:21:27 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 12:23:23 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 12:23:25 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 12:24:21 | × | verde quits (~user@user/verde) (Remote host closed the connection) |
| 12:24:49 | → | euleritian joins (~euleritia@dynamic-176-006-179-020.176.6.pool.telefonica.de) |
| 12:24:49 | × | danse-nr3 quits (~danse-nr3@151.43.196.110) (Ping timeout: 246 seconds) |
| 12:42:15 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 12:44:27 | → | califax joins (~califax@user/califx) |
| 12:44:39 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 12:46:47 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 264 seconds) |
| 12:46:51 | → | califax joins (~califax@user/califx) |
| 12:49:40 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 12:49:50 | × | gmg quits (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 12:52:05 | → | gmg joins (~user@user/gehmehgeh) |
| 12:52:30 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 12:55:21 | × | Digit quits (~user@user/digit) (Ping timeout: 255 seconds) |
| 13:01:24 | × | akegalj quits (~akegalj@95.168.118.12) (Read error: Connection reset by peer) |
| 13:07:35 | → | Digit joins (~user@user/digit) |
| 13:08:18 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:668b:8ad4:1fc2:fd6f) |
| 13:12:53 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 13:13:15 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Client Quit) |
| 13:18:14 | → | dmj` joins (uid72307@id-72307.hampstead.irccloud.com) |
| 13:25:27 | → | __monty__ joins (~toonn@user/toonn) |
| 13:28:29 | × | nyc quits (~quassel@2603:7000:a106:2fb5::1f12) (Ping timeout: 240 seconds) |
| 13:32:17 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 13:32:44 | → | Midjak joins (~MarciZ@82.66.147.146) |
| 13:34:20 | × | euleritian quits (~euleritia@dynamic-176-006-179-020.176.6.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 13:35:13 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 13:36:44 | → | cfricke joins (~cfricke@user/cfricke) |
| 13:36:51 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 13:37:24 | → | euleritian joins (~euleritia@dynamic-176-004-198-011.176.4.pool.telefonica.de) |
| 13:54:20 | → | akegalj joins (~akegalj@86.33.70.155) |
| 13:57:22 | → | nyc joins (~quassel@2603:7000:a106:2fb5::1f12) |
| 14:05:14 | → | danse-nr3 joins (~danse-nr3@151.43.194.82) |
| 14:06:42 | × | euleritian quits (~euleritia@dynamic-176-004-198-011.176.4.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 14:08:02 | → | euleritian joins (~euleritia@dynamic-176-001-214-220.176.1.pool.telefonica.de) |
| 14:13:48 | → | Digitteknohippie joins (~user@user/digit) |
| 14:15:07 | × | Digit quits (~user@user/digit) (Ping timeout: 260 seconds) |
| 14:18:43 | × | soverysour quits (~soverysou@user/soverysour) (Remote host closed the connection) |
| 14:18:55 | Digitteknohippie | is now known as Digit |
| 14:19:15 | → | soverysour joins (~soverysou@86.122.85.40) |
| 14:19:15 | × | soverysour quits (~soverysou@86.122.85.40) (Changing host) |
| 14:19:15 | → | soverysour joins (~soverysou@user/soverysour) |
| 14:21:04 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 14:25:46 | × | dcoutts__ quits (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 256 seconds) |
| 14:26:08 | × | nyc quits (~quassel@2603:7000:a106:2fb5::1f12) (Remote host closed the connection) |
| 14:35:48 | → | kyborg2011 joins (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 14:38:46 | × | cheater quits (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 14:40:18 | → | zzz joins (~yin@user/zero) |
| 14:40:45 | → | y-koj joins (~yk@2404:7a81:c840:5e00:c44:429d:83d8:df96) |
| 14:43:39 | <hadronized> | anyone had a look at Idris2? I saw somewhere that it can run without a GC?! |
| 14:50:06 | <EvanR> | they replaced the basic C runtime with semispace collector with chicken scheme, I think |
| 14:50:27 | <EvanR> | I wouldn't bet on idris2 being the pathway to extreme performance |
| 14:51:11 | <EvanR> | it's really about the dependent types |
| 14:51:17 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 240 seconds) |
| 14:52:37 | <hadronized> | I’m not sure why people are so hyped about DT |
| 14:55:48 | × | y-koj quits (~yk@2404:7a81:c840:5e00:c44:429d:83d8:df96) (Quit: WeeChat 4.2.1) |
| 14:56:04 | → | y-koj joins (~yk@2404:7a81:c840:5e00:c44:429d:83d8:df96) |
| 14:58:24 | → | __monty__ joins (~toonn@user/toonn) |
| 15:00:32 | <mauke> | good DPS, cloaked by default, always good for a comeback |
| 15:02:22 | × | kimiamania quits (~65804703@user/kimiamania) (Quit: Ping timeout (120 seconds)) |
| 15:02:46 | → | kimiamania joins (~65804703@user/kimiamania) |
| 15:05:07 | × | euleritian quits (~euleritia@dynamic-176-001-214-220.176.1.pool.telefonica.de) (Ping timeout: 246 seconds) |
| 15:06:12 | → | euleritian joins (~euleritia@dynamic-176-001-135-067.176.1.pool.telefonica.de) |
| 15:08:59 | × | danse-nr3 quits (~danse-nr3@151.43.194.82) (Ping timeout: 264 seconds) |
| 15:12:39 | → | someone235 joins (uid419897@id-419897.ilkley.irccloud.com) |
| 15:18:41 | × | kyborg2011 quits (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Read error: Connection reset by peer) |
| 15:19:09 | → | kyborg2011 joins (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 15:23:20 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 15:23:33 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 15:26:15 | × | euleritian quits (~euleritia@dynamic-176-001-135-067.176.1.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 15:26:36 | × | kimiamania quits (~65804703@user/kimiamania) (Quit: Ping timeout (120 seconds)) |
| 15:27:05 | → | kimiamania joins (~65804703@user/kimiamania) |
| 15:29:11 | → | euleritian joins (~euleritia@dynamic-176-006-011-233.176.6.pool.telefonica.de) |
| 15:30:49 | → | dcoutts__ joins (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) |
| 15:37:27 | × | euphores quits (~SASL_euph@user/euphores) (Ping timeout: 264 seconds) |
| 15:43:21 | × | Midjak quits (~MarciZ@82.66.147.146) (Quit: Leaving) |
| 15:44:17 | × | dcoutts__ quits (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 272 seconds) |
| 15:44:19 | → | Midjak joins (~MarciZ@82.66.147.146) |
| 15:48:23 | × | Athas quits (athas@sigkill.dk) (Quit: ZNC 1.8.2 - https://znc.in) |
| 15:48:41 | → | Athas joins (athas@sigkill.dk) |
| 15:54:10 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 15:55:11 | × | euleritian quits (~euleritia@dynamic-176-006-011-233.176.6.pool.telefonica.de) (Ping timeout: 264 seconds) |
| 15:56:22 | × | cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 15:59:07 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 16:03:34 | → | danse-nr3 joins (~danse-nr3@151.43.194.82) |
| 16:03:41 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:668b:8ad4:1fc2:fd6f) (Remote host closed the connection) |
| 16:03:54 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:c91:a997:4d69:689b) |
| 16:07:27 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 16:08:41 | × | akegalj quits (~akegalj@86.33.70.155) (Quit: leaving) |
| 16:08:47 | × | Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 16:11:16 | × | zzz quits (~yin@user/zero) (Ping timeout: 268 seconds) |
| 16:12:49 | × | CiaoSen quits (~Jura@2a05:5800:2d2:8900:e6b9:7aff:fe80:3d03) (Ping timeout: 268 seconds) |
| 16:13:41 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 240 seconds) |
| 16:17:54 | → | falafel joins (~falafel@2a0c:5a87:3103:ec01::62b8) |
| 16:20:33 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 16:21:42 | → | euleritian joins (~euleritia@77.22.252.56) |
| 16:26:15 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 16:35:55 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:c91:a997:4d69:689b) (Remote host closed the connection) |
| 16:38:22 | → | JamesMowery1 joins (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) |
| 16:39:44 | × | JamesMowery quits (~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Ping timeout: 252 seconds) |
| 16:39:45 | JamesMowery1 | is now known as JamesMowery |
| 16:41:35 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 16:41:45 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 16:41:46 | × | soverysour quits (~soverysou@user/soverysour) (Ping timeout: 256 seconds) |
| 16:42:43 | → | soverysour joins (~soverysou@86.122.85.40) |
| 16:42:43 | × | soverysour quits (~soverysou@86.122.85.40) (Changing host) |
| 16:42:43 | → | soverysour joins (~soverysou@user/soverysour) |
| 16:45:10 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 256 seconds) |
| 16:46:36 | → | euleritian joins (~euleritia@dynamic-176-000-211-014.176.0.pool.telefonica.de) |
| 16:50:17 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 16:50:30 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 16:52:11 | × | ames quits (~amelia@offtopia/offtopian/amelia) (Quit: Bye!) |
| 16:52:20 | → | ames joins (~amelia@offtopia/offtopian/amelia) |
| 16:55:22 | × | causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.3.1) |
| 16:56:07 | → | euphores joins (~SASL_euph@user/euphores) |
| 16:56:32 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 16:58:03 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 16:58:45 | × | euleritian quits (~euleritia@dynamic-176-000-211-014.176.0.pool.telefonica.de) (Ping timeout: 268 seconds) |
| 17:00:21 | → | euleritian joins (~euleritia@dynamic-176-007-158-220.176.7.pool.telefonica.de) |
| 17:00:58 | × | falafel quits (~falafel@2a0c:5a87:3103:ec01::62b8) (Ping timeout: 246 seconds) |
| 17:08:34 | × | euleritian quits (~euleritia@dynamic-176-007-158-220.176.7.pool.telefonica.de) (Read error: Connection reset by peer) |
| 17:08:56 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 17:09:03 | → | euleritian joins (~euleritia@77.22.252.56) |
| 17:13:17 | × | euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 240 seconds) |
| 17:15:45 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 17:18:07 | → | Square joins (~Square@user/square) |
| 17:19:10 | × | TactfulCitrus quits (al@gateway/vpn/protonvpn/tactfulcitrus) (Ping timeout: 256 seconds) |
| 17:26:54 | → | madhavanmiui joins (~madhavanm@2409:40f4:10fe:af12:8000::) |
| 17:29:41 | × | rosco quits (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 17:30:18 | × | notzmv quits (~daniel@user/notzmv) (Ping timeout: 255 seconds) |
| 17:38:58 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 17:41:18 | × | danse-nr3 quits (~danse-nr3@151.43.194.82) (Ping timeout: 268 seconds) |
| 17:41:40 | × | someone235 quits (uid419897@id-419897.ilkley.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:45:07 | → | notzmv joins (~daniel@user/notzmv) |
| 17:46:35 | → | noumenon joins (~noumenon@113.51-175-156.customer.lyse.net) |
| 17:48:54 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 17:49:41 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 17:51:11 | → | lxsameer joins (~lxsameer@Serene/lxsameer) |
| 17:53:20 | → | fun-safe-math joins (~fun-safe-@24.21.106.247) |
| 17:56:09 | × | fun-safe-math quits (~fun-safe-@24.21.106.247) (Client Quit) |
| 17:56:19 | × | soverysour quits (~soverysou@user/soverysour) (Ping timeout: 260 seconds) |
| 17:56:29 | → | fun-safe-math joins (~fun-safe-@24.21.106.247) |
| 17:56:29 | × | fun-safe-math quits (~fun-safe-@24.21.106.247) (Client Quit) |
| 17:58:09 | → | fun-safe-math joins (~fun-safe-@24.21.106.247) |
| 17:58:25 | → | ft joins (~ft@p3e9bcb39.dip0.t-ipconnect.de) |
| 17:58:47 | × | destituion quits (~destituio@85.221.111.174) (Ping timeout: 264 seconds) |
| 17:59:42 | → | destituion joins (~destituio@85.221.111.174) |
| 18:00:09 | → | ystael joins (~ystael@user/ystael) |
| 18:00:12 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 18:01:39 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 18:01:48 | × | fun-safe-math quits (~fun-safe-@24.21.106.247) (Client Quit) |
| 18:03:28 | → | fun-safe-math joins (~fun-safe-@24.21.106.247) |
| 18:03:46 | → | euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 18:07:47 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 264 seconds) |
| 18:07:54 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 18:09:15 | Lord_of_Life_ | is now known as Lord_of_Life |
| 18:11:57 | × | madhavanmiui quits (~madhavanm@2409:40f4:10fe:af12:8000::) (Quit: Quit) |
| 18:12:29 | × | destituion quits (~destituio@85.221.111.174) (Ping timeout: 272 seconds) |
| 18:13:19 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:15:20 | → | soverysour joins (~soverysou@86.122.85.40) |
| 18:15:20 | × | soverysour quits (~soverysou@86.122.85.40) (Changing host) |
| 18:15:20 | → | soverysour joins (~soverysou@user/soverysour) |
| 18:17:59 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 18:18:59 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 18:19:41 | × | soverysour quits (~soverysou@user/soverysour) (Ping timeout: 240 seconds) |
| 18:21:05 | <iqubic> | I like Idris2. |
| 18:21:41 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:26:23 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 18:26:25 | → | andrei_n joins (~andrei_n@user/andrei-n:62396) |
| 18:29:45 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:29:59 | → | Digitteknohippie joins (~user@user/digit) |
| 18:31:16 | × | Digit quits (~user@user/digit) (Ping timeout: 246 seconds) |
| 18:34:35 | → | zzz joins (~yin@user/zero) |
| 18:35:02 | Digitteknohippie | is now known as Digit |
| 18:38:28 | → | destituion joins (~destituio@2a02:2121:306:89fe:b849:537f:4eb9:4445) |
| 18:39:06 | → | acidjnk_new3 joins (~acidjnk@p200300d6e714dc52cdce3fd1d2726986.dip0.t-ipconnect.de) |
| 18:40:59 | → | moolc joins (~malc@109-252-143-253.dynamic.spd-mgts.ru) |
| 18:41:23 | ← | moolc parts (~malc@109-252-143-253.dynamic.spd-mgts.ru) (ERC 5.6 (IRC client for GNU Emacs 30.0.50)) |
| 18:42:41 | → | Digitteknohippie joins (~user@user/digit) |
| 18:43:17 | × | acidjnk_new quits (~acidjnk@p200300d6e714dc520c8312600ef4c57c.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 18:44:31 | × | Digit quits (~user@user/digit) (Ping timeout: 268 seconds) |
| 18:48:23 | → | simendsjo joins (~user@84.209.170.3) |
| 18:55:57 | → | crns joins (~crns@user/crns) |
| 18:56:28 | × | crns quits (~crns@user/crns) (Client Quit) |
| 19:07:13 | × | andrei_n quits (~andrei_n@user/andrei-n:62396) (Quit: Leaving) |
| 19:11:38 | → | dcoutts__ joins (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) |
| 19:21:28 | Digitteknohippie | is now known as Digit |
| 19:22:30 | → | Guest|78 joins (~Guest|78@100.4.128.234) |
| 19:22:34 | × | Guest|78 quits (~Guest|78@100.4.128.234) (Client Quit) |
| 19:24:02 | → | soverysour joins (~soverysou@user/soverysour) |
| 19:28:35 | × | soverysour quits (~soverysou@user/soverysour) (Ping timeout: 252 seconds) |
| 19:28:36 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 19:29:23 | <EvanR> | hadronized, dependent types let you express logical propositions |
| 19:32:08 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 19:33:31 | <EvanR> | when you have a value of some type in haskell, you tend to know a lot of stuff. With dependent types you can know even more stuff. There are practical issues but you only were wondering about the positives xD |
| 19:34:27 | × | dcoutts__ quits (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) (Ping timeout: 264 seconds) |
| 19:37:17 | × | Square quits (~Square@user/square) (Ping timeout: 240 seconds) |
| 19:48:03 | <monochrom> | Some people want dependent types for what can also be done by Liquid Haskell and refinement types, e.g., the domain is integers between 100 and 200. |
| 19:50:25 | <monochrom> | Some other people want dependent types for how Idris uses it: fine-grained effect/capability types, e.g., more fine-grained than our IO, so your type says a subset of {console, files, IORef, ...}. |
| 19:51:25 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 19:52:22 | <monochrom> | Some other people want dependent types for just row polymorphism i.e. a record system that doesn't suck. :) |
| 19:53:47 | <EvanR> | that's a roundabout way to get that, and not clear it wouldn't suck! |
| 19:55:19 | <monochrom> | In every use case, dependent typing is an overkill. But history and politics taught us that, when multiple groups who will have conflicting stakes eventually but right now they have a more pressing common foe, they will be very hyped up about joining forces. |
| 19:58:07 | <c_wraith> | I just want pi types so I can abstract over values at the type level |
| 19:58:33 | <monochrom> | Yeah the general idea is that if you have a Gödel-complete proof language, then you can define any powerful programming language you want. OK that's a hyperbole but think about it. :) |
| 20:00:10 | → | mxs9 joins (~mxs@user/mxs) |
| 20:01:44 | <monochrom> | In my own notes when I study math, there are actually a few instances when I use Pi types because it clarifies and directly express what the math text means to say but too afraid to bring up infinite cartesian products... |
| 20:03:41 | <monochrom> | basically scenerio like choice functions where the math text says "f : X -> big union of Y_1, Y_2 ... , with the contraint that f(x) must be in Y_x". OK that's a type Pi. |
| 20:03:46 | <monochrom> | err Pi type |
| 20:04:14 | <monochrom> | Speaking of which, please remind me on June 28 to celebrate tau day! |
| 20:07:38 | <c_wraith> | so are Tau types twice as good as Pi types? |
| 20:08:16 | <monochrom> | :) |
| 20:09:00 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 20:09:11 | <monochrom> | Some kind of Fubini's theorem ought to say that Tau_x,y = Pi_x Pi_y :) |
| 20:15:59 | → | danse-nr3 joins (~danse-nr3@151.35.139.58) |
| 20:20:31 | → | cheater joins (~Username@user/cheater) |
| 20:31:41 | × | Luj quits (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Ping timeout: 240 seconds) |
| 20:32:23 | <EvanR> | it's funny because type theory seems to say more specifically what you want, but at the same time, means nothing because it's basically a theory of syntax only |
| 20:35:34 | <danse-nr3> | "a theory of syntax"? |
| 20:39:45 | <lxsameer> | hey folks, have you ever used tasty-autocollect or tasty-discover in a nix based build environment |
| 20:40:02 | <monochrom> | I thought through this question a long time ago, I concluded that one person's semantics is another person's syntax. But I understand that it is not obvious to everyone. |
| 20:41:01 | → | swamp_ joins (~zmt00@user/zmt00) |
| 20:41:02 | <monochrom> | Part of it being that it is customary to not talk about the syntax of one's meta-logic. But it is still there. |
| 20:44:19 | × | zmt01 quits (~zmt00@user/zmt00) (Ping timeout: 260 seconds) |
| 20:48:53 | × | zzz quits (~yin@user/zero) (Ping timeout: 252 seconds) |
| 20:49:47 | × | lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds) |
| 20:50:36 | × | barthandelous01 quits (~calebbrze@216.158.140.68) (Quit: WeeChat 4.3.2) |
| 21:05:03 | → | dcoutts__ joins (~duncan@oxfd-27-b2-v4wan-164228-cust163.vm42.cable.virginm.net) |
| 21:05:17 | → | Square joins (~Square@user/square) |
| 21:15:22 | → | pavonia joins (~user@user/siracusa) |
| 21:17:09 | × | michalz quits (~michalz@185.246.207.205) (Quit: ZNC 1.9.0 - https://znc.in) |
| 21:21:57 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 21:23:49 | → | zzz joins (~yin@user/zero) |
| 21:26:05 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:26:35 | × | EvanR quits (~EvanR@user/evanr) (Remote host closed the connection) |
| 21:26:55 | → | EvanR joins (~EvanR@user/evanr) |
| 21:29:40 | → | falafel joins (~falafel@2a0c:5a87:3103:ec01::62b8) |
| 21:30:07 | → | barthandelous01 joins (barth@triton.blinkenshell.org) |
| 21:36:25 | × | manwithluck quits (manwithluc@gateway/vpn/protonvpn/manwithluck) (Ping timeout: 246 seconds) |
| 21:41:32 | → | AlexNoo_ joins (~AlexNoo@178.34.162.224) |
| 21:42:12 | × | poxel quits (~lennart@user/poxel) (Quit: WeeChat 4.3.2) |
| 21:43:20 | × | AlexZenon quits (~alzenon@178.34.163.174) (Ping timeout: 252 seconds) |
| 21:45:12 | × | AlexNoo quits (~AlexNoo@178.34.163.174) (Ping timeout: 268 seconds) |
| 21:47:53 | → | AlexZenon joins (~alzenon@178.34.162.224) |
| 21:51:35 | × | hc quits (~hc@mail.hce.li) (Remote host closed the connection) |
| 22:17:55 | × | Midjak quits (~MarciZ@82.66.147.146) (Quit: Leaving) |
| 22:22:46 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:30:03 | <dolio> | I'm not particularly convinced that you're showing that 'dependent types are overkill' when you list multiple features that people want to use dependent types for, and have to be separately grafted onto other languages. |
| 22:31:09 | <geekosaur> | that you can use feature X to do thing Y doesn't mean it's the best way to do thing Y |
| 22:31:59 | <monochrom> | Good points, both of you. :) |
| 22:32:01 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 22:32:07 | <dolio> | Well, I didn't make the examples. |
| 22:34:17 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:35:40 | × | Eoco quits (~ian@128.101.131.218) (Quit: WeeChat 4.1.1) |
| 22:41:33 | × | acidjnk_new3 quits (~acidjnk@p200300d6e714dc52cdce3fd1d2726986.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 22:43:04 | × | kyborg2011 quits (~kyborg201@host-176-36-215-61.b024.la.net.ua) (Read error: Connection reset by peer) |
| 22:43:34 | → | kyborg2011 joins (~kyborg201@host-176-36-215-61.b024.la.net.ua) |
| 22:44:21 | × | danse-nr3 quits (~danse-nr3@151.35.139.58) (Read error: Connection reset by peer) |
| 22:45:24 | → | danse-nr3 joins (~danse-nr3@151.37.122.33) |
| 22:46:47 | × | euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds) |
| 22:48:57 | → | euleritian joins (~euleritia@dynamic-176-001-131-134.176.1.pool.telefonica.de) |
| 22:53:57 | × | ystael quits (~ystael@user/ystael) (Ping timeout: 268 seconds) |
| 22:54:15 | × | glguy quits (g@libera/staff/glguy) (Quit: Quit) |
| 22:56:40 | → | glguy joins (g@libera/staff/glguy) |
| 22:57:50 | → | Square2 joins (~Square4@user/square) |
| 22:58:53 | × | mud quits (~mud@user/kadoban) (Ping timeout: 268 seconds) |
| 23:01:03 | × | Square quits (~Square@user/square) (Ping timeout: 255 seconds) |
| 23:02:02 | × | glguy quits (g@libera/staff/glguy) (Remote host closed the connection) |
| 23:03:16 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 23:03:30 | → | glguy joins (g@libera/staff/glguy) |
| 23:03:35 | × | danse-nr3 quits (~danse-nr3@151.37.122.33) (Ping timeout: 264 seconds) |
| 23:03:38 | → | danza joins (~francesco@151.37.122.33) |
| 23:04:52 | → | mud joins (~mud@user/kadoban) |
| 23:08:09 | → | talismanick joins (~user@2601:644:937c:ed10::ae5) |
| 23:08:45 | × | danza quits (~francesco@151.37.122.33) (Ping timeout: 268 seconds) |
| 23:19:39 | × | talismanick quits (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection) |
| 23:24:04 | → | talismanick joins (~user@2601:644:937c:ed10::ae5) |
| 23:25:04 | → | danza joins (~francesco@151.37.122.33) |
| 23:25:24 | <talismanick> | Is suppressing the "type inference for inner bindings fragile" warning with MonoLocalBinds generally safe? |
| 23:26:08 | <talismanick> | or, more precisely, intent- and correctness-preserving |
| 23:38:16 | → | joeyadams joins (~joeyadams@2603:6010:5100:2ed:be5c:bfac:9926:c006) |
| 23:52:14 | × | johnw quits (~johnw@69.62.242.138) (Ping timeout: 268 seconds) |
| 23:52:22 | → | johnw_ joins (~johnw@69.62.242.138) |
| 23:56:29 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 240 seconds) |
| 23:59:32 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
All times are in UTC on 2024-06-19.