2025/01/24

2025-01-24 00:01:19 +0100j1n37(~j1n37@user/j1n37) (Ping timeout: 264 seconds)
2025-01-24 00:01:22 +0100weary-traveler(~user@user/user363627) user363627
2025-01-24 00:03:11 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-24 00:04:29 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 00:04:43 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-01-24 00:06:56 +0100Guest59(~Guest59@2a09:bac3:bc20:1923::281:51)
2025-01-24 00:09:09 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 248 seconds)
2025-01-24 00:09:12 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Ping timeout: 264 seconds)
2025-01-24 00:10:03 +0100chexum(~quassel@gateway/tor-sasl/chexum) chexum
2025-01-24 00:10:24 +0100chiselfuse(~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds)
2025-01-24 00:12:24 +0100chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-01-24 00:14:25 +0100Guest59(~Guest59@2a09:bac3:bc20:1923::281:51) (Quit: Client closed)
2025-01-24 00:15:54 +0100xff0x(~xff0x@2405:6580:b080:900:7b70:7132:4b2b:5865) (Ping timeout: 260 seconds)
2025-01-24 00:16:20 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2025-01-24 00:17:54 +0100j1n37-(~j1n37@user/j1n37) j1n37
2025-01-24 00:18:45 +0100j1n37(~j1n37@user/j1n37) (Ping timeout: 248 seconds)
2025-01-24 00:20:16 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 00:20:18 +0100ColinRobinsonJuanDaugherty
2025-01-24 00:21:06 +0100Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no) (Ping timeout: 276 seconds)
2025-01-24 00:21:51 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 00:22:26 +0100Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no) Miroboru
2025-01-24 00:25:07 +0100Everything(~Everythin@195.138.86.118) (Quit: Lost terminal)
2025-01-24 00:25:17 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 00:25:57 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 246 seconds)
2025-01-24 00:26:24 +0100j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-01-24 00:27:06 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-01-24 00:34:38 +0100madjidnrl(~madjidnrl@129.45.36.94)
2025-01-24 00:35:29 +0100madjidnrl(~madjidnrl@129.45.36.94) (Client Quit)
2025-01-24 00:36:04 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 00:36:09 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 00:37:02 +0100j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-01-24 00:38:48 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-01-24 00:38:56 +0100xff0x(~xff0x@2405:6580:b080:900:7b70:7132:4b2b:5865)
2025-01-24 00:39:35 +0100jle`(~jle`@2603:8001:3b02:84d4::a0b) (Ping timeout: 252 seconds)
2025-01-24 00:40:23 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 245 seconds)
2025-01-24 00:40:27 +0100jle`(~jle`@2603:8001:3b02:84d4:467d:3e5f:31ca:9a0a) jle`
2025-01-24 00:41:15 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds)
2025-01-24 00:41:31 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 00:43:12 +0100JuanDaughertyColinRobinson
2025-01-24 00:46:56 +0100j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-01-24 00:47:09 +0100j1n37-(~j1n37@user/j1n37) j1n37
2025-01-24 00:51:51 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 00:53:32 +0100j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-01-24 00:54:28 +0100xdminsy(~xdminsy@117.147.71.143) (Read error: Connection reset by peer)
2025-01-24 00:55:00 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-01-24 00:55:21 +0100xdminsy(~xdminsy@117.147.71.143) xdminsy
2025-01-24 00:59:24 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 01:01:48 +0100j1n37(~j1n37@user/j1n37) (Ping timeout: 272 seconds)
2025-01-24 01:07:54 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 01:10:21 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 01:11:15 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 01:12:14 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-24 01:15:10 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 01:15:46 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 248 seconds)
2025-01-24 01:21:23 +0100Guest26(~Guest26@81-228-133-81-no600.tbcn.telia.com) (Quit: Client closed)
2025-01-24 01:26:08 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 01:31:09 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 260 seconds)
2025-01-24 01:31:21 +0100weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-01-24 01:36:16 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-01-24 01:37:57 +0100weary-traveler(~user@user/user363627) user363627
2025-01-24 01:41:58 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 01:42:02 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 01:44:51 +0100LainExperiments(~LainExper@user/LainExperiments) (Quit: Client closed)
2025-01-24 01:45:13 +0100acidjnk(~acidjnk@p200300d6e7283f96b914b0b581af9338.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2025-01-24 01:47:05 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 265 seconds)
2025-01-24 01:52:18 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-24 01:52:37 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 01:52:44 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-24 01:53:01 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 01:53:05 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-24 01:53:22 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 01:53:46 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-24 01:54:04 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 01:55:48 +0100xff0x(~xff0x@2405:6580:b080:900:7b70:7132:4b2b:5865) (Ping timeout: 265 seconds)
2025-01-24 01:57:44 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 01:58:07 +0100_0xa(~user@95.179.128.10)
2025-01-24 01:58:07 +0100_0xa(~user@95.179.128.10) (Changing host)
2025-01-24 01:58:07 +0100_0xa(~user@user/0xa/x-3134607) _0xa
2025-01-24 01:58:17 +0100jmtd(jon@dow.land) jmtd
2025-01-24 01:58:24 +0100deriamis_(nobody@2600:3c0a::f03c:95ff:fee8:f335) deriamis
2025-01-24 01:58:26 +0100xelxebar_(~xelxebar@wilsonb.com) xelxebar
2025-01-24 01:58:30 +0100biberu\(~biberu@user/biberu) biberu
2025-01-24 01:59:39 +0100Arsen_(arsen@gentoo/developer/managarm.dev.Arsen) Arsen
2025-01-24 02:00:11 +0100joeyh(~joeyh@kitenet.net) joeyh
2025-01-24 02:00:24 +0100codedmart_(~codedmart@li335-49.members.linode.com)
2025-01-24 02:00:40 +0100nefercheprure(tma@twin.jikos.cz) TMA
2025-01-24 02:01:00 +0100sweater2(~sweater@206.81.18.26) sweater
2025-01-24 02:01:01 +0100dfordivam1(~dfordivam@160.16.87.223.v6.sakura.ne.jp) dfordivam
2025-01-24 02:01:56 +0100notzmv(~umar@user/notzmv) (Remote host closed the connection)
2025-01-24 02:02:00 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 02:03:14 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 272 seconds)
2025-01-24 02:03:38 +0100remsen(ianremsen@tilde.team) remsense
2025-01-24 02:04:05 +0100xnbya(~xnbya@2a01:4f8:c17:cbdd::1)
2025-01-24 02:04:16 +0100markasoftware_(~quassel@2604:180:f2::217) markasoftware
2025-01-24 02:04:27 +0100xnbya2(~xnbya@2a01:4f8:c17:cbdd::1) (Quit: No Ping reply in 180 seconds.)
2025-01-24 02:04:28 +0100biberu(~biberu@user/biberu) (Quit: ZNC - https://znc.in)
2025-01-24 02:04:28 +0100Jon(jon@dow.land) (Quit: ZNC - http://znc.in)
2025-01-24 02:04:28 +0100deriamis(nobody@2600:3c0a::f03c:95ff:fee8:f335) (Quit: ZNC - https://znc.in)
2025-01-24 02:04:28 +0100_0xa_(~user@2001:19f0:5001:2ba8:5400:1ff:feda:88fc) (Quit: ZNC 1.7.5+deb4 - https://znc.in)
2025-01-24 02:04:28 +0100xelxebar(~xelxebar@wilsonb.com) (Quit: ZNC 1.7.2+deb3 - https://znc.in)
2025-01-24 02:04:28 +0100remmie(ianremsen@tilde.team) (Quit: ZNC 1.8.1 - https://znc.in)
2025-01-24 02:04:28 +0100codedmart(codedmart@2600:3c01::f03c:92ff:fefe:8511) (Quit: ZNC 1.7.5+deb4 - https://znc.in)
2025-01-24 02:04:28 +0100jmtdJon
2025-01-24 02:04:28 +0100Arsen(arsen@gentoo/developer/managarm.dev.Arsen) (Quit: No Ping reply in 180 seconds.)
2025-01-24 02:04:28 +0100joeyh_(~joeyh@kitenet.net) (Quit: ZNC 1.9.1+deb1 - https://znc.in)
2025-01-24 02:04:28 +0100markasoftware(~quassel@107.161.26.124) (Quit: No Ping reply in 180 seconds.)
2025-01-24 02:04:28 +0100dfordvm(~dfordivam@160.16.87.223.v6.sakura.ne.jp) (Remote host closed the connection)
2025-01-24 02:04:28 +0100dsrt^(~dsrt@108.192.66.114) (Remote host closed the connection)
2025-01-24 02:04:28 +0100sweater1(~sweater@206.81.18.26) (Remote host closed the connection)
2025-01-24 02:04:30 +0100biberu\biberu
2025-01-24 02:04:34 +0100remsenremmie
2025-01-24 02:04:43 +0100dsrt^(~dsrt@108.192.66.114)
2025-01-24 02:06:08 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 02:07:04 +0100HappyNewYear2025(~newyear@2.219.56.221) (Ping timeout: 244 seconds)
2025-01-24 02:07:06 +0100LainExperiments(~LainExper@user/LainExperiments) LainExperiments
2025-01-24 02:09:07 +0100TMA(tma@twin.jikos.cz) (Ping timeout: 264 seconds)
2025-01-24 02:09:16 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-01-24 02:13:31 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 02:13:43 +0100hawer(~newyear@2.219.56.221)
2025-01-24 02:14:37 +0100ColinRobinson(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-01-24 02:16:35 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 265 seconds)
2025-01-24 02:18:14 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 02:18:41 +0100LainExperiments(~LainExper@user/LainExperiments) (Quit: Client closed)
2025-01-24 02:21:44 +0100sprotte24(~sprotte24@p200300d16f0615004cac1667a189cb83.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2025-01-24 02:21:52 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-01-24 02:26:34 +0100otto_s(~user@p5de2f4cd.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2025-01-24 02:28:11 +0100otto_s(~user@p5de2f982.dip0.t-ipconnect.de)
2025-01-24 02:29:19 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 02:29:43 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-24 02:30:33 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 02:31:49 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-01-24 02:33:59 +0100Midjak(~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep)
2025-01-24 02:36:11 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 02:41:19 +0100haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection)
2025-01-24 02:42:11 +0100haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) hackager
2025-01-24 02:42:11 +0100ChanServ+v haskellbridge
2025-01-24 02:45:22 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2025-01-24 02:47:22 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 02:48:02 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-01-24 02:48:14 +0100LainExperiments(~LainExper@user/LainExperiments) LainExperiments
2025-01-24 02:50:27 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-01-24 02:50:30 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-01-24 02:50:45 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 02:54:49 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 244 seconds)
2025-01-24 02:55:55 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 02:56:26 +0100LainExperiments(~LainExper@user/LainExperiments) (Quit: Client closed)
2025-01-24 03:05:31 +0100_0xa_(~user@2001:19f0:5001:2ba8:5400:1ff:feda:88fc)
2025-01-24 03:05:54 +0100_0xa(~user@user/0xa/x-3134607) (Ping timeout: 252 seconds)
2025-01-24 03:06:56 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 03:07:14 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 03:08:26 +0100LainExperiments(~LainExper@user/LainExperiments) LainExperiments
2025-01-24 03:11:31 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 264 seconds)
2025-01-24 03:12:08 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 03:13:14 +0100hueso(~root@user/hueso) (Ping timeout: 252 seconds)
2025-01-24 03:13:43 +0100hueso(~root@user/hueso) hueso
2025-01-24 03:15:02 +0100agent314(~quassel@static-198-54-131-122.cust.tzulo.com) agent314
2025-01-24 03:15:02 +0100agent314(~quassel@static-198-54-131-122.cust.tzulo.com) (Client Quit)
2025-01-24 03:22:59 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 03:27:54 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 03:34:54 +0100weary-traveler(~user@user/user363627) user363627
2025-01-24 03:38:44 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 03:40:10 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 03:40:18 +0100johnjaye(~pi@syn-035-146-235-019.res.spectrum.com) johnjaye
2025-01-24 03:43:55 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 03:44:24 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 03:49:04 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 03:55:14 +0100ft(~ft@p3e9bcab6.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-01-24 03:57:06 +0100ft(~ft@p508db1ba.dip0.t-ipconnect.de) ft
2025-01-24 03:57:13 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 03:58:47 +0100hgolden_(~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) hgolden
2025-01-24 04:02:14 +0100hgolden(~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Ping timeout: 260 seconds)
2025-01-24 04:08:53 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 04:09:27 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 04:13:55 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 04:14:05 +0100user363627(~user@user/user363627) user363627
2025-01-24 04:16:57 +0100heavy_cloud(~heavy_clo@2603:7081:1600:6425:c8b5:8fc6:d959:2025)
2025-01-24 04:17:31 +0100weary-traveler(~user@user/user363627) (Ping timeout: 264 seconds)
2025-01-24 04:22:04 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 260 seconds)
2025-01-24 04:22:43 +0100heavy_cloud(~heavy_clo@2603:7081:1600:6425:c8b5:8fc6:d959:2025) (Quit: Client closed)
2025-01-24 04:24:08 +0100LainExperiments(~LainExper@user/LainExperiments) (Quit: Client closed)
2025-01-24 04:24:40 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 04:30:15 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 04:33:38 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 248 seconds)
2025-01-24 04:34:29 +0100xdminsy(~xdminsy@117.147.71.143) (Read error: Connection reset by peer)
2025-01-24 04:34:38 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 04:35:25 +0100xdminsy(~xdminsy@117.147.71.143) xdminsy
2025-01-24 04:40:31 +0100Sgeo_(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-01-24 04:42:35 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2025-01-24 04:45:05 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 04:50:02 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 04:55:28 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 05:00:07 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 264 seconds)
2025-01-24 05:00:53 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 05:06:07 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 05:12:30 +0100weary-traveler(~user@user/user363627) user363627
2025-01-24 05:16:26 +0100user363627(~user@user/user363627) (Ping timeout: 252 seconds)
2025-01-24 05:16:40 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 05:19:20 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 05:23:24 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 05:23:27 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 246 seconds)
2025-01-24 05:27:43 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 05:32:03 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 245 seconds)
2025-01-24 05:34:43 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 05:39:33 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 245 seconds)
2025-01-24 05:46:19 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 264 seconds)
2025-01-24 05:50:03 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 05:54:55 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 05:54:57 +0100OftenFaded(~OftenFade@user/tisktisk) (Ping timeout: 246 seconds)
2025-01-24 05:57:14 +0100OftenFaded(~OftenFade@user/tisktisk) OftenFaded
2025-01-24 06:05:51 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 06:08:24 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 06:10:04 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 06:10:42 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 06:12:43 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 264 seconds)
2025-01-24 06:14:11 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
2025-01-24 06:14:22 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-24 06:21:39 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 06:22:41 +0100michalz(~michalz@185.246.207.215)
2025-01-24 06:23:25 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan
2025-01-24 06:25:59 +0100michalz_(~michalz@185.246.207.203)
2025-01-24 06:27:07 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 06:27:43 +0100michalz(~michalz@185.246.207.215) (Ping timeout: 264 seconds)
2025-01-24 06:37:25 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 06:42:43 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 06:51:04 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 06:52:44 +0100hgolden_(~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Remote host closed the connection)
2025-01-24 06:56:50 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 06:57:37 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 07:01:02 +0100hgolden(~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) hgolden
2025-01-24 07:01:18 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 07:04:02 +0100Axma72592(~Axman6@user/axman6) Axman6
2025-01-24 07:04:37 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 07:06:11 +0100Axman6(~Axman6@user/axman6) (Ping timeout: 240 seconds)
2025-01-24 07:09:06 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 07:09:08 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 245 seconds)
2025-01-24 07:11:33 +0100JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-01-24 07:13:43 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 245 seconds)
2025-01-24 07:17:16 +0100takuan(~takuan@178-116-218-225.access.telenet.be)
2025-01-24 07:21:12 +0100eL_Bart0(eL_Bart0@dietunichtguten.org) (Ping timeout: 244 seconds)
2025-01-24 07:22:23 +0100ft(~ft@p508db1ba.dip0.t-ipconnect.de) (Quit: leaving)
2025-01-24 07:24:08 +0100EvanR_(~EvanR@user/evanr) EvanR
2025-01-24 07:24:38 +0100EvanR(~EvanR@user/evanr) (Read error: Connection reset by peer)
2025-01-24 07:24:53 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-01-24 07:24:54 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 07:29:12 +0100mange(~user@user/mange) (Quit: Quittin' time!)
2025-01-24 07:29:38 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 248 seconds)
2025-01-24 07:30:37 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-01-24 07:31:19 +0100euleritian(~euleritia@dynamic-176-006-145-062.176.6.pool.telefonica.de)
2025-01-24 07:33:54 +0100hughjfch1(~hughjfche@vmi2417424.contaboserver.net) hughjfchen
2025-01-24 07:40:42 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 07:45:34 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 07:45:39 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 07:46:35 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-01-24 07:48:28 +0100weary-traveler(~user@user/user363627) user363627
2025-01-24 07:49:55 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 264 seconds)
2025-01-24 07:52:04 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 07:54:50 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!)
2025-01-24 07:57:07 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 07:58:24 +0100remedan(~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan
2025-01-24 08:02:00 +0100user_(~user@user/fmira) (Ping timeout: 264 seconds)
2025-01-24 08:07:50 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 08:13:19 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 08:20:10 +0100szkl(uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2025-01-24 08:24:03 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 08:25:24 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Ping timeout: 264 seconds)
2025-01-24 08:27:15 +0100chexum(~quassel@gateway/tor-sasl/chexum) chexum
2025-01-24 08:28:53 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 244 seconds)
2025-01-24 08:32:33 +0100tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving)
2025-01-24 08:32:41 +0100zlqrvx(~zlqrvx@user/zlqrvx) (Quit: %quit%)
2025-01-24 08:33:02 +0100zlqrvx(~zlqrvx@user/zlqrvx) zlqrvx
2025-01-24 08:35:00 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 08:37:07 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2025-01-24 08:39:18 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 08:39:51 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 08:42:57 +0100tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) tcard
2025-01-24 08:45:48 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 08:53:05 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 08:54:18 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-24 08:54:36 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-01-24 08:58:13 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 248 seconds)
2025-01-24 09:00:01 +0100caconym(~caconym@user/caconym) (Quit: bye)
2025-01-24 09:00:44 +0100caconym(~caconym@user/caconym) caconym
2025-01-24 09:02:10 +0100Googulator(~Googulato@2a01-036d-0106-2445-f43e-80de-c8dc-0b63.pool6.digikabel.hu) (Ping timeout: 240 seconds)
2025-01-24 09:02:28 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 09:03:12 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 244 seconds)
2025-01-24 09:04:02 +0100CrunchyFlakes_(~CrunchyFl@ip923482e1.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds)
2025-01-24 09:05:20 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-01-24 09:06:03 +0100CrunchyFlakes(~CrunchyFl@ip923482e1.dynamic.kabel-deutschland.de)
2025-01-24 09:06:45 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 246 seconds)
2025-01-24 09:06:57 +0100swamp_(~zmt00@user/zmt00) (Ping timeout: 276 seconds)
2025-01-24 09:07:33 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 09:08:55 +0100alecs(~alecs@nat16.software.imdea.org) alecs
2025-01-24 09:10:07 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-01-24 09:16:13 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 245 seconds)
2025-01-24 09:17:31 +0100JuanDaugherty(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-01-24 09:19:17 +0100zmt00(~zmt00@user/zmt00) zmt00
2025-01-24 09:20:09 +0100zmt00(~zmt00@user/zmt00) (Remote host closed the connection)
2025-01-24 09:20:26 +0100acidjnk(~acidjnk@p200300d6e7283f4988944b924ab82f58.dip0.t-ipconnect.de) acidjnk
2025-01-24 09:23:07 +0100kuribas(~user@ip-188-118-57-242.reverse.destiny.be) kuribas
2025-01-24 09:23:24 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 09:27:25 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 09:27:36 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 09:32:54 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 272 seconds)
2025-01-24 09:43:33 +0100chele(~chele@user/chele) chele
2025-01-24 09:44:03 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 09:47:48 +0100tnt1(~Thunderbi@user/tnt1) (Remote host closed the connection)
2025-01-24 09:50:42 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 252 seconds)
2025-01-24 09:50:45 +0100euleritian(~euleritia@dynamic-176-006-145-062.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-01-24 09:51:03 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 09:54:05 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 09:55:11 +0100dhil(~dhil@2a0c:b381:588:5f00:29fc:4647:d8a6:1493) dhil
2025-01-24 09:56:48 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 09:57:12 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-01-24 09:59:31 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 10:00:52 +0100eL_Bart0(eL_Bart0@dietunichtguten.org)
2025-01-24 10:03:04 +0100zmt00(~zmt00@user/zmt00) zmt00
2025-01-24 10:09:53 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 10:10:19 +0100zmt00(~zmt00@user/zmt00) (Ping timeout: 264 seconds)
2025-01-24 10:11:35 +0100ash3en(~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en
2025-01-24 10:12:49 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 10:16:02 +0100ash3en(~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 265 seconds)
2025-01-24 10:17:09 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 248 seconds)
2025-01-24 10:17:09 +0100vpan(~vpan@212.117.1.172)
2025-01-24 10:26:07 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-01-24 10:35:30 +0100tv(~tv@user/tv) tv
2025-01-24 10:36:38 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-01-24 10:39:35 +0100sord937(~sord937@gateway/tor-sasl/sord937) sord937
2025-01-24 10:40:04 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-01-24 10:48:32 +0100pavonia(~user@user/siracusa) siracusa
2025-01-24 10:50:00 +0100hawer(~newyear@2.219.56.221) (Read error: Connection reset by peer)
2025-01-24 10:54:52 +0100monochrom(trebla@216.138.220.146) (Ping timeout: 252 seconds)
2025-01-24 10:55:07 +0100monochrom(trebla@216.138.220.146)
2025-01-24 10:57:30 +0100__monty__(~toonn@user/toonn) toonn
2025-01-24 11:00:22 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-24 11:01:53 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 11:06:10 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2025-01-24 11:06:43 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 264 seconds)
2025-01-24 11:09:07 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 264 seconds)
2025-01-24 11:15:46 +0100ash3en(~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en
2025-01-24 11:25:09 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2025-01-24 11:43:13 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2)
2025-01-24 11:44:17 +0100tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2025-01-24 11:50:58 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 11:51:51 +0100nefercheprureTMA
2025-01-24 11:55:22 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 12:03:43 +0100merijn(~merijn@62.45.137.128) (Ping timeout: 264 seconds)
2025-01-24 12:06:13 +0100homo(~homo@user/homo) (Remote host closed the connection)
2025-01-24 12:06:26 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 12:06:50 +0100homo(~homo@user/homo) homo
2025-01-24 12:07:22 +0100xff0x(~xff0x@2405:6580:b080:900:2b3c:b3c3:f979:5337)
2025-01-24 12:08:49 +0100Square2(~Square4@user/square) Square
2025-01-24 12:10:57 +0100dysthesis(~dysthesis@user/dysthesis) dysthesis
2025-01-24 12:17:19 +0100merijn(~merijn@62.45.137.128) merijn
2025-01-24 12:22:56 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-01-24 12:23:45 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 12:25:24 +0100dysthesis(~dysthesis@user/dysthesis) (Ping timeout: 264 seconds)
2025-01-24 12:27:55 +0100dysthesis(~dysthesis@user/dysthesis) dysthesis
2025-01-24 12:33:43 +0100hughjfch1(~hughjfche@vmi2417424.contaboserver.net) (Quit: WeeChat 4.4.3)
2025-01-24 12:34:14 +0100hughjfch1(~hughjfche@vmi2417424.contaboserver.net) hughjfchen
2025-01-24 12:34:14 +0100ash3en(~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Remote host closed the connection)
2025-01-24 12:39:43 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 12:39:43 +0100 <kuribas> merijn: Where you saying (forall a. Num a) is an existential, not a universal?
2025-01-24 12:40:41 +0100wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-01-24 12:41:56 +0100 <merijn> Whether I was saying that, that depends very much on what context that syntax is in. And my terminology is a sloppy mess anyway :p
2025-01-24 12:41:56 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-01-24 12:42:22 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 12:44:08 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 12:53:50 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2025-01-24 12:54:25 +0100euphores(~SASL_euph@user/euphores) (Ping timeout: 248 seconds)
2025-01-24 12:59:46 +0100rvalue-(~rvalue@user/rvalue) rvalue
2025-01-24 13:00:15 +0100rvalue(~rvalue@user/rvalue) (Ping timeout: 252 seconds)
2025-01-24 13:00:49 +0100wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2025-01-24 13:01:59 +0100euphores(~SASL_euph@user/euphores) euphores
2025-01-24 13:03:55 +0100ft(~ft@p508db1ba.dip0.t-ipconnect.de) ft
2025-01-24 13:04:29 +0100rvalue-rvalue
2025-01-24 13:04:45 +0100 <dminuoso> kuribas: That type is not existential.
2025-01-24 13:04:50 +0100V(~v@ircpuzzles/2022/april/winner/V) V
2025-01-24 13:10:25 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 248 seconds)
2025-01-24 13:10:38 +0100 <dminuoso> `(∃a. ... a ...) -> r` however is an existential type and it is isomorphic to `∀ a. (... a ... -> r)`
2025-01-24 13:21:37 +0100Midjak(~MarciZ@82.66.147.146) Midjak
2025-01-24 13:29:28 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 13:29:57 +0100 <ncf> forall a. Num a is not a type
2025-01-24 13:30:51 +0100 <ncf> dminuoso: (∃a. ... a ...) is an existential type
2025-01-24 13:30:55 +0100 <ncf> (∃a. ... a ...) -> r is not
2025-01-24 13:33:10 +0100dysthesis(~dysthesis@user/dysthesis) (Remote host closed the connection)
2025-01-24 13:33:54 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-01-24 13:42:35 +0100Googulator(~Googulato@host-88-132-146-182.prtelecom.hu)
2025-01-24 13:46:28 +0100jespada(~jespada@2800:a4:2288:4600:a43e:beb4:c592:b90b) jespada
2025-01-24 13:52:24 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-01-24 13:52:49 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de)
2025-01-24 13:59:48 +0100visilii(~visilii@46.61.242.99) (Read error: Connection reset by peer)
2025-01-24 14:01:07 +0100visilii(~visilii@46.61.242.99)
2025-01-24 14:02:23 +0100iamsleepy(~weechat@2a01:4f9:3070:feff:9969:2d95:7b68:eef5) (Read error: Connection reset by peer)
2025-01-24 14:02:47 +0100iamsleepy(~weechat@2a01:4f9:3070:feff:a9de:dfff:cd7f:fdcd) iamsleepy
2025-01-24 14:16:10 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2025-01-24 14:18:12 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 14:18:25 +0100 <kuribas> ncf: it is with impredicative types enabled?
2025-01-24 14:18:51 +0100 <ncf> no
2025-01-24 14:19:11 +0100 <kuribas> well (forall a. Num a => a)
2025-01-24 14:20:08 +0100 <ncf> yes
2025-01-24 14:20:13 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-01-24 14:22:24 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-01-24 14:28:41 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-01-24 14:38:30 +0100Everything(~Everythin@195.138.86.118) Everything
2025-01-24 14:39:19 +0100Smiles(uid551636@id-551636.lymington.irccloud.com) Smiles
2025-01-24 14:40:19 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 14:56:26 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2)
2025-01-24 14:56:29 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 252 seconds)
2025-01-24 15:00:56 +0100KicksonButt(~quassel@187.21.174.221)
2025-01-24 15:05:14 +0100KicksonButt(~quassel@187.21.174.221) (Client Quit)
2025-01-24 15:05:33 +0100KicksonButt(~quassel@187.21.174.221)
2025-01-24 15:07:57 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-01-24 15:11:41 +0100weary-traveler(~user@user/user363627) user363627
2025-01-24 15:11:46 +0100Arsen_Arsen
2025-01-24 15:12:43 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 264 seconds)
2025-01-24 15:15:12 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net)
2025-01-24 15:19:38 +0100simplystuart(~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 244 seconds)
2025-01-24 15:22:09 +0100 <dminuoso> ncf: Oh, I indeed mixed this one up.
2025-01-24 15:24:10 +0100Googulator(~Googulato@host-88-132-146-182.prtelecom.hu) (Ping timeout: 240 seconds)
2025-01-24 15:26:56 +0100 <kuribas> dminuoso: that's not valid haskell syntax
2025-01-24 15:27:20 +0100 <dminuoso> kuribas: Half of it is.
2025-01-24 15:27:38 +0100 <merijn> Actually ∀ totally is valid haskell with -XUnicodeSyntax :p
2025-01-24 15:27:49 +0100 <dminuoso> Yes we do not have `∃x.` .. but then again we do not really have existential codes (except for those encoded via universal quantification)
2025-01-24 15:30:33 +0100 <kuribas> We do have existential types.
2025-01-24 15:30:43 +0100 <dminuoso> kuribas: Let me rephrase:
2025-01-24 15:30:47 +0100 <dminuoso> We do not have existential quantification.
2025-01-24 15:30:55 +0100 <dminuoso> Except that you encode it via the above isomorphism.
2025-01-24 15:31:20 +0100 <dminuoso> Not quite sure whether we can give a clean and accurate definition of what "an existential type" is exactly.
2025-01-24 15:32:12 +0100 <dminuoso> If an existential type is any quantified type where an `∃a. ...` could appear in, then `id` too is an existential type because we could encode it in terms of an existential quantifier.
2025-01-24 15:33:27 +0100 <dminuoso> s/too is an /too has an/
2025-01-24 15:35:47 +0100 <kuribas> "data Foo = forall a. Foo a" is an existential type.
2025-01-24 15:35:59 +0100 <kuribas> a is existential in Foo.
2025-01-24 15:36:13 +0100 <kuribas> Foo is not a function type.
2025-01-24 15:36:16 +0100 <dminuoso> That one is a bit funny.
2025-01-24 15:36:36 +0100 <dminuoso> So the language extension *is* called ExistentialQuantification, and if it had been faithful, it would have allowed to write:
2025-01-24 15:36:53 +0100 <dminuoso> `data Foo where Foo :: exists a. a -> Foo`
2025-01-24 15:37:22 +0100 <dminuoso> Instead it uses a very strange notation where you put the `forall a` into a strange spot, there by impying that.
2025-01-24 15:37:36 +0100 <dminuoso> % :set -XExistentialQuantification
2025-01-24 15:37:36 +0100 <yahb2> <no output>
2025-01-24 15:37:45 +0100 <dminuoso> % data Foo = forall a. Foo a
2025-01-24 15:37:45 +0100 <yahb2> <no output>
2025-01-24 15:37:47 +0100 <dminuoso> % :t Foo
2025-01-24 15:37:47 +0100 <yahb2> Foo :: a -> Foo
2025-01-24 15:38:19 +0100 <Leary> dminuoso: That should be `(exists a. a)`; you wouldn't even need GADTSyntax to write it.
2025-01-24 15:38:36 +0100 <dminuoso> Leary: Sure or that.
2025-01-24 15:38:55 +0100 <dminuoso> Leary: I just wanted to use GADTSyntax to avoid some confusion.
2025-01-24 15:41:04 +0100 <dminuoso> Can you make GHC print out quantifiers explicitly with :t ?
2025-01-24 15:43:14 +0100 <Leary> kuribas: `Foo` is also effectively "encoded via universal quantification" due to the fact that we need to type any code that interacts with it using only `forall`: `Foo :: forall a. a -> Foo`; `\f -> \case{ Foo x -> f x } :: forall r. (forall a. a -> r) -> r`.
2025-01-24 15:44:29 +0100 <Leary> *Foo -> r
2025-01-24 15:45:07 +0100 <Leary> Shouldda swapped those args, but you get the picture.
2025-01-24 15:45:59 +0100ubert(~Thunderbi@2a02:8109:ab8a:5a00:3d80:bfe2:3c69:fb84) ubert
2025-01-24 15:46:12 +0100 <dminuoso> I think the only sensible definition of "existential type" is one that has an existential quantifier inside it.
2025-01-24 15:46:32 +0100 <dminuoso> If its encoded via unviersal quantification, I would not call it an "existential type"
2025-01-24 15:47:11 +0100 <dminuoso> Otherwise there would be no distinction between "universal type" and "existential type", and thereby no reason to have two terms.
2025-01-24 15:47:45 +0100 <dminuoso> (Which begs the question what to call a type has both an existential and universal quantifier inside)
2025-01-24 15:48:06 +0100 <dminuoso> Maybe we should not use these terms at all.
2025-01-24 15:49:24 +0100euleritian(~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-01-24 15:50:31 +0100euleritian(~euleritia@dynamic-176-006-139-225.176.6.pool.telefonica.de)
2025-01-24 15:50:35 +0100 <Leary> The strict definition should be that a universal or existential type has the corresponding quantifier outermost, but in the absense of the latter quantifier and the presence of reasonable encodings thereof, that definition obviously just isn't pragmatic enough.