2024/07/16

2024-07-16 00:00:50 +0200jcarpenter2(~lol@2603:3016:1e01:b9a0:5c24:ab66:e174:b6d5)
2024-07-16 00:04:01 +0200__monty__(~toonn@user/toonn) (Quit: leaving)
2024-07-16 00:19:29 +0200pavonia(~user@user/siracusa)
2024-07-16 00:20:56 +0200mud(~mud@user/kadoban) (Remote host closed the connection)
2024-07-16 00:21:23 +0200mud(~mud@user/kadoban)
2024-07-16 00:24:35 +0200dyniec(~dyniec@dybiec.info)
2024-07-16 00:29:04 +0200 <monochrom> Oh w00t new ghcup version!
2024-07-16 00:29:57 +0200 <int-e> hmm why is that exciting?
2024-07-16 00:30:00 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2024-07-16 00:30:19 +0200euleritian(~euleritia@dynamic-176-005-135-121.176.5.pool.telefonica.de)
2024-07-16 00:30:21 +0200 <monochrom> Because I'm bored >:)
2024-07-16 00:30:45 +0200euleritian(~euleritia@dynamic-176-005-135-121.176.5.pool.telefonica.de) (Read error: Connection reset by peer)
2024-07-16 00:30:58 +0200euleritian(~euleritia@pd9ebb103.dip0.t-ipconnect.de)
2024-07-16 00:34:07 +0200 <yushyin> software that is well-maintained also gets me excited sometimes, because these days it is not a given!
2024-07-16 00:35:52 +0200sadie-sorceress(~sadie-sor@c-71-229-185-228.hsd1.co.comcast.net)
2024-07-16 00:39:22 +0200 <davean> When was it?
2024-07-16 00:39:57 +0200 <davean> I'll spool up my timemachine
2024-07-16 00:40:06 +0200acidjnk(~acidjnk@p200300d6e72cfb855d3b0bd945f63b84.dip0.t-ipconnect.de) (Ping timeout: 258 seconds)
2024-07-16 00:44:59 +0200emmanuelux(~emmanuelu@user/emmanuelux)
2024-07-16 00:47:15 +0200ddellacosta(~ddellacos@172.59.176.161)
2024-07-16 00:53:33 +0200ddellacosta(~ddellacos@172.59.176.161) (Ping timeout: 246 seconds)
2024-07-16 00:53:42 +0200CrunchyFlakes(~CrunchyFl@146.52.130.128) (Read error: Connection reset by peer)
2024-07-16 00:55:00 +0200 <EvanR> well-maintained is relative right. It evokes a picture where The Ambient Software Platform keeps making changes which make your motionless code suddenly look broken
2024-07-16 00:55:19 +0200 <EvanR> given that, what does it mean for The Ambient Software Platform to be well-maintained?
2024-07-16 00:55:32 +0200ddellacosta(~ddellacos@ool-44c73d29.dyn.optonline.net)
2024-07-16 00:55:36 +0200 <geekosaur> isn't that the definition for web stuff?
2024-07-16 00:56:19 +0200CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
2024-07-16 00:58:00 +0200sadie-sorceress(~sadie-sor@c-71-229-185-228.hsd1.co.comcast.net) (Quit: Client closed)
2024-07-16 00:58:25 +0200 <yin> yushyin: these days? has it ever been?
2024-07-16 00:58:40 +0200Umeaboy(~Umeaboy@94-255-145-133.cust.bredband2.com) (Quit: Leaving)
2024-07-16 00:58:55 +0200 <EvanR> if I go into my code and write absolute nonsense that doesn't compile, can I complain that the compiler and OS aren't well-maintained xD
2024-07-16 01:06:19 +0200bearen(Thunderbir@user/bearen) (Ping timeout: 265 seconds)
2024-07-16 01:07:05 +0200pointlessslippe1(~pointless@212.82.82.3) (Ping timeout: 252 seconds)
2024-07-16 01:09:24 +0200ae(~ae@user/ae)
2024-07-16 01:11:57 +0200Sgeo(~Sgeo@user/sgeo)
2024-07-16 01:12:21 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-07-16 01:18:58 +0200 <ae> greetings :)
2024-07-16 01:27:54 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2024-07-16 01:43:36 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds)
2024-07-16 01:45:54 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-07-16 02:04:11 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 264 seconds)
2024-07-16 02:04:50 +0200Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 252 seconds)
2024-07-16 02:05:41 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk)
2024-07-16 02:08:11 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
2024-07-16 02:09:45 +0200Maxdamantus(~Maxdamant@user/maxdamantus)
2024-07-16 02:28:58 +0200ystael_(~ystael@user/ystael) (Ping timeout: 265 seconds)
2024-07-16 02:55:07 +0200yin(~yin@user/zero) (Ping timeout: 268 seconds)
2024-07-16 02:58:59 +0200ystael(~ystael@user/ystael)
2024-07-16 03:00:57 +0200tomku(~tomku@user/tomku) (Ping timeout: 246 seconds)
2024-07-16 03:01:44 +0200yin(~yin@user/zero)
2024-07-16 03:03:06 +0200tomku(~tomku@user/tomku)
2024-07-16 03:06:55 +0200ystael(~ystael@user/ystael) (Ping timeout: 258 seconds)
2024-07-16 03:17:23 +0200saraband(~saraband@pool-173-73-24-54.washdc.fios.verizon.net)
2024-07-16 03:20:35 +0200saraband(~saraband@pool-173-73-24-54.washdc.fios.verizon.net) (Client Quit)
2024-07-16 03:21:54 +0200tabemann(~tabemann@2600:1700:7990:24e0:12ef:2120:f770:f8cc) (Remote host closed the connection)
2024-07-16 03:22:21 +0200tabemann(~tabemann@2600:1700:7990:24e0:7233:7c99:3fac:5c8c)
2024-07-16 03:29:58 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 245 seconds)
2024-07-16 03:32:06 +0200acarrico(~acarrico@dhcp-68-142-57-215.greenmountainaccess.net) (Quit: Leaving.)
2024-07-16 03:35:11 +0200dysthesis(~dysthesis@user/dysthesis)
2024-07-16 03:37:42 +0200aforemny(~aforemny@2001:9e8:6cd2:fc00:1da8:718a:ae87:dc3a) (Ping timeout: 246 seconds)
2024-07-16 03:38:33 +0200aforemny(~aforemny@89.245.22.200)
2024-07-16 03:43:13 +0200g00gler(uid125351@id-125351.uxbridge.irccloud.com)
2024-07-16 03:52:07 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-07-16 03:58:53 +0200harveypwca(~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288)
2024-07-16 04:02:15 +0200 <dmj`> there should be a THIH that uses the constraint solving approach
2024-07-16 04:03:27 +0200Square2(~Square@user/square)
2024-07-16 04:17:23 +0200lain`(lain`@user/lain/x-9874679) (Ping timeout: 252 seconds)
2024-07-16 04:18:59 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:afa:a01:eb90:b007)
2024-07-16 04:20:27 +0200lain`(lain`@user/lain/x-9874679)
2024-07-16 04:24:33 +0200td_(~td@i53870911.versanet.de) (Ping timeout: 245 seconds)
2024-07-16 04:26:26 +0200td_(~td@i53870918.versanet.de)
2024-07-16 04:34:03 +0200harveypwca(~harveypwc@2601:246:d080:b40:1889:d9bf:2dd8:b288) (Quit: Leaving)
2024-07-16 04:39:07 +0200vizimajac(~Rodney@97e7368c.skybroadband.com) (Ping timeout: 264 seconds)
2024-07-16 04:45:43 +0200yin(~yin@user/zero) (Ping timeout: 264 seconds)
2024-07-16 04:51:35 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
2024-07-16 04:57:56 +0200dysthesis(~dysthesis@user/dysthesis) (Ping timeout: 260 seconds)
2024-07-16 05:07:26 +0200vizimajac(~Rodney@90.201.223.82)
2024-07-16 05:14:18 +0200aforemny_(~aforemny@2001:9e8:6cee:ed00:5f3f:c04b:274:bbf)
2024-07-16 05:15:43 +0200aforemny(~aforemny@89.245.22.200) (Ping timeout: 265 seconds)
2024-07-16 05:25:36 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2024-07-16 05:45:05 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:afa:a01:eb90:b007) (Quit: Leaving)
2024-07-16 06:02:06 +0200g00gler(uid125351@id-125351.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2024-07-16 06:04:36 +0200CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-07-16 06:07:13 +0200CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
2024-07-16 06:12:52 +0200mniip(mniip@libera/staff/mniip) (*.net *.split)
2024-07-16 06:12:52 +0200bastelfreak(bastelfrea@libera/staff/VoxPupuli.bastelfreak) (*.net *.split)
2024-07-16 06:12:59 +0200mniip(mniip@libera/staff/mniip)
2024-07-16 06:13:13 +0200bastelfreak(bastelfrea@libera/staff/VoxPupuli.bastelfreak)
2024-07-16 06:18:25 +0200letsgethexy(~mrdeeds@173.16.247.92)
2024-07-16 06:25:11 +0200spider(spider@tilde.cafe) (Server closed connection)
2024-07-16 06:25:29 +0200spider(spider@tilde.cafe)
2024-07-16 06:30:28 +0200letsgethexy(~mrdeeds@173.16.247.92) (Remote host closed the connection)
2024-07-16 06:46:25 +0200emmanuelux_(~emmanuelu@user/emmanuelux)
2024-07-16 06:49:08 +0200emmanuelux(~emmanuelu@user/emmanuelux) (Ping timeout: 245 seconds)
2024-07-16 06:53:36 +0200CATS(apic@brezn3.muc.ccc.de) (Server closed connection)
2024-07-16 06:53:47 +0200CATS(apic@brezn3.muc.ccc.de)
2024-07-16 06:55:47 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds)
2024-07-16 06:56:42 +0200int-e(~noone@int-e.eu) (Server closed connection)
2024-07-16 06:56:52 +0200int-e(~noone@int-e.eu)
2024-07-16 06:57:17 +0200aws(~alews@user/aws) (Server closed connection)
2024-07-16 06:57:34 +0200aws(~alews@user/aws)
2024-07-16 07:13:02 +0200tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection)
2024-07-16 07:13:15 +0200tcard(~tcard@2400:4051:5801:7500:1e90:74c3:2754:ce8a)
2024-07-16 07:30:21 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-07-16 07:33:57 +0200misterfish(~misterfis@84.53.85.146) (Ping timeout: 246 seconds)
2024-07-16 07:34:29 +0200sweater(~sweater@206.81.18.26) (Server closed connection)
2024-07-16 07:34:47 +0200sweater(~sweater@206.81.18.26)
2024-07-16 07:38:48 +0200acidjnk(~acidjnk@p200300d6e72cfb805cd63c25806f679d.dip0.t-ipconnect.de)
2024-07-16 07:40:46 +0200brettgilio(~brettgili@154.3.237.18)
2024-07-16 07:43:47 +0200ario(~ario@159.65.220.102) (Server closed connection)
2024-07-16 07:43:55 +0200ario(~ario@159.65.220.102)
2024-07-16 07:44:45 +0200byte(~byte@149.28.222.189) (Server closed connection)
2024-07-16 07:45:03 +0200byte(~byte@149.28.222.189)
2024-07-16 07:48:42 +0200glguy(g@libera/staff/glguy) (Read error: Connection reset by peer)
2024-07-16 07:49:29 +0200vgtw(~vgtw@user/vgtw)
2024-07-16 07:51:33 +0200glguy(glguy@libera/staff/glguy)
2024-07-16 08:01:12 +0200rosco(~rosco@175.136.155.137)
2024-07-16 08:01:39 +0200bilegeek(~bilegeek@2600:1008:b09a:c2ab:ba0b:9828:fe58:2964)
2024-07-16 08:07:06 +0200vgtw(~vgtw@user/vgtw) (Quit: ZNC - https://znc.in)
2024-07-16 08:18:20 +0200Dykam(Dykam@dykam.nl) (Server closed connection)
2024-07-16 08:18:33 +0200Dykam(Dykam@dykam.nl)
2024-07-16 08:20:43 +0200ethantwardy(user@user/ethantwardy) (Ping timeout: 268 seconds)
2024-07-16 08:20:43 +0200mmaruseacph2(~mihai@mihai.page) (Ping timeout: 268 seconds)
2024-07-16 08:20:58 +0200mmaruseacph2(~mihai@mihai.page)
2024-07-16 08:21:07 +0200ethantwardy(user@user/ethantwardy)
2024-07-16 08:21:21 +0200meejah(~meejah@104.236.166.239) (Ping timeout: 268 seconds)
2024-07-16 08:22:47 +0200meejah(~meejah@rutas.meejah.ca)
2024-07-16 08:24:12 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-07-16 08:30:44 +0200joeyh_(~joeyh@kitenet.net) (Server closed connection)
2024-07-16 08:30:55 +0200joeyh(~joeyh@kitenet.net)
2024-07-16 08:32:12 +0200m1dnight(~christoph@82.146.125.185) (Quit: WeeChat 4.2.2)
2024-07-16 08:32:53 +0200m1dnight(~christoph@82.146.125.185)
2024-07-16 08:44:41 +0200lockna_(~lockna@static.139.16.130.94.clients.your-server.de) (Server closed connection)
2024-07-16 08:44:55 +0200lockna(~lockna@2a01:4f8:10b:14f1::2)
2024-07-16 08:48:09 +0200gmg(~user@user/gehmehgeh)
2024-07-16 08:48:55 +0200JimL(~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
2024-07-16 08:55:36 +0200__monty__(~toonn@user/toonn)
2024-07-16 08:57:36 +0200mima(~mmh@user/mima) (Server closed connection)
2024-07-16 08:57:51 +0200mima(~mmh@user/mima)
2024-07-16 08:58:23 +0200pointlessslippe1(~pointless@212.82.82.3)
2024-07-16 09:00:01 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-07-16 09:00:32 +0200xelxebar(~xelxebar@wilsonb.com) (Quit: ZNC 1.7.2+deb3 - https://znc.in)
2024-07-16 09:02:30 +0200Maxdamantus(~Maxdamant@user/maxdamantus) (Ping timeout: 246 seconds)
2024-07-16 09:04:22 +0200Maxdamantus(~Maxdamant@user/maxdamantus)
2024-07-16 09:06:23 +0200tdammers_(~tdammers@41-138-178-143.ftth.glasoperator.nl) (Server closed connection)
2024-07-16 09:06:46 +0200tdammers_(~tdammers@41-138-178-143.ftth.glasoperator.nl)
2024-07-16 09:08:34 +0200vgtw(~vgtw@user/vgtw)
2024-07-16 09:14:31 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
2024-07-16 09:17:40 +0200xelxebar(~xelxebar@wilsonb.com)
2024-07-16 09:24:36 +0200xelxebar(~xelxebar@wilsonb.com) (Quit: ZNC 1.7.2+deb3 - https://znc.in)
2024-07-16 09:24:48 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-07-16 09:25:02 +0200xelxebar(~xelxebar@wilsonb.com)
2024-07-16 09:27:02 +0200puke(~puke@user/puke) (Remote host closed the connection)
2024-07-16 09:33:37 +0200xelxebar(~xelxebar@wilsonb.com) (Quit: ZNC 1.7.2+deb3 - https://znc.in)
2024-07-16 09:34:02 +0200xelxebar(~xelxebar@wilsonb.com)
2024-07-16 09:40:29 +0200quintasan(~quassel@quintasan.pl) (Server closed connection)
2024-07-16 09:40:38 +0200quintasan(~quassel@quintasan.pl)
2024-07-16 09:43:25 +0200emmanuelux_(~emmanuelu@user/emmanuelux) (Quit: au revoir)
2024-07-16 09:44:21 +0200ft(~ft@p4fc2ab80.dip0.t-ipconnect.de) (Quit: leaving)
2024-07-16 09:52:06 +0200euleritian(~euleritia@pd9ebb103.dip0.t-ipconnect.de) (Ping timeout: 258 seconds)
2024-07-16 09:53:14 +0200cpressey(~weechat@176.254.71.203)
2024-07-16 09:55:23 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-07-16 09:56:49 +0200euleritian(~euleritia@dynamic-176-005-135-121.176.5.pool.telefonica.de)
2024-07-16 09:57:52 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-07-16 10:18:12 +0200tstat(~tstat@user/tstat) (Server closed connection)
2024-07-16 10:19:00 +0200tstat(~tstat@user/tstat)
2024-07-16 10:19:11 +0200misterfish(~misterfis@87.215.131.102)
2024-07-16 10:20:38 +0200econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2024-07-16 10:23:25 +0200danse-nr3(~danse-nr3@151.37.183.46)
2024-07-16 10:23:52 +0200JamesMowery(~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Quit: Ping timeout (120 seconds))
2024-07-16 10:24:12 +0200JamesMowery(~JamesMowe@ip98-167-207-182.ph.ph.cox.net)
2024-07-16 10:32:50 +0200danse-nr3(~danse-nr3@151.37.183.46) (Ping timeout: 248 seconds)
2024-07-16 10:36:34 +0200dolio(~dolio@130.44.134.54) (Ping timeout: 264 seconds)
2024-07-16 10:37:02 +0200danse-nr3(~danse-nr3@151.37.183.46)
2024-07-16 10:43:25 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
2024-07-16 10:45:39 +0200CiaoSen(~Jura@2a05:5800:2b3:5600:e6b9:7aff:fe80:3d03)
2024-07-16 10:46:41 +0200bryanv(~quassel@2603:c028:4503:7500:45b7:933:ab17:bc10) (Server closed connection)
2024-07-16 10:46:55 +0200bryanv(~quassel@2603:c028:4503:7500:45b7:933:ab17:bc10)
2024-07-16 10:52:16 +0200dolio(~dolio@130.44.134.54)
2024-07-16 10:58:17 +0200yangby(~secret@115.204.116.173)
2024-07-16 11:01:38 +0200dolio(~dolio@130.44.134.54) (Ping timeout: 272 seconds)
2024-07-16 11:03:28 +0200bilegeek(~bilegeek@2600:1008:b09a:c2ab:ba0b:9828:fe58:2964) (Quit: Leaving)
2024-07-16 11:17:23 +0200JamesMowery0(~JamesMowe@ip98-167-207-182.ph.ph.cox.net)
2024-07-16 11:19:14 +0200JamesMowery(~JamesMowe@ip98-167-207-182.ph.ph.cox.net) (Ping timeout: 248 seconds)
2024-07-16 11:19:14 +0200JamesMowery0JamesMowery
2024-07-16 11:19:48 +0200danse-nr3(~danse-nr3@151.37.183.46) (Changing host)
2024-07-16 11:19:48 +0200danse-nr3(~danse-nr3@user/danse-nr3)
2024-07-16 11:26:24 +0200abrar(~abrar@pool-72-78-199-167.phlapa.fios.verizon.net) (Server closed connection)
2024-07-16 11:26:42 +0200misterfish(~misterfis@87.215.131.102) (Ping timeout: 248 seconds)
2024-07-16 11:26:48 +0200abrar(~abrar@pool-72-78-199-167.phlapa.fios.verizon.net)
2024-07-16 11:28:40 +0200misterfish(~misterfis@178.225.158.139)
2024-07-16 11:34:02 +0200chele(~chele@user/chele)
2024-07-16 11:44:29 +0200Raito_Bezarius(~Raito@wireguard/tunneler/raito-bezarius) (Server closed connection)
2024-07-16 11:45:53 +0200Raito_Bezarius(~Raito@wireguard/tunneler/raito-bezarius)
2024-07-16 11:59:59 +0200stefan-_(~cri@42dots.de) (Server closed connection)
2024-07-16 12:00:14 +0200stefan-_(~cri@42dots.de)
2024-07-16 12:00:16 +0200Jackneill_(~Jackneill@178-164-177-183.pool.digikabel.hu) (Quit: Leaving)
2024-07-16 12:10:23 +0200enikar(~enikar@user/enikar) (Server closed connection)
2024-07-16 12:10:42 +0200enikar(~enikar@user/enikar)
2024-07-16 12:11:17 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-07-16 12:21:27 +0200 <tromp> what is the type of Church numeral 2 in CoC (Calculus of Constructions) ? Is it Nat = forall(a : *) -> (a -> a) -> a -> a ?
2024-07-16 12:23:08 +0200Square2(~Square@user/square) (Ping timeout: 258 seconds)
2024-07-16 12:25:14 +0200 <ncf> all church numerals have the same type
2024-07-16 12:25:30 +0200mikess(~mikess@user/mikess) (Ping timeout: 246 seconds)
2024-07-16 12:28:02 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Ping timeout: 248 seconds)
2024-07-16 12:39:00 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-07-16 12:39:46 +0200 <tromp> got disconnected; hope I didn't miss an answer...
2024-07-16 12:40:53 +0200 <ncf> all church numerals have the same type
2024-07-16 12:51:56 +0200 <tromp> i know
2024-07-16 12:52:17 +0200 <tromp> is that the correct type?
2024-07-16 12:52:53 +0200 <ncf> sure
2024-07-16 12:53:25 +0200 <tromp> is that short for forall(a : *) -> forall(_ : (forall(_ : a -> a)) -> forall(_ : a) -> a ?
2024-07-16 12:54:31 +0200 <tromp> i.e. 4 uses of the Pi constructor?
2024-07-16 12:55:49 +0200 <ncf> yes
2024-07-16 12:56:40 +0200 <ncf> (a : *) → (_ : (_ : a) → a) → (_ : a) → a
2024-07-16 12:59:14 +0200 <tromp> Thanks. Does anyone know of a Haskell implementation of Loader's Number? https://googology.fandom.com/wiki/Loader%27s_number
2024-07-16 13:03:16 +0200 <ncf> that would be cool, but i don't
2024-07-16 13:10:17 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com)
2024-07-16 13:10:19 +0200danse-nr3(~danse-nr3@user/danse-nr3) (Quit: Leaving)
2024-07-16 13:19:33 +0200mcfrdy(~mcfrdy@user/mcfrdy) (Server closed connection)
2024-07-16 13:19:53 +0200mcfrdy(~mcfrdy@user/mcfrdy)
2024-07-16 13:21:21 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 260 seconds)
2024-07-16 13:23:35 +0200FinnElija(~finn_elij@user/finn-elija/x-0085643)
2024-07-16 13:28:06 +0200sprout(~quassel@2a02-a448-3a80-0-bd3d-b7cf-ad17-1736.fixed6.kpn.net) (Read error: Connection reset by peer)
2024-07-16 13:31:58 +0200sprout(~quassel@2a02-a448-3a80-0-1da5-990b-8c01-534d.fixed6.kpn.net)
2024-07-16 13:36:22 +0200misterfish(~misterfis@178.225.158.139) (Ping timeout: 244 seconds)
2024-07-16 13:37:11 +0200emergence(emergence@2607:5300:60:5910:dcad:beff:feef:5bc) (Server closed connection)
2024-07-16 13:37:23 +0200emergence(emergence@2607:5300:60:5910:dcad:beff:feef:5bc)
2024-07-16 13:37:59 +0200misterfish(~misterfis@87.215.131.102)
2024-07-16 13:41:11 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds)
2024-07-16 13:41:35 +0200yangby(~secret@115.204.116.173) (Quit: Go out for a walk and buy a drink.)
2024-07-16 13:41:39 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-07-16 13:56:51 +0200td_(~td@i53870918.versanet.de) (Ping timeout: 246 seconds)
2024-07-16 13:57:04 +0200td_(~td@i53870918.versanet.de)
2024-07-16 14:01:06 +0200nullie(~nullie@2a01:4f8:c2c:6177::1) (Quit: WeeChat 4.2.2)
2024-07-16 14:01:10 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-07-16 14:01:24 +0200hexeme(~hexeme@user/hexeme) (Server closed connection)
2024-07-16 14:01:25 +0200nullie(~nullie@2a01:4f8:c2c:6177::1)
2024-07-16 14:02:19 +0200hexeme(~hexeme@user/hexeme)
2024-07-16 14:04:23 +0200nullie(~nullie@2a01:4f8:c2c:6177::1) (Client Quit)
2024-07-16 14:04:40 +0200cpressey(~weechat@176.254.71.203) (Ping timeout: 272 seconds)
2024-07-16 14:04:46 +0200nullie(~nullie@2a01:4f8:c2c:6177::1)
2024-07-16 14:05:40 +0200nullie(~nullie@2a01:4f8:c2c:6177::1) (Client Quit)
2024-07-16 14:05:57 +0200nullie(~nullie@nuremberg.nullie.name)
2024-07-16 14:08:30 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2024-07-16 14:11:12 +0200ddellacosta(~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 246 seconds)
2024-07-16 14:40:33 +0200m5zs7k(aquares@web10.mydevil.net) (Ping timeout: 252 seconds)
2024-07-16 14:40:55 +0200AlexZenon(~alzenon@178.34.160.117) (Quit: ;-)
2024-07-16 14:41:45 +0200AlexNoo(~AlexNoo@178.34.160.117) (Quit: Leaving)
2024-07-16 14:42:33 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-07-16 14:43:38 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit)
2024-07-16 14:45:24 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-07-16 14:46:21 +0200Sciencentistguy(~sciencent@hacksoc/ordinary-member) (Server closed connection)
2024-07-16 14:46:43 +0200Sciencentistguy(~sciencent@hacksoc/ordinary-member)
2024-07-16 14:49:50 +0200yin(~yin@user/zero)
2024-07-16 14:50:18 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-07-16 14:50:39 +0200califax(~califax@user/califx)
2024-07-16 14:54:06 +0200MironZ3(~MironZ@nat-infra.ehlab.uk) (Server closed connection)
2024-07-16 14:54:29 +0200MironZ3(~MironZ@nat-infra.ehlab.uk)
2024-07-16 14:58:21 +0200Square2(~Square@user/square)
2024-07-16 15:06:53 +0200cpressey(~weechat@176.254.71.203)
2024-07-16 15:07:06 +0200 <haskellbridge> <mauke> Why are messages from ncf shown as coming from "haskellbridge" on the Matrix side?
2024-07-16 15:13:55 +0200m5zs7k(aquares@web10.mydevil.net)
2024-07-16 15:16:46 +0200AlexNoo(~AlexNoo@178.34.160.117)
2024-07-16 15:17:10 +0200AlexZenon(~alzenon@178.34.160.117)
2024-07-16 15:17:54 +0200 <ncf> um, because i'm on irc?
2024-07-16 15:19:06 +0200 <ncf> test
2024-07-16 15:20:20 +0200 <ncf> yeah i guess that's weird. geekosaur?
2024-07-16 15:23:26 +0200kuribas(~user@ip-188-118-57-242.reverse.destiny.be)
2024-07-16 15:31:15 +0200 <EvanR> test
2024-07-16 15:50:47 +0200hugo-(hugo@quicksilver.lysator.liu.se) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in)
2024-07-16 16:06:58 +0200ystael(~ystael@user/ystael)
2024-07-16 16:14:42 +0200kaol(~kaol@94-237-42-30.nl-ams1.upcloud.host) (Server closed connection)
2024-07-16 16:14:49 +0200kaol(~kaol@94-237-42-30.nl-ams1.upcloud.host)
2024-07-16 16:15:46 +0200chiselfuse(~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds)
2024-07-16 16:16:51 +0200chiselfuse(~chiselfus@user/chiselfuse)
2024-07-16 16:29:06 +0200 <geekosaur> "view raw" says your client is sending notices instead of messages
2024-07-16 16:29:23 +0200 <geekosaur> …wait, but it just did that to mine too
2024-07-16 16:30:05 +0200haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection)
2024-07-16 16:30:25 +0200 <geekosaur> uh oh
2024-07-16 16:30:27 +0200haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com)
2024-07-16 16:30:27 +0200ChanServ+v haskellbridge
2024-07-16 16:31:04 +0200 <tomsmeding> test
2024-07-16 16:31:11 +0200kritzefitz(~kritzefit@debian/kritzefitz) (Ping timeout: 264 seconds)
2024-07-16 16:31:21 +0200 <geekosaur> foo
2024-07-16 16:31:45 +0200 <geekosaur> working now
2024-07-16 16:31:57 +0200 <ncf> 🐝
2024-07-16 16:32:15 +0200 <mauke> what happen?
2024-07-16 16:32:23 +0200chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2024-07-16 16:32:24 +0200gmg(~user@user/gehmehgeh) (Remote host closed the connection)
2024-07-16 16:32:24 +0200 <geekosaur> dunno
2024-07-16 16:32:25 +0200ChaiTRex(~ChaiTRex@user/chaitrex) (Remote host closed the connection)
2024-07-16 16:32:25 +0200chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2024-07-16 16:32:33 +0200 <ncf> yay
2024-07-16 16:32:39 +0200chexum(~quassel@gateway/tor-sasl/chexum)
2024-07-16 16:32:57 +0200ChaiTRex(~ChaiTRex@user/chaitrex)
2024-07-16 16:33:10 +0200chiselfuse(~chiselfus@user/chiselfuse)
2024-07-16 16:33:10 +0200 <geekosaur> I did restart it a couple days ago, maybe they had a bad update (I'm running from their `latest` docker container)
2024-07-16 16:33:20 +0200gmg(~user@user/gehmehgeh)
2024-07-16 16:40:05 +0200deriamis_(deriamis@ec2-54-187-167-69.us-west-2.compute.amazonaws.com) (Server closed connection)
2024-07-16 16:41:04 +0200deriamis(deriamis@2600:1f14:1251:ba02:2994:f9dc:75a8:113b)
2024-07-16 16:48:53 +0200 <haskellbridge> <thirdofmay18081814goya> anyone got suggestions for declaring nested records to parse a nested json object? any extension that would allow me to declare a single nested record data type instead of needing to make a new data type for each subsequent nested record?
2024-07-16 16:49:18 +0200 <haskellbridge> <thirdofmay18081814goya> e.g. i'd like to make a data type that models
2024-07-16 16:49:18 +0200 <haskellbridge> ... long message truncated: https://kf8nh.com/_matrix/media/v3/download/kf8nh.com/fJODeknIoqILfAADEYDhRSUD (27 lines)
2024-07-16 16:50:55 +0200kritzefitz(~kritzefit@debian/kritzefitz)
2024-07-16 16:52:11 +0200 <mauke> with aeson, wouldn't that just be custom FromJSON/ToJSON instances?
2024-07-16 16:52:33 +0200 <haskellbridge> <thirdofmay18081814goya> mauke: yeah but i'd like to declare it in a single data type
2024-07-16 16:52:40 +0200 <mauke> except you don't get "nested records" on the haskell side
2024-07-16 16:52:50 +0200 <mauke> you can do it with a flat record, though
2024-07-16 16:53:23 +0200zetef(~quassel@82.76.106.80)
2024-07-16 16:53:44 +0200zetef(~quassel@82.76.106.80) (Client Quit)
2024-07-16 16:54:21 +0200ash3en(~ash3en@89.246.174.164)
2024-07-16 16:54:29 +0200 <haskellbridge> <thirdofmay18081814goya> mauke: yeah purely as a question of presentation i wanted to avoid multiple flat records
2024-07-16 16:54:47 +0200 <tomsmeding> what would the desired set of data types be?
2024-07-16 16:54:56 +0200 <tomsmeding> if you don't want nested records
2024-07-16 16:54:59 +0200 <mauke> ... multiple?
2024-07-16 16:55:14 +0200 <tomsmeding> or is it "I want the normal thing but I want to type less code"
2024-07-16 16:55:50 +0200 <haskellbridge> <thirdofmay18081814goya> mauke: yeah, one record for the "response" data type, and another for each nested record within "response": "identity", "stock", "dimensions", etc.
2024-07-16 16:56:53 +0200 <tomsmeding> there is no extension that will create that set of data types for you from some smaller description of the structure
2024-07-16 16:57:05 +0200 <tomsmeding> you could write some TemplateHaskell and make it though :p
2024-07-16 16:57:16 +0200 <cheater> i was just going to say that TH is one such extension
2024-07-16 16:57:46 +0200 <haskellbridge> <thirdofmay18081814goya> yeah might be a template haskell question, i have multiple of these i'd like to define. really i just want to have a nice self-contained type declaration i can look at, it's not for any other reason
2024-07-16 16:57:52 +0200 <haskellbridge> <thirdofmay18081814goya> will look up how i might do this with TH, ty
2024-07-16 16:58:18 +0200 <mauke> https://hackage.haskell.org/package/aeson-2.2.3.0/docs/Data-Aeson.html#g:2
2024-07-16 16:58:28 +0200 <cheater> can it be you're just not used to what haskell looks like
2024-07-16 16:58:43 +0200 <cheater> sometimes the best hack is no hack at all
2024-07-16 16:58:56 +0200 <cheater> keep doing things the way god intended
2024-07-16 16:59:54 +0200ddellacosta(~ddellacos@ool-44c73d29.dyn.optonline.net)
2024-07-16 17:00:12 +0200 <haskellbridge> <thirdofmay18081814goya> heheh it's possible, but i enjoy typescript's self-contained presentation of this sort of type
2024-07-16 17:00:15 +0200 <ash3en> what is the TH situation? is this not needed magic hackery causing headaches or superior meta programming for pros?
2024-07-16 17:00:48 +0200ezzieyguywuf(~Unknown@user/ezzieyguywuf)
2024-07-16 17:01:05 +0200 <ash3en> or rephrased: is TH elegant?
2024-07-16 17:02:19 +0200 <tomsmeding> that is in the eye of the beholder :)
2024-07-16 17:02:56 +0200 <mauke> yesn't
2024-07-16 17:04:18 +0200ddellacosta(~ddellacos@ool-44c73d29.dyn.optonline.net) (Ping timeout: 248 seconds)
2024-07-16 17:07:07 +0200 <ash3en> intuively it *feels* like a liability and breaking haskell concepts. but otoh it may use haskell to it's fullest! arghh help lol
2024-07-16 17:13:00 +0200misterfish(~misterfis@87.215.131.102) (Ping timeout: 252 seconds)
2024-07-16 17:13:54 +0200 <haskellbridge> <thirdofmay18081814goya> there's an anonymous records library that's being maintained
2024-07-16 17:13:55 +0200 <haskellbridge> <thirdofmay18081814goya> "large-anon"
2024-07-16 17:16:05 +0200chele(~chele@user/chele) (Remote host closed the connection)
2024-07-16 17:16:34 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 248 seconds)
2024-07-16 17:19:48 +0200kosmikus(~kosmikus@nullzig.kosmikus.org) (Server closed connection)
2024-07-16 17:20:00 +0200kosmikus(~kosmikus@nullzig.kosmikus.org)
2024-07-16 17:22:52 +0200 <haskellbridge> <thirdofmay18081814goya> found someone who already did the work: https://github.com/brandonchinn178/aeson-schemas
2024-07-16 17:23:01 +0200 <haskellbridge> <thirdofmay18081814goya> bless 'em
2024-07-16 17:30:41 +0200 <EvanR> last resort TH is also bad because of compile times
2024-07-16 17:30:57 +0200 <tomsmeding> what is "last resort TH"?
2024-07-16 17:31:40 +0200 <EvanR> just TH
2024-07-16 17:32:09 +0200 <EvanR> metaprogramming = missing language feature
2024-07-16 17:32:36 +0200 <tomsmeding> or experimental language feature
2024-07-16 17:32:55 +0200 <tomsmeding> or language feature that would be nice but would unnecessarily burden the maintainers of the language implementation for something that only you use
2024-07-16 17:33:07 +0200 <tomsmeding> metaprogramming _is_ a language feature
2024-07-16 17:33:31 +0200 <tomsmeding> to the extent that various languages do metaprogramming in vastly different ways
2024-07-16 17:34:19 +0200 <tomsmeding> Rust even has two: macro_rules! and procedural macros
2024-07-16 17:35:24 +0200 <EvanR> it covers all missing language features
2024-07-16 17:35:45 +0200 <EvanR> but not necessarily in the best and most efficient way
2024-07-16 17:35:45 +0200 <tomsmeding> no, there are language features that you cannot cover with most existing metaprogramming designs
2024-07-16 17:35:57 +0200 <EvanR> like what
2024-07-16 17:36:08 +0200 <tomsmeding> IO from a language that doesn't have IO?
2024-07-16 17:36:21 +0200 <EvanR> how does this apply to TH
2024-07-16 17:36:28 +0200 <tomsmeding> you were talking about metaprogramming in general :p
2024-07-16 17:36:45 +0200 <EvanR> yeah there is crippled metaprogramming
2024-07-16 17:36:51 +0200 <EvanR> like C preprocessor
2024-07-16 17:37:05 +0200 <tomsmeding> no matter how good your metaprogramming, if the base language does not have IO, you're not going to metaprogram yourself to IO
2024-07-16 17:37:19 +0200 <EvanR> by IO are you just talking about a type system
2024-07-16 17:37:35 +0200 <EvanR> clearly most languages have I/O
2024-07-16 17:37:38 +0200 <tomsmeding> no I mean stuff like lua where if the host does not give you IO libraries, you _cannot do IO_
2024-07-16 17:38:02 +0200 <tomsmeding> which is the point of lua as an embedded language, the host can restrict what kind of side effects are possible
2024-07-16 17:38:18 +0200 <tomsmeding> by simply not giving you the functions which would perform those side effects
2024-07-16 17:38:21 +0200 <EvanR> lua has I/O unless you go out of your way to cripple it and move it to the host
2024-07-16 17:38:32 +0200 <EvanR> but I don't know if this matters to the argument
2024-07-16 17:38:46 +0200 <tomsmeding> I took issue with your blanket statements that metaprogramming fixes all problems :p
2024-07-16 17:38:53 +0200 <EvanR> it doesn't really have metaprogramming
2024-07-16 17:39:18 +0200 <tomsmeding> and even assuming that you're in a turing-complete language with side effects etc, you could perhaps theoretically map any kind of code to whatever you want it to mean
2024-07-16 17:39:30 +0200 <tomsmeding> but it's not like that's practical or a decent way to implement a missing language feature :p
2024-07-16 17:39:39 +0200 <EvanR> that's what I was saying
2024-07-16 17:39:52 +0200 <tomsmeding> then why do you say "it covers all missing language features"
2024-07-16 17:39:57 +0200 <tomsmeding> technically correct, maybe
2024-07-16 17:40:27 +0200 <tomsmeding> still, I could want interactive hole filling in haskell
2024-07-16 17:40:28 +0200 <EvanR> stop argeeing!
2024-07-16 17:40:32 +0200 <tomsmeding> is that a language feature or a compiler feature?
2024-07-16 17:40:39 +0200 <tomsmeding> lol
2024-07-16 17:40:59 +0200 <tomsmeding> as in, "technically correct if you choose unhelpful definitions of the words in question"
2024-07-16 17:41:13 +0200 <tomsmeding> anyway this discussion got longer than it was meant to lol
2024-07-16 17:41:36 +0200 <tomsmeding> sorry for the rant
2024-07-16 17:42:07 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2024-07-16 17:42:18 +0200kuribas(~user@ip-188-118-57-242.reverse.destiny.be) (ERC (IRC client for Emacs 27.1))
2024-07-16 17:42:21 +0200danse-nr3(~danse-nr3@user/danse-nr3)
2024-07-16 17:42:28 +0200L29Ah(~L29Ah@wikipedia/L29Ah)
2024-07-16 17:43:46 +0200ystael(~ystael@user/ystael) (Ping timeout: 248 seconds)
2024-07-16 17:44:51 +0200ystael(~ystael@user/ystael)
2024-07-16 17:45:07 +0200ash3en(~ash3en@89.246.174.164) (Remote host closed the connection)
2024-07-16 17:52:51 +0200 <haskellbridge> <thirdofmay18081814goya> what's your preferred approach to refinement types in haskell?
2024-07-16 17:52:54 +0200 <haskellbridge> <thirdofmay18081814goya> liquid haskell?
2024-07-16 17:54:18 +0200 <EvanR> smart constructors
2024-07-16 17:55:00 +0200 <EvanR> liquid haskell is another language
2024-07-16 18:05:24 +0200 <haskellbridge> <thirdofmay18081814goya> EvanR: hm, you can't call these in type declarations
2024-07-16 18:05:50 +0200 <haskellbridge> <thirdofmay18081814goya> +(if you want to use refinement types to declare other types)
2024-07-16 18:05:59 +0200 <EvanR> in liquid haskell?
2024-07-16 18:06:10 +0200mikess(~mikess@user/mikess)
2024-07-16 18:06:24 +0200 <haskellbridge> <thirdofmay18081814goya> no in standard haskell
2024-07-16 18:08:37 +0200 <EvanR> haskell doesn't have refinement types
2024-07-16 18:10:58 +0200CiaoSen(~Jura@2a05:5800:2b3:5600:e6b9:7aff:fe80:3d03) (Ping timeout: 248 seconds)
2024-07-16 18:16:06 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 272 seconds)
2024-07-16 18:16:11 +0200albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8) (Server closed connection)
2024-07-16 18:17:54 +0200dolio(~dolio@130.44.140.168)
2024-07-16 18:19:52 +0200econo_(uid147250@id-147250.tinside.irccloud.com)
2024-07-16 18:23:14 +0200albet70(~xxx@2400:8902::f03c:92ff:fe60:98d8)
2024-07-16 18:27:14 +0200Apollyon(~Apollyon@user/Apollyon)
2024-07-16 18:27:29 +0200danse-nr3(~danse-nr3@user/danse-nr3) (Ping timeout: 248 seconds)
2024-07-16 18:29:33 +0200Athas(athas@sigkill.dk) (Server closed connection)
2024-07-16 18:31:06 +0200ames(~amelia@offtopia/offtopian/amelia) (Server closed connection)
2024-07-16 18:31:07 +0200Athas(athas@2a01:7c8:aaac:1cf:43b5:af0:11ab:b009)
2024-07-16 18:31:18 +0200ames(~amelia@offtopia/offtopian/amelia)
2024-07-16 18:32:41 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
2024-07-16 18:34:45 +0200tomku(~tomku@user/tomku) (Ping timeout: 246 seconds)
2024-07-16 18:38:51 +0200manwithluck(manwithluc@gateway/vpn/protonvpn/manwithluck) (Server closed connection)
2024-07-16 18:39:18 +0200manwithluck(manwithluc@gateway/vpn/protonvpn/manwithluck)
2024-07-16 18:40:27 +0200cpressey(~weechat@176.254.71.203) (Ping timeout: 252 seconds)
2024-07-16 18:41:35 +0200tomku(~tomku@user/tomku)
2024-07-16 18:45:10 +0200danse-nr3(~danse-nr3@user/danse-nr3)
2024-07-16 18:46:53 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 244 seconds)
2024-07-16 18:54:08 +0200phma(~phma@host-67-44-208-24.hnremote.net) (Read error: Connection reset by peer)
2024-07-16 18:57:53 +0200Square2(~Square@user/square) (Ping timeout: 248 seconds)
2024-07-16 18:59:35 +0200ft(~ft@p4fc2ab80.dip0.t-ipconnect.de)
2024-07-16 19:03:00 +0200danse-nr3(~danse-nr3@user/danse-nr3) (Ping timeout: 252 seconds)
2024-07-16 19:06:49 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2024-07-16 19:12:38 +0200misterfish(~misterfis@84.53.85.146)
2024-07-16 19:12:54 +0200phma(~phma@host-67-44-208-140.hnremote.net)
2024-07-16 19:22:54 +0200 <amjoseph> tromp thanks for posting that! would never have expected that the [sequence whose limit is the] proof-theoretic ordinal for CoC can be computed by such a short program. i'm a bit surprised, however, that they didn't *prove* that it actually computes that. you should be able to prove it in coq since iirc CiC has strictly greater consistency strength. anyways, TIL; thanks.
2024-07-16 19:23:05 +0200ash3en(~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20)
2024-07-16 19:23:58 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-07-16 19:25:36 +0200 <amjoseph> tromp (also) maybe try asking sridhar ramesh?
2024-07-16 19:27:44 +0200rosco(~rosco@175.136.155.137) (Quit: Lost terminal)
2024-07-16 19:28:02 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
2024-07-16 19:32:05 +0200danse-nr3(~danse-nr3@user/danse-nr3)
2024-07-16 19:37:06 +0200danse-nr3(~danse-nr3@user/danse-nr3) (Ping timeout: 252 seconds)
2024-07-16 19:37:37 +0200destituion(~destituio@2001:4644:c37:0:5095:eb5b:7529:4c8f)
2024-07-16 19:38:13 +0200danse-nr3(~danse-nr3@user/danse-nr3)
2024-07-16 19:40:34 +0200AlexZenon(~alzenon@178.34.160.117) (Ping timeout: 248 seconds)
2024-07-16 19:40:56 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-07-16 19:44:44 +0200infinity0_(~infinity0@pwned.gg)
2024-07-16 19:45:08 +0200AlexZenon(~alzenon@178.34.160.117)
2024-07-16 19:45:52 +0200infinity0(~infinity0@pwned.gg) (Ping timeout: 246 seconds)
2024-07-16 19:47:00 +0200misterfish(~misterfis@84.53.85.146) (Ping timeout: 252 seconds)
2024-07-16 19:51:49 +0200misterfish(~misterfis@84.53.85.146)
2024-07-16 19:55:51 +0200 <mauke> :t \x y -> ?f x y <= EQ
2024-07-16 19:55:52 +0200 <lambdabot> (?f::t1 -> t2 -> Ordering) => t1 -> t2 -> Bool
2024-07-16 19:56:21 +0200zfnmxt(~zfnmxt@user/zfnmxt) (Server closed connection)
2024-07-16 19:56:39 +0200zfnmxt(~zfnmxt@user/zfnmxt)
2024-07-16 19:56:48 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 272 seconds)
2024-07-16 20:02:02 +0200wagle(~wagle@quassel.wagle.io) (Server closed connection)
2024-07-16 20:02:17 +0200wagle(~wagle@quassel.wagle.io)
2024-07-16 20:18:57 +0200misterfish(~misterfis@84.53.85.146) (Ping timeout: 248 seconds)
2024-07-16 20:21:19 +0200ash3en(~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) (Ping timeout: 256 seconds)
2024-07-16 20:24:18 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds)
2024-07-16 20:25:12 +0200misterfish(~misterfis@84.53.85.146)
2024-07-16 20:25:56 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915)
2024-07-16 20:33:53 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2024-07-16 20:35:41 +0200doyougnu(~doyougnu@syn-045-046-170-068.res.spectrum.com) (Server closed connection)
2024-07-16 20:35:57 +0200doyougnu(~doyougnu@syn-045-046-170-068.res.spectrum.com)
2024-07-16 20:38:46 +0200califax(~califax@user/califx) (Remote host closed the connection)
2024-07-16 20:39:03 +0200califax(~califax@user/califx)
2024-07-16 20:40:54 +0200Apollyon(~Apollyon@user/Apollyon) (Remote host closed the connection)
2024-07-16 20:41:18 +0200jespada(~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Server closed connection)
2024-07-16 20:44:30 +0200cpressey(~weechat@176.254.71.203)
2024-07-16 20:46:29 +0200gmg(~user@user/gehmehgeh)
2024-07-16 20:46:51 +0200jespada(~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net)
2024-07-16 20:49:57 +0200raehik(~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
2024-07-16 20:53:11 +0200koz(~koz@121.99.240.58) (Server closed connection)
2024-07-16 20:53:27 +0200koz(~koz@121.99.240.58)
2024-07-16 20:54:51 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-07-16 20:54:53 +0200 <stefan-__> is it possible to check if a FilePath exists (and if not show an error) when extracting CLI params via optparse-applicative?
2024-07-16 20:57:23 +0200Angelz(Angelz@user/angelz) (Server closed connection)
2024-07-16 20:59:06 +0200 <mud> stefan-__: Not saying you definitely shouldn't do that, but: be careful of the pattern of check-first for files. It leads to race conditions, things can change between when you check and when you actually use it.
2024-07-16 20:59:23 +0200 <mud> You're usually better off just dealing with the error _as_ you use the file, because you're going to have to do it there anyway.
2024-07-16 21:01:47 +0200ash3en(~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20)
2024-07-16 21:02:32 +0200bearen(Thunderbir@user/bearen)
2024-07-16 21:08:01 +0200Angelz(Angelz@Angelz.oddprotocol.org)
2024-07-16 21:09:48 +0200simendsjo(~user@31-209-41-70.cust.bredband2.com)
2024-07-16 21:15:31 +0200euphores(~SASL_euph@user/euphores)
2024-07-16 21:19:04 +0200Maeda(~Maeda@91-161-10-149.subs.proxad.net) (Quit: leaving)
2024-07-16 21:19:05 +0200c_wraith(~c_wraith@adjoint.us) (Server closed connection)
2024-07-16 21:20:15 +0200c_wraith(~c_wraith@adjoint.us)
2024-07-16 21:21:58 +0200 <EvanR> boldly open the file and if there is a reasonable thing to do other than crash in case of a problem, catch the specific exception
2024-07-16 21:24:01 +0200 <EvanR> or in a more complicated application, check the result of the async thread tasked with doing something with that file
2024-07-16 21:25:00 +0200danse-nr3(~danse-nr3@user/danse-nr3) (Read error: Connection reset by peer)
2024-07-16 21:25:30 +0200danse-nr3(~danse-nr3@user/danse-nr3)
2024-07-16 21:27:06 +0200destituion(~destituio@2001:4644:c37:0:5095:eb5b:7529:4c8f) (Ping timeout: 252 seconds)
2024-07-16 21:27:48 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-07-16 21:29:33 +0200destituion(~destituio@2a02:2121:6b6:b142:8d9d:8eb3:8da8:98dd)
2024-07-16 21:59:36 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2024-07-16 22:01:48 +0200danse-nr3(~danse-nr3@user/danse-nr3) (Quit: Leaving)
2024-07-16 22:16:21 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com)
2024-07-16 22:17:51 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-07-16 22:24:41 +0200A_Dragon(A_D@libera/staff/dragon) (Quit: ZNC - https://znc.in)
2024-07-16 22:24:56 +0200A_Dragon(A_D@libera/staff/dragon)
2024-07-16 22:25:23 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-07-16 22:25:41 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
2024-07-16 22:27:10 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-07-16 22:29:17 +0200 <stefan-__> mud + EvanR: thanks, maybe this even better fits separation of concerns, in the way that optparse-applicative is really only used for CLI param parsing
2024-07-16 22:30:23 +0200 <raehik> I want to sort a list-like `f a`. I have an `a -> a -> Ordering`. Is there a way I can do this polymorphically over `f`?
2024-07-16 22:31:07 +0200 <ncf> raehik: https://elvishjerricco.github.io/2017/03/23/applicative-sorting.html ?
2024-07-16 22:31:37 +0200 <mreh> what about using Foldable?
2024-07-16 22:32:30 +0200 <raehik> mreh: Foldable is for folding operations. I don't want to fold the list to a single value
2024-07-16 22:32:36 +0200tomku(~tomku@user/tomku) (Ping timeout: 272 seconds)
2024-07-16 22:32:40 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2024-07-16 22:32:44 +0200 <raehik> I can't see an `f a -> f a` operation in Foldable
2024-07-16 22:32:47 +0200 <mreh> :t toList
2024-07-16 22:32:48 +0200 <lambdabot> Foldable t => t a -> [a]
2024-07-16 22:32:51 +0200tomku(~tomku@user/tomku)
2024-07-16 22:33:10 +0200 <mreh> half way there
2024-07-16 22:33:29 +0200 <ncf> you obviously need Traversable
2024-07-16 22:33:45 +0200 <ncf> or something equivalent
2024-07-16 22:34:14 +0200 <raehik> mreh: this lets me sort `f a`, but at the cost of going between List, which isn't really what I was looking for
2024-07-16 22:34:27 +0200 <mreh> raehik: listen to ncf
2024-07-16 22:34:44 +0200simendsjo(~user@31-209-41-70.cust.bredband2.com) (Ping timeout: 244 seconds)
2024-07-16 22:34:49 +0200 <raehik> ncf: thanks for that, looks interesting!
2024-07-16 22:34:52 +0200 <mreh> You want to substitute elements in the functor for each other, traversable sounds like a good fit to me
2024-07-16 22:37:33 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-07-16 22:38:00 +0200 <raehik> my thought process was "what if I had a `Vector a` and wanted to sort it quickly", but... I can't see a sort op in the vector package. huh
2024-07-16 22:39:34 +0200mrehwonders how does one update a collection using multiple concurrent `Event (f a -> f a)`s in reflex...
2024-07-16 22:39:46 +0200 <mreh> raehik: what flavour of Vector?
2024-07-16 22:40:05 +0200 <mreh> and what does quickly mean?
2024-07-16 22:40:16 +0200 <raehik> Any, say Primitive
2024-07-16 22:40:40 +0200CiaoSen(~Jura@2a05:5800:2b3:5600:e6b9:7aff:fe80:3d03)
2024-07-16 22:40:53 +0200 <raehik> quickly as in init a new vector of the same size and write into it
2024-07-16 22:41:39 +0200 <mreh> I would just convert between Vector a and [a] and back again probably
2024-07-16 22:41:53 +0200 <raehik> perhaps stream fusion permits simply going through List
2024-07-16 22:42:10 +0200 <haskellbridge> <Jade> `vector-algorithms` has fast sorts
2024-07-16 22:42:12 +0200connrs(~connrs@user/connrs) (Server closed connection)
2024-07-16 22:42:28 +0200connrs(~connrs@user/connrs)
2024-07-16 22:42:56 +0200 <raehik> Ah! yes, fantastic. I knew of that pkg too haha
2024-07-16 22:43:03 +0200 <raehik> it does in-place sorts so hard to Hoogle
2024-07-16 22:44:47 +0200it_(~quassel@v2202212189510211193.supersrv.de) (Server closed connection)
2024-07-16 22:44:55 +0200it_(~quassel@v2202212189510211193.supersrv.de)
2024-07-16 22:49:54 +0200cpressey(~weechat@176.254.71.203) (Ping timeout: 248 seconds)
2024-07-16 22:51:30 +0200pieguy128(~pieguy128@bras-base-mtrlpq5031w-grc-45-67-70-24-166.dsl.bell.ca) (Server closed connection)
2024-07-16 22:52:54 +0200pieguy128(~pieguy128@bras-base-mtrlpq5031w-grc-45-67-70-24-166.dsl.bell.ca)
2024-07-16 22:55:24 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 244 seconds)
2024-07-16 22:55:28 +0200 <raehik> I've used mutable vectors before and I still had to search around to confirm how to do basic things (`modify`)...
2024-07-16 23:02:09 +0200misterfish(~misterfis@84.53.85.146) (Ping timeout: 248 seconds)
2024-07-16 23:02:10 +0200AlexZenon(~alzenon@178.34.160.117) (Ping timeout: 248 seconds)
2024-07-16 23:03:06 +0200 <raehik> it'd also be nice if vector-algorithms endorsed certain sorts for different usages. I had to go through each module to check docs instead. perhaps that's the intended experience but felt a bit long-winded
2024-07-16 23:04:29 +0200emmanuelux(~emmanuelu@user/emmanuelux)
2024-07-16 23:09:38 +0200ash3en(~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) (Remote host closed the connection)
2024-07-16 23:09:46 +0200 <EvanR> haskell is fairly far down the road from "just sort my list-like thing I don't care how you do it"
2024-07-16 23:10:00 +0200 <EvanR> starting with how there's no generic "list-like" data structure
2024-07-16 23:10:01 +0200ash3en(~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20)
2024-07-16 23:10:30 +0200 <EvanR> you have to decide what string, what number, what whatever based on whether you're optimizing engineering effort or performance for the task
2024-07-16 23:10:32 +0200AlexZenon(~alzenon@178.34.160.117)
2024-07-16 23:11:43 +0200ash3en(~ash3en@2a02:3100:7db2:6b01:4f69:739c:8091:4c20) (Remote host closed the connection)
2024-07-16 23:13:43 +0200 <raehik> EvanR: Right, I agree. vector-algos gives many options for sorting
2024-07-16 23:14:20 +0200 <raehik> I was lamenting the lack of any package preamble or introduction. I don't want a button that says "just use this", I was hoping for a general overview
2024-07-16 23:15:21 +0200 <raehik> (perhaps you were looking at earlier messages, I was specifically keen on Vectors now)
2024-07-16 23:17:20 +0200 <monochrom> There is the issue of having heard of vector-algorithms in the first place. But suppose we're past that, then maybe you haven't seen the life hack of: click on any module, then click on "Index".
2024-07-16 23:18:03 +0200 <monochrom> BTW I also wish the "Index" link were on the package front page on hackage.
2024-07-16 23:20:04 +0200 <tomsmeding> monochrom: it is
2024-07-16 23:20:09 +0200 <tomsmeding> [Index] under Modules
2024-07-16 23:20:49 +0200 <monochrom> Ugh OK now I see but it's ant-size that's why I never saw it.
2024-07-16 23:21:21 +0200AlexZenon(~alzenon@178.34.160.117) (Ping timeout: 248 seconds)
2024-07-16 23:21:22 +0200 <tomsmeding> I myself am quite partial to Quick Jump, which is also brought up if you press the 's' key on the keyboard on any module page (and, for many packages -- but apparently not this one -- on the package front page)
2024-07-16 23:21:53 +0200 <tomsmeding> I found the link by searching for "index" on the page :p
2024-07-16 23:23:50 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-07-16 23:25:44 +0200__monty__(~toonn@user/toonn) (Quit: leaving)
2024-07-16 23:25:49 +0200AlexZenon(~alzenon@178.34.160.117)
2024-07-16 23:26:43 +0200 <raehik> monochrom: if that's the intended experience then all good I suppose. individual modules have great docs but the user is apparently expected to click around until they're happy with the algo they find
2024-07-16 23:27:23 +0200 <raehik> I was hoping for some benches and high-level notes. not actively complaining or searching for a fix
2024-07-16 23:27:32 +0200 <monochrom> I don't think it's intended. But I think people trust too much into hierarchies.
2024-07-16 23:28:00 +0200 <raehik> monochrom: as in module hierarchies? unclear what you mean
2024-07-16 23:30:09 +0200 <monochrom> OK let me describe my own dilemma. I teach multiple courses, over multiple semesters. Should my directory tree structure be "semester/course" or should it be "course/semester"? (Answer: "tree" is already wrong right there. Should be a matrix.)
2024-07-16 23:31:41 +0200 <monochrom> I even sometimes torment my C-and-Unix students with: "The prof was using the former but now changes his mind and wants to migrate to the latter! Write a shell script for that..."
2024-07-16 23:31:43 +0200 <raehik> you're absolutely right I hate hierarchies too. we need a filesystem based on tag matrices NOW
2024-07-16 23:33:31 +0200 <raehik> the current answer is, sadly, an overabundance of symlinks
2024-07-16 23:33:51 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com)
2024-07-16 23:36:56 +0200cpressey(~weechat@176.254.71.203)
2024-07-16 23:37:28 +0200infinity0_(~infinity0@pwned.gg) (Remote host closed the connection)
2024-07-16 23:37:51 +0200infinity0(~infinity0@pwned.gg)
2024-07-16 23:40:19 +0200Vajb(~Vajb@n84f8idehd0ucclhxoj-1.v6.elisa-mobile.fi) (Ping timeout: 264 seconds)
2024-07-16 23:40:35 +0200Vajb(~Vajb@n85jaspk9c2pfwcdhy6-1.v6.elisa-mobile.fi)
2024-07-16 23:46:47 +0200cpressey(~weechat@176.254.71.203) (Quit: WeeChat 4.3.0)
2024-07-16 23:47:20 +0200ddellacosta(~ddellacos@ool-44c73d29.dyn.optonline.net)
2024-07-16 23:48:37 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2024-07-16 23:51:46 +0200acidjnk(~acidjnk@p200300d6e72cfb805cd63c25806f679d.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
2024-07-16 23:59:45 +0200ystael(~ystael@user/ystael) (Ping timeout: 248 seconds)