2025/03/21

2025-03-21 00:00:11 +0100abiss27(~abiss27@190.213.236.106)
2025-03-21 00:01:17 +0100abiss27(~abiss27@190.213.236.106) (Changing host)
2025-03-21 00:01:17 +0100abiss27(~abiss27@user/abiss) abiss
2025-03-21 00:02:02 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-03-21 00:03:13 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-03-21 00:03:29 +0100 <monochrom> hehe
2025-03-21 00:03:56 +0100 <monochrom> "infer the type of id id id id id id id id id id id id"
2025-03-21 00:04:02 +0100 <monochrom> @quote monochrom 17-ary
2025-03-21 00:04:02 +0100 <lambdabot> monochrom says: I am 17-ary, going on 18-ary, I can take curry of you
2025-03-21 00:04:43 +0100Buliarou1(~gypsydang@46.232.210.139) (Remote host closed the connection)
2025-03-21 00:05:44 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-03-21 00:06:33 +0100yin(~z@user/zero) zero
2025-03-21 00:09:39 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 00:10:58 +0100abiss27(~abiss27@user/abiss) ()
2025-03-21 00:11:32 +0100abiss27(~abiss27@190.213.236.106)
2025-03-21 00:12:11 +0100xff0x(~xff0x@2405:6580:b080:900:810c:5794:3404:58c8) (Ping timeout: 265 seconds)
2025-03-21 00:12:28 +0100abiss27(~abiss27@190.213.236.106) (Client Quit)
2025-03-21 00:14:36 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-03-21 00:20:49 +0100abiss27(~abiss27@user/abiss) abiss
2025-03-21 00:25:25 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 00:26:02 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 268 seconds)
2025-03-21 00:26:05 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 00:28:45 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2025-03-21 00:30:20 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 00:30:23 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 245 seconds)
2025-03-21 00:41:11 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 00:45:54 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-03-21 00:52:53 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 245 seconds)
2025-03-21 00:56:56 +0100kh0d(~kh0d@212.200.247.167) (Remote host closed the connection)
2025-03-21 00:56:59 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 00:57:51 +0100kh0d(~kh0d@212.200.247.167) kh0d
2025-03-21 00:59:35 +0100xff0x(~xff0x@2405:6580:b080:900:d229:f63b:2d49:ccd3)
2025-03-21 01:01:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 01:02:36 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 252 seconds)
2025-03-21 01:04:08 +0100kh0d(~kh0d@212.200.247.167) kh0d
2025-03-21 01:11:21 +0100abiss27(~abiss27@user/abiss) (Quit: I'm off, Goodbye!)
2025-03-21 01:11:49 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 01:12:46 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 01:14:52 +0100abiss27(~abiss27@190.213.236.106)
2025-03-21 01:15:59 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 265 seconds)
2025-03-21 01:16:34 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-03-21 01:17:28 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-21 01:19:04 +0100xff0x(~xff0x@2405:6580:b080:900:d229:f63b:2d49:ccd3) (Ping timeout: 260 seconds)
2025-03-21 01:20:58 +0100xff0x(~xff0x@2405:6580:b080:900:b993:7de8:b31e:5325)
2025-03-21 01:22:05 +0100abiss27(~abiss27@190.213.236.106) (Changing host)
2025-03-21 01:22:05 +0100abiss27(~abiss27@user/abiss) abiss
2025-03-21 01:23:12 +0100LainExperiments(~LainExper@user/LainExperiments) LainExperiments
2025-03-21 01:24:03 +0100abiss27(~abiss27@user/abiss) (Quit: I'm off, Goodbye!)
2025-03-21 01:24:42 +0100abiss27(~abiss27@190.213.236.106)
2025-03-21 01:26:06 +0100abiss27(~abiss27@190.213.236.106) (Client Quit)
2025-03-21 01:28:33 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 01:28:41 +0100LainExperiments4(~LainExper@user/LainExperiments) LainExperiments
2025-03-21 01:28:59 +0100kh0d(~kh0d@212.200.247.167)
2025-03-21 01:30:27 +0100LainExperiments4(~LainExper@user/LainExperiments) (Client Quit)
2025-03-21 01:30:45 +0100tabaqui(~tabaqui@167.71.80.236) (Ping timeout: 252 seconds)
2025-03-21 01:31:18 +0100LainExperiments(~LainExper@user/LainExperiments) (Ping timeout: 240 seconds)
2025-03-21 01:35:24 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 01:35:34 +0100sprotte24(~sprotte24@p200300d16f3eed00f17f1149f1ad7273.dip0.t-ipconnect.de) (Quit: Leaving)
2025-03-21 01:36:34 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 260 seconds)
2025-03-21 01:38:07 +0100notdabs(~Owner@2600:1700:69cf:9000:99ef:5e1b:cda4:8b3) (Read error: Connection reset by peer)
2025-03-21 01:39:50 +0100Square(~Square@user/square) Square
2025-03-21 01:40:55 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 01:41:53 +0100acidjnk(~acidjnk@p200300d6e71c4f9399301ab9560bdae8.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2025-03-21 01:43:24 +0100xff0x(~xff0x@2405:6580:b080:900:b993:7de8:b31e:5325) (Ping timeout: 260 seconds)
2025-03-21 01:43:56 +0100xff0x(~xff0x@2405:6580:b080:900:3522:3957:cbed:8aef)
2025-03-21 01:45:38 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-21 01:48:18 +0100acidjnk(~acidjnk@p200300d6e71c4f9399301ab9560bdae8.dip0.t-ipconnect.de) acidjnk
2025-03-21 01:50:18 +0100kh0d(~kh0d@212.200.247.167) kh0d
2025-03-21 01:51:46 +0100justsomeguy(~justsomeg@user/justsomeguy) justsomeguy
2025-03-21 01:53:35 +0100euleritian(~euleritia@95.90.214.149) (Remote host closed the connection)
2025-03-21 01:54:03 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 01:54:19 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-03-21 01:55:00 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 01:56:40 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 01:57:33 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 01:57:44 +0100Googulator88(~Googulato@2a01-036d-0106-0ae4-b88c-ff83-9891-e272.pool6.digikabel.hu) (Quit: Client closed)
2025-03-21 01:58:02 +0100Googulator88(~Googulato@80-95-93-233.pool.digikabel.hu)
2025-03-21 01:59:33 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 245 seconds)
2025-03-21 02:01:38 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 02:02:14 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-03-21 02:12:10 +0100j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-03-21 02:12:28 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 02:13:18 +0100xff0x(~xff0x@2405:6580:b080:900:3522:3957:cbed:8aef) (Ping timeout: 245 seconds)
2025-03-21 02:13:37 +0100Digit(~user@user/digit) Digit
2025-03-21 02:13:58 +0100kh0d(~kh0d@212.200.247.167) kh0d
2025-03-21 02:16:51 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-03-21 02:17:39 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-03-21 02:22:44 +0100Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-03-21 02:24:05 +0100acidjnk(~acidjnk@p200300d6e71c4f9399301ab9560bdae8.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-03-21 02:28:15 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 02:32:41 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-03-21 02:32:56 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 02:33:29 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-03-21 02:34:00 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-03-21 02:34:20 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 02:38:22 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 244 seconds)
2025-03-21 02:39:03 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Remote host closed the connection)
2025-03-21 02:39:23 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 02:42:37 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 02:44:02 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 02:45:10 +0100Square2(~Square4@user/square) Square
2025-03-21 02:46:51 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 244 seconds)
2025-03-21 02:47:53 +0100Square(~Square@user/square) (Ping timeout: 245 seconds)
2025-03-21 02:48:29 +0100tusko(uid478376@user/tusko) ()
2025-03-21 02:49:19 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 02:55:25 +0100mvk(~mvk@2607:fea8:5c96:5800::7ea9) mvk
2025-03-21 02:55:25 +0100mvk(~mvk@2607:fea8:5c96:5800::7ea9) (Client Quit)
2025-03-21 02:58:56 +0100kh0d(~kh0d@212.200.247.167) kh0d
2025-03-21 02:59:50 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 03:03:36 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 252 seconds)
2025-03-21 03:04:32 +0100user363627(~user@user/user363627) user363627
2025-03-21 03:04:42 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 03:07:20 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-03-21 03:08:20 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-21 03:08:36 +0100weary-traveler(~user@user/user363627) (Ping timeout: 265 seconds)
2025-03-21 03:12:41 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Ping timeout: 244 seconds)
2025-03-21 03:15:36 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 03:19:30 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-03-21 03:22:44 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 03:28:01 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 03:32:09 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 246 seconds)
2025-03-21 03:33:40 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 03:34:57 +0100kh0d(~kh0d@212.200.247.167) kh0d
2025-03-21 03:38:07 +0100j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-03-21 03:38:45 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-21 03:40:12 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 246 seconds)
2025-03-21 03:41:49 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-03-21 03:44:55 +0100j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-03-21 03:48:00 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-03-21 03:49:03 +0100j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-03-21 03:49:26 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-03-21 03:49:27 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 03:50:24 +0100tromp(~textual@2a02:a210:cba:8500:f085:be23:3f4e:4a7a) (Ping timeout: 244 seconds)
2025-03-21 03:54:12 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 03:59:23 +0100Guest9(~Guest9@2600:4040:52fa:9700:fd29:3b63:e979:8aca)
2025-03-21 03:59:52 +0100Guest9(~Guest9@2600:4040:52fa:9700:fd29:3b63:e979:8aca) (Client Quit)
2025-03-21 04:01:31 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 04:06:12 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-21 04:09:29 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-03-21 04:10:16 +0100kh0d(~kh0d@212.200.247.167) kh0d
2025-03-21 04:13:25 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 04:15:23 +0100kh0d(~kh0d@212.200.247.167) (Ping timeout: 245 seconds)
2025-03-21 04:16:37 +0100rvalue(~rvalue@user/rvalue) (Read error: Connection reset by peer)
2025-03-21 04:17:13 +0100rvalue(~rvalue@user/rvalue) rvalue
2025-03-21 04:17:15 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 04:17:40 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-03-21 04:18:45 +0100sudden(~cat@user/sudden) (Ping timeout: 248 seconds)
2025-03-21 04:19:49 +0100dsrt^(~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) (Ping timeout: 248 seconds)
2025-03-21 04:20:26 +0100sudden(~cat@user/sudden) sudden
2025-03-21 04:20:31 +0100dsrt^(~dsrt@c-71-199-187-173.hsd1.ga.comcast.net)
2025-03-21 04:22:39 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 04:27:44 +0100kh0d(~kh0d@212.200.65.86) kh0d
2025-03-21 04:33:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 04:33:19 +0100kh0d(~kh0d@212.200.65.86) (Ping timeout: 260 seconds)
2025-03-21 04:36:57 +0100user363627weary-traveler
2025-03-21 04:37:28 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 04:47:41 +0100kh0d(~kh0d@212.200.65.86) kh0d
2025-03-21 04:48:25 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 04:53:13 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-21 04:55:23 +0100Xe(~Xe@perl/impostor/xe) (Ping timeout: 245 seconds)
2025-03-21 04:57:04 +0100Xe(~Xe@perl/impostor/xe) Xe
2025-03-21 04:58:49 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 05:03:02 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 244 seconds)
2025-03-21 05:04:13 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 05:08:09 +0100tremon(~tremon@83.80.159.219) (Quit: getting boxed in)
2025-03-21 05:08:15 +0100Fijxu(~Fijxu@user/fijxu) (Quit: XD!!)
2025-03-21 05:11:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 05:12:17 +0100Fijxu(~Fijxu@user/fijxu) fijxu
2025-03-21 05:15:17 +0100azh_ming(~aaron@pool-108-48-188-212.washdc.fios.verizon.net)
2025-03-21 05:17:28 +0100aazh_anon_ming(~aazh_anon@pool-108-48-188-212.washdc.fios.verizon.net)
2025-03-21 05:18:46 +0100azh_ming(~aaron@pool-108-48-188-212.washdc.fios.verizon.net) (Quit: leaving)
2025-03-21 05:19:12 +0100aazh_anon_ming(~aazh_anon@pool-108-48-188-212.washdc.fios.verizon.net) (Remote host closed the connection)
2025-03-21 05:19:22 +0100azh_ming(~azh_ming@pool-108-48-188-212.washdc.fios.verizon.net)
2025-03-21 05:20:25 +0100 <azh_ming> @pl \f g x y -> f (x ++ g x) (g y)
2025-03-21 05:20:25 +0100 <lambdabot> join . ((flip . ((.) .)) .) . (. ap (++)) . (.)
2025-03-21 05:21:44 +0100Square(~Square@user/square) Square
2025-03-21 05:22:31 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 05:24:06 +0100azh_ming(~azh_ming@pool-108-48-188-212.washdc.fios.verizon.net) (Changing host)
2025-03-21 05:24:06 +0100azh_ming(~azh_ming@user/azh-ming:58353) azh_ming
2025-03-21 05:25:04 +0100Square2(~Square4@user/square) (Ping timeout: 260 seconds)
2025-03-21 05:27:21 +0100 <haskellbridge> <Bowuigi> Peak Haskell
2025-03-21 05:27:35 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-03-21 05:28:22 +0100azh_ming(~azh_ming@user/azh-ming:58353) (Remote host closed the connection)
2025-03-21 05:28:46 +0100azh_ming(~azh_ming@user/azh-ming:58353) azh_ming
2025-03-21 05:28:48 +0100azh_ming(~azh_ming@user/azh-ming:58353) (Remote host closed the connection)
2025-03-21 05:29:58 +0100azh_ming(~aaron@user/azh-ming:58353) azh_ming
2025-03-21 05:30:45 +0100 <azh_ming> /join #politics
2025-03-21 05:30:51 +0100azh_ming(~aaron@user/azh-ming:58353) (Client Quit)
2025-03-21 05:34:57 +0100azh_ming(~aaron@user/azh-ming:58353) azh_ming
2025-03-21 05:38:38 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 05:43:19 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 05:44:13 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 05:48:30 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 244 seconds)
2025-03-21 05:54:01 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 05:56:46 +0100kh0d(~kh0d@212.200.65.86) (Ping timeout: 244 seconds)
2025-03-21 05:57:24 +0100azh_ming(~aaron@user/azh-ming:58353) (Quit: leaving)
2025-03-21 05:58:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 06:01:12 +0100tavare(~tavare@user/tavare) tavare
2025-03-21 06:02:30 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 06:07:17 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 06:10:25 +0100Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2025-03-21 06:11:06 +0100ChaiTRex(~ChaiTRex@user/chaitrex) (Remote host closed the connection)
2025-03-21 06:11:43 +0100ChaiTRex(~ChaiTRex@user/chaitrex) ChaiTRex
2025-03-21 06:11:46 +0100kh0d(~kh0d@212.200.65.86) kh0d
2025-03-21 06:13:18 +0100olivial(~benjaminl@user/benjaminl) (Ping timeout: 244 seconds)
2025-03-21 06:14:53 +0100tavare(~tavare@user/tavare) (Remote host closed the connection)
2025-03-21 06:15:06 +0100Square(~Square@user/square) (Ping timeout: 252 seconds)
2025-03-21 06:15:39 +0100olivial(~benjaminl@user/benjaminl) benjaminl
2025-03-21 06:15:57 +0100jmcantrell(~weechat@user/jmcantrell) (Quit: WeeChat 4.5.2)
2025-03-21 06:16:24 +0100kh0d(~kh0d@212.200.65.86) (Ping timeout: 244 seconds)
2025-03-21 06:18:04 +0100shr\ke_(~shrike@user/paxhumana) paxhumana
2025-03-21 06:18:18 +0100shr\ke(~shrike@user/shrke:31298) (Ping timeout: 252 seconds)
2025-03-21 06:18:19 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 06:18:21 +0100shr\ke_shr\ke
2025-03-21 06:23:01 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-03-21 06:26:17 +0100michalz(~michalz@185.246.207.193)
2025-03-21 06:27:25 +0100arahael(~arahael@user/arahael) arahael
2025-03-21 06:29:17 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 06:29:47 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-21 06:31:12 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-03-21 06:33:42 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-03-21 06:34:04 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
2025-03-21 06:34:06 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 06:35:13 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-03-21 06:39:19 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 06:45:29 +0100kh0d(~kh0d@212.200.65.86) kh0d
2025-03-21 06:49:52 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 06:50:13 +0100kh0d(~kh0d@212.200.65.86) (Ping timeout: 248 seconds)
2025-03-21 06:50:52 +0100dolio(~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in)
2025-03-21 06:54:25 +0100dolio(~dolio@130.44.140.168) dolio
2025-03-21 06:56:00 +0100poscat(~poscat@user/poscat) (Quit: Bye)
2025-03-21 06:56:04 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 06:58:22 +0100poscat(~poscat@user/poscat) poscat
2025-03-21 07:00:20 +0100dolio(~dolio@130.44.140.168) (Quit: ZNC 1.9.1 - https://znc.in)
2025-03-21 07:03:32 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 07:08:56 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-03-21 07:09:33 +0100takuan(~takuan@d8D86B601.access.telenet.be)
2025-03-21 07:15:21 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 07:18:04 +0100kh0d(~kh0d@212.200.65.86)
2025-03-21 07:19:20 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 07:19:26 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 244 seconds)
2025-03-21 07:24:39 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 07:24:46 +0100kh0d(~kh0d@212.200.65.86) (Ping timeout: 265 seconds)
2025-03-21 07:35:07 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 07:40:03 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-03-21 07:43:10 +0100Inst(~Inst@user/Inst) Inst
2025-03-21 07:43:25 +0100 <Inst> curious, do you need to use IORef (or relatives) to cache top-level data?
2025-03-21 07:43:47 +0100acidjnk(~acidjnk@p200300d6e71c4f937555fc5a67c80b19.dip0.t-ipconnect.de) acidjnk
2025-03-21 07:44:00 +0100 <Inst> Let's say, I'm using a web framework. I define a webpage under Lucid, Lucid2, or Blaze on the top-level.
2025-03-21 07:45:14 +0100 <Inst> Every time the page is served, is the top-level definition re-evaluated? Or would it be more efficient to freeze it with IORef, then pass the IORef to the route handler as an argument, with the route handler being in MonadIO?
2025-03-21 07:47:24 +0100Inst(~Inst@user/Inst) (Remote host closed the connection)
2025-03-21 07:48:29 +0100synchromesh(~john@2406:5a00:24cf:bb00:19d8:9179:8622:bdf3) (Read error: Connection reset by peer)
2025-03-21 07:49:29 +0100synchromesh(~john@2406:5a00:24cf:bb00:19d8:9179:8622:bdf3) synchromesh
2025-03-21 07:49:50 +0100Inst(~Inst@user/Inst) Inst
2025-03-21 07:50:54 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 07:52:00 +0100Inst(~Inst@user/Inst) (Remote host closed the connection)
2025-03-21 07:54:35 +0100weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-03-21 07:55:48 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-03-21 07:56:55 +0100kh0d(~kh0d@212.200.65.86) kh0d
2025-03-21 07:58:41 +0100ash3en(~Thunderbi@89.56.182.235) ash3en
2025-03-21 08:00:01 +0100caconym(~caconym@user/caconym) (Quit: bye)
2025-03-21 08:00:46 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 08:00:56 +0100caconym(~caconym@user/caconym) caconym
2025-03-21 08:02:02 +0100 <Axman6> top level values are generally only evaluated once, just like all named things in Haskell. There are caveats to that though, if it's a function I can't remember what happens
2025-03-21 08:02:19 +0100 <Axman6> if it has a generic type, it might also not be cached
2025-03-21 08:02:53 +0100kh0d(~kh0d@212.200.65.86) (Ping timeout: 245 seconds)
2025-03-21 08:03:09 +0100ash3en(~Thunderbi@89.56.182.235) (Client Quit)
2025-03-21 08:04:33 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 08:04:47 +0100 <haskellbridge> <Liamzee> thanks, couldn't find an answer on Google
2025-03-21 08:04:58 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 245 seconds)
2025-03-21 08:05:17 +0100 <Axman6> I think CAF, constant applicative form, is a useful thing to search for, but my memory's rusty
2025-03-21 08:06:13 +0100 <haskellbridge> <Liamzee> thanks, but the term has confusion with the typeclass
2025-03-21 08:07:27 +0100 <haskellbridge> <Liamzee> With Lucid I suspect it might be better to burn the HTML down to a bytestring first
2025-03-21 08:07:38 +0100 <haskellbridge> <Liamzee> since it's a builder function
2025-03-21 08:07:51 +0100 <haskellbridge> <Liamzee> that's also a monad transformer
2025-03-21 08:08:27 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-03-21 08:08:43 +0100ft(~ft@p508db463.dip0.t-ipconnect.de) (Quit: leaving)
2025-03-21 08:09:04 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 08:09:48 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi) (Quit: wildsalander)
2025-03-21 08:11:07 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-03-21 08:11:19 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-03-21 08:13:27 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-03-21 08:13:56 +0100Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-03-21 08:14:00 +0100euleritian(~euleritia@95.90.214.149)
2025-03-21 08:14:33 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 245 seconds)
2025-03-21 08:14:47 +0100 <[exa]> Liamzee: what's the type of your toplevel definition btw? that usually determines whether it's gonna get cached or not.
2025-03-21 08:15:20 +0100Lord_of_Life_Lord_of_Life
2025-03-21 08:18:21 +0100kh0d(~kh0d@109.111.226.14)
2025-03-21 08:22:35 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 08:23:15 +0100kh0d(~kh0d@109.111.226.14) (Ping timeout: 252 seconds)
2025-03-21 08:26:00 +0100ash3en(~Thunderbi@89.56.182.235) ash3en
2025-03-21 08:28:06 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-03-21 08:29:59 +0100euleritian(~euleritia@95.90.214.149) (Ping timeout: 260 seconds)
2025-03-21 08:30:20 +0100dsrt^(~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) (Read error: Connection reset by peer)
2025-03-21 08:30:25 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 08:31:59 +0100j1n37-(~j1n37@user/j1n37) j1n37
2025-03-21 08:32:17 +0100j1n37(~j1n37@user/j1n37) (Ping timeout: 244 seconds)
2025-03-21 08:33:15 +0100dsrt^(~dsrt@c-71-199-187-173.hsd1.ga.comcast.net)
2025-03-21 08:37:36 +0100ash3en(~Thunderbi@89.56.182.235) (Ping timeout: 272 seconds)
2025-03-21 08:37:51 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-03-21 08:38:08 +0100dsrt^(~dsrt@c-71-199-187-173.hsd1.ga.comcast.net) (Ping timeout: 268 seconds)
2025-03-21 08:38:22 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 08:38:59 +0100dsrt^(~dsrt@c-71-199-187-173.hsd1.ga.comcast.net)
2025-03-21 08:43:21 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-21 08:43:44 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-03-21 08:44:26 +0100Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-03-21 08:45:47 +0100kh0d(~kh0d@109.111.226.14) kh0d
2025-03-21 08:46:31 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 08:50:18 +0100kh0d(~kh0d@109.111.226.14) (Ping timeout: 246 seconds)
2025-03-21 08:50:45 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 248 seconds)
2025-03-21 08:52:40 +0100ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-03-21 08:53:42 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-03-21 08:53:42 +0100ljdarj1ljdarj
2025-03-21 08:54:09 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 08:59:27 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-03-21 09:05:29 +0100kh0d(~kh0d@109.111.226.14) kh0d
2025-03-21 09:05:34 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 09:05:42 +0100Googulator88(~Googulato@80-95-93-233.pool.digikabel.hu) (Ping timeout: 240 seconds)
2025-03-21 09:06:44 +0100ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 260 seconds)
2025-03-21 09:10:31 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-03-21 09:11:26 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds)
2025-03-21 09:12:22 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 09:15:59 +0100tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Quit: Leaving)
2025-03-21 09:19:01 +0100peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 248 seconds)
2025-03-21 09:21:22 +0100merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-03-21 09:25:34 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Remote host closed the connection)
2025-03-21 09:25:34 +0100tzh_(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2025-03-21 09:30:23 +0100tcard(~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) tcard
2025-03-21 09:31:35 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 09:32:52 +0100JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-03-21 09:35:55 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-03-21 09:44:52 +0100tzh_(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-03-21 09:47:35 +0100ash3en(~Thunderbi@89.56.182.235) ash3en
2025-03-21 09:48:42 +0100 <haskellbridge> <Liamzee> Html () :(
2025-03-21 09:49:04 +0100 <haskellbridge> <Liamzee> so burn to bytestring, it'll get cached, but as a builder, which is afaik just a function pointer
2025-03-21 09:49:40 +0100lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-03-21 09:53:19 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi)
2025-03-21 09:58:27 +0100vanishingideal(~vanishing@user/vanishingideal) vanishingideal
2025-03-21 09:58:58 +0100JuanDaugherty(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-03-21 10:01:50 +0100__monty__(~toonn@user/toonn) toonn
2025-03-21 10:06:01 +0100krei-se-(~krei-se@p5dea1e73.dip0.t-ipconnect.de) krei-se
2025-03-21 10:06:25 +0100krei-se(~krei-se@p3ee0faf4.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-03-21 10:08:34 +0100 <[exa]> Liamzee: yap that's a builder, not cacheable
2025-03-21 10:09:55 +0100 <[exa]> but you can cache the prebuild piece (let it evaluate to something with runHtml or so?) and then just shove it into the other html builders?
2025-03-21 10:11:54 +0100 <[exa]> basically having the global value as this should do it: memoized = toLazyByteString ...someglue... runHtmlT $ mypage
2025-03-21 10:12:30 +0100forell(~forell@user/forell) forell
2025-03-21 10:12:39 +0100 <[exa]> `someglue` should be solvable by following a typehole
2025-03-21 10:15:22 +0100dhil(~dhil@2a0c:b381:52e:3600:dd6a:fa62:e132:ec11) dhil
2025-03-21 10:16:59 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 10:21:30 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-03-21 10:26:00 +0100califax(~califax@user/califx) (Ping timeout: 264 seconds)
2025-03-21 10:26:41 +0100califax(~califax@user/califx) califx
2025-03-21 10:30:07 +0100kuribas(~user@ip-188-118-57-242.reverse.destiny.be) kuribas
2025-03-21 10:36:09 +0100lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 260 seconds)
2025-03-21 10:39:48 +0100califax(~califax@user/califx) (Ping timeout: 264 seconds)
2025-03-21 10:41:14 +0100califax(~califax@user/califx) califx
2025-03-21 10:57:47 +0100 <tomsmeding> Athas: I have few insights regarding higher-order derivatives in general, let alone with `ad`. :P
2025-03-21 10:58:12 +0100 <tomsmeding> (Assuming you mean 2nd, etc. derivatives, not "AD of code containing (higher-order) functions")
2025-03-21 10:58:19 +0100 <Athas> tomsmeding: well, I got it working (albeit with undesirable boilerplate), but now it's just remarkably slow.
2025-03-21 10:58:29 +0100 <tomsmeding> Athas: which mode did you use?
2025-03-21 10:58:43 +0100 <Athas> Forward-over-forward. And it's slower than just hacking up your own dual numbers.
2025-03-21 10:59:03 +0100 <tomsmeding> forward in `ad` is just a dual number, so that's rather surprising
2025-03-21 10:59:28 +0100 <tomsmeding> did you try Numeric.AD.Mode.Tower(.Double)? It purports to be higher-order forward derivatives
2025-03-21 10:59:46 +0100 <Athas> Well, it's not so easy - I need actual nested AD.
2025-03-21 11:00:04 +0100 <Athas> I've realised I'm not good at fast Haskell.
2025-03-21 11:00:14 +0100 <tomsmeding> few people are
2025-03-21 11:00:34 +0100 <tomsmeding> can you share your code with the manual dual numbers? I'm curious to see what beats `ad`
2025-03-21 11:01:21 +0100 <__monty__> (I'd appreciate another recap of what AD is. It's not just a way to numerically compute derivatives of numerical functions, is it? Feel free to leave the recap for when the discussion is more or less over.)
2025-03-21 11:01:31 +0100 <tomsmeding> __monty__: it is
2025-03-21 11:01:49 +0100 <tomsmeding> the problem is that you can do so efficiently for a function of type R^n -> R, or for a function of type R -> R^n
2025-03-21 11:02:09 +0100 <tomsmeding> the typical dual-numbers formulation gives you the _latter_, whereas you usually (but not always) want the former
2025-03-21 11:02:25 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 11:02:28 +0100 <tomsmeding> the former you get with reverse AD, which is more complicated
2025-03-21 11:02:35 +0100 <tomsmeding> does that help?
2025-03-21 11:04:14 +0100 <Athas> This is my code: https://github.com/gradbench/gradbench/blob/4fdb8cc00daaae42b99431fde3da7be1b1bbbc13/tools/haskell…
2025-03-21 11:04:14 +0100 <Athas> This is the ad hoc version: https://engineering.purdue.edu/~qobi/stalingrad-examples2009/particle-FF-ghc.html
2025-03-21 11:04:26 +0100 <Athas> And the dual numbers: https://engineering.purdue.edu/~qobi/stalingrad-examples2009/common-ghc.html
2025-03-21 11:04:42 +0100 <tomsmeding> ooh, DatatypeContexts
2025-03-21 11:05:13 +0100 <Athas> Yes, it is aaaalmost working Haskell.
2025-03-21 11:05:18 +0100 <Athas> There are also n+k patterns.
2025-03-21 11:05:24 +0100 <Athas> But it is easy to fix.
2025-03-21 11:05:31 +0100 <tomsmeding> that will likely be faster if you `data Bundle = Bundle {-# UNPACK #-} !Double {-# UNPACK #-} !Double`
2025-03-21 11:05:41 +0100 <tomsmeding> but let me read
2025-03-21 11:05:42 +0100 <Athas> Sure, but it is already faster than 'ad'.
2025-03-21 11:05:45 +0100 <tomsmeding> lol
2025-03-21 11:06:10 +0100 <tomsmeding> 'ad' with Forward over Forward, or Forward over ForwardDouble?
2025-03-21 11:06:15 +0100 <Athas> Forward over Forward.
2025-03-21 11:06:38 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 245 seconds)
2025-03-21 11:07:05 +0100 <tomsmeding> I like this blast-to-the-past Haskell style
2025-03-21 11:08:36 +0100gmg(~user@user/gehmehgeh) (Ping timeout: 264 seconds)
2025-03-21 11:10:48 +0100 <tomsmeding> Athas: I see a 'gradient' function that uses forward AD
2025-03-21 11:10:51 +0100 <tomsmeding> is that intentional?
2025-03-21 11:11:41 +0100 <Athas> tomsmeding: in which program?
2025-03-21 11:12:24 +0100 <tomsmeding> I was looking at the stalingrad example, but it seems you've implemented that with a proper reverse-mode gradient
2025-03-21 11:12:46 +0100 <Athas> I have done all variants in my 'ad' code.
2025-03-21 11:12:58 +0100 <Athas> The hand-written code only has forward-over-forward.
2025-03-21 11:13:01 +0100 <tomsmeding> oh, right
2025-03-21 11:13:08 +0100 <tomsmeding> the closest match is 'ff'?
2025-03-21 11:14:02 +0100xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 272 seconds)
2025-03-21 11:14:08 +0100 <Athas> Yes.
2025-03-21 11:14:12 +0100 <tomsmeding> the input to f is also only length 2, so doing forward mode twice has a chance of being competitive with reverse AD
2025-03-21 11:15:04 +0100 <tomsmeding> I have no clue juts from looking at the code; I would perhaps profile to see if there's anything surprising, but it's bound to produce noise here
2025-03-21 11:15:13 +0100 <Athas> Yes, forward mode is better here, but it is still slow.
2025-03-21 11:16:33 +0100 <tomsmeding> the Forward in 'ad' is a sum type with special cases for zero (not sure why?) and constants
2025-03-21 11:16:53 +0100 <tomsmeding> oh, the zero is relevant if you're doing nested AD I guess
2025-03-21 11:17:16 +0100 <tomsmeding> perhaps that just introduces busywork here? I don't know
2025-03-21 11:17:50 +0100mniip(mniip@libera/staff/mniip) (Ping timeout: 604 seconds)
2025-03-21 11:18:11 +0100 <tomsmeding> Athas: if you haven't yet, I recommend implementing 'ff' by Forward over ForwardDouble, I suspect it'll help quite a bit
2025-03-21 11:20:41 +0100 <Athas> tomsmeding: I gave it a shot yesterday, but received some type errors I couldn't figure out. Maybe I will try again.
2025-03-21 11:22:48 +0100 <ski> that `stalingrad' code looks a bit weird
2025-03-21 11:22:56 +0100 <haskellbridge> <Liamzee> [exa]: so it's the fault of the person who made the servant lib
2025-03-21 11:22:57 +0100 <haskellbridge> <Liamzee> oh well
2025-03-21 11:23:44 +0100 <Athas> ski: it's written by Scheme programmers and specifically to resemble the style of a corresponding Scheme program.
2025-03-21 11:24:15 +0100 <haskellbridge> <Liamzee> erm, not the lib, but the adapter for the lib
2025-03-21 11:24:38 +0100 <haskellbridge> <Liamzee> will probably try to figure out how to get it to cache lucid later
2025-03-21 11:24:47 +0100synchromesh(~john@2406:5a00:24cf:bb00:19d8:9179:8622:bdf3) (Quit: WeeChat 4.1.1)
2025-03-21 11:25:23 +0100 <ski> (lot of use of `let'-`in', rather than `where'. some redundant brackets (e.g. when defining some infix operators, or sometimes around function calls, or even conses). incorrect `Show' instance (ought to use `showsPrec', not `show')
2025-03-21 11:25:39 +0100 <ski> mhm
2025-03-21 11:25:56 +0100 <ski> any relation to the Stalin Scheme implementation, Athas ?
2025-03-21 11:26:09 +0100 <Athas> ski: yeah, same people.
2025-03-21 11:26:14 +0100 <ski> ah
2025-03-21 11:26:51 +0100 <Athas> This is code from a benchmark suite to demonstrate how wonderful Stalingrad (an extension of Stalin) is.
2025-03-21 11:27:20 +0100 <ski> it calls out to Scheme code, from Haskell ?
2025-03-21 11:28:04 +0100 <Athas> No, it is a bunch of implementations of the same program in various languages, followed by a performance comparison. Stalingrad is by far the fastest.
2025-03-21 11:28:29 +0100mniip(mniip@libera/staff/mniip) mniip
2025-03-21 11:28:32 +0100gmg(~user@user/gehmehgeh) gehmehgeh
2025-03-21 11:28:54 +0100 <ski> ah
2025-03-21 11:30:31 +0100 <Athas> See https://www.bcl.hamilton.ie/~qobi/ad2016-benchmarks/
2025-03-21 11:30:36 +0100 <Athas> Nice work, really!
2025-03-21 11:32:40 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.5.2)
2025-03-21 11:32:47 +0100 <ski> "Scheme->C" is a particular Scheme implementation ?
2025-03-21 11:32:53 +0100 <ski> can't recall hearing about that one, before
2025-03-21 11:34:06 +0100 <ski> yea, looks like a quite nice variety of different backend languages
2025-03-21 11:34:20 +0100 <ski> /implementations
2025-03-21 11:35:57 +0100 <ski> does any of those use source transformations ?
2025-03-21 11:36:14 +0100 <sprout> needs egel
2025-03-21 11:36:57 +0100 <ski> "three files that contain the code that is transformed zero, one, and two times" -- sounds like it, yea
2025-03-21 11:37:46 +0100 <ski> "We could not benchmark against ADIC because we were unsuccessful in getting ADIC to transform its own generated code." -- for higher derivatives ?
2025-03-21 11:39:01 +0100 <ski> "polyvariant submission" does sound like it suggests something like partial evaluation / program specialization, or related
2025-03-21 11:42:08 +0100alp(~alp@2001:861:8ca0:4940:1861:ecb2:15d3:3a1d)
2025-03-21 11:42:48 +0100AlexZenon(~alzenon@94.233.240.210) (Read error: Connection reset by peer)
2025-03-21 11:43:04 +0100AlexZenon(~alzenon@94.233.240.210)
2025-03-21 11:45:21 +0100Ekho(~Ekho@user/ekho) (Remote host closed the connection)
2025-03-21 11:47:46 +0100Fijxu(~Fijxu@user/fijxu) (Ping timeout: 248 seconds)
2025-03-21 11:48:43 +0100natto17(~natto@129.154.243.159) natto
2025-03-21 11:49:32 +0100natto(~natto@129.154.243.159) (Ping timeout: 260 seconds)
2025-03-21 11:49:32 +0100noteness(~noteness@user/noteness) (Ping timeout: 260 seconds)
2025-03-21 11:49:32 +0100Hafydd(~Hafydd@user/hafydd) (Ping timeout: 260 seconds)
2025-03-21 11:49:33 +0100noteness_(~noteness@user/noteness) nessessary129
2025-03-21 11:50:29 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 11:50:49 +0100Hafydd(~Hafydd@user/hafydd) Hafydd
2025-03-21 11:51:04 +0100Fijxu_(~Fijxu@user/fijxu) fijxu
2025-03-21 11:51:58 +0100ash3en(~Thunderbi@89.56.182.235) (Ping timeout: 252 seconds)
2025-03-21 11:54:45 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 248 seconds)
2025-03-21 12:00:19 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-03-21 12:00:46 +0100Ekho(~Ekho@user/ekho) Ekho
2025-03-21 12:06:20 +0100 <Athas> ski: yes, Scheme->C is a Scheme compiler (actually there seems to be several of that name, very confusing). I don't think any of them implement AD with source transformation.
2025-03-21 12:07:28 +0100 <Athas> ski: oh right, those Fortran things are source transformers. But they work terribly.
2025-03-21 12:07:40 +0100 <Athas> The authors actually wrote an entire paper about how none of those tools work.
2025-03-21 12:09:41 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 248 seconds)
2025-03-21 12:13:34 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds)
2025-03-21 12:15:06 +0100euleritian(~euleritia@dynamic-176-006-132-178.176.6.pool.telefonica.de)
2025-03-21 12:24:58 +0100sprotte24(~sprotte24@p200300d16f266c002dc4a2d25f2ad6fe.dip0.t-ipconnect.de)
2025-03-21 12:27:04 +0100euleritian(~euleritia@dynamic-176-006-132-178.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 12:27:22 +0100euleritian(~euleritia@95.90.214.149)
2025-03-21 12:27:48 +0100 <merijn> Athas: That sounds about right :p
2025-03-21 12:30:36 +0100xff0x(~xff0x@2405:6580:b080:900:74ac:a2fa:2f95:eb9f)
2025-03-21 12:35:00 +0100ash3en(~Thunderbi@89.56.182.235) ash3en
2025-03-21 12:35:33 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 12:40:14 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-03-21 12:43:44 +0100euleritian(~euleritia@95.90.214.149) (Ping timeout: 260 seconds)
2025-03-21 12:44:10 +0100^Dan(~xxx@89.136.142.218)
2025-03-21 12:45:16 +0100alecs(~alecs@nat16.software.imdea.org) (Quit: alecs)
2025-03-21 12:46:51 +0100lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-03-21 12:47:24 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 12:52:17 +0100^Dan(~xxx@89.136.142.218) (Remote host closed the connection)
2025-03-21 13:01:42 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-03-21 13:03:42 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 13:03:45 +0100chele(~chele@user/chele) chele
2025-03-21 13:08:44 +0100ash3en(~Thunderbi@89.56.182.235) (Quit: ash3en)
2025-03-21 13:08:53 +0100alp(~alp@2001:861:8ca0:4940:1861:ecb2:15d3:3a1d) (Ping timeout: 248 seconds)
2025-03-21 13:08:53 +0100ash3en1(~Thunderbi@89.56.182.235) ash3en
2025-03-21 13:09:46 +0100rvalue(~rvalue@user/rvalue) (Read error: Connection reset by peer)
2025-03-21 13:10:17 +0100rvalue(~rvalue@user/rvalue) rvalue
2025-03-21 13:11:17 +0100ash3en1ash3en
2025-03-21 13:17:29 +0100amir(sid22336@user/amir) (Quit: Connection closed for inactivity)
2025-03-21 13:20:37 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 13:23:18 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds)
2025-03-21 13:24:16 +0100euleritian(~euleritia@95.90.214.149)
2025-03-21 13:25:30 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 268 seconds)
2025-03-21 13:34:44 +0100kh0d(~kh0d@109.111.226.14) (Remote host closed the connection)
2025-03-21 13:35:15 +0100ash3en(~Thunderbi@89.56.182.235) (Quit: ash3en)
2025-03-21 13:35:27 +0100ash3en1(~Thunderbi@89.56.182.235) ash3en
2025-03-21 13:37:45 +0100ash3en1ash3en
2025-03-21 13:42:40 +0100kh0d(~kh0d@109.111.226.14) kh0d
2025-03-21 13:45:09 +0100loonycyborg_(loonycybor@chat.chantal.wesnoth.org) (Ping timeout: 265 seconds)
2025-03-21 13:45:46 +0100tabaqui(~tabaqui@167.71.80.236) tabaqui
2025-03-21 13:47:27 +0100loonycyborg(loonycybor@wesnoth/developer/loonycyborg) loonycyborg
2025-03-21 13:47:35 +0100hughjfchen(~hughjfche@vmi2417424.contaboserver.net) (Quit: WeeChat 4.4.3)
2025-03-21 13:47:55 +0100hughjfchen(~hughjfche@vmi2417424.contaboserver.net) hughjfchen
2025-03-21 13:48:43 +0100kh0d(~kh0d@109.111.226.14) (Ping timeout: 245 seconds)
2025-03-21 13:49:30 +0100hughjfchen(~hughjfche@vmi2417424.contaboserver.net) (Client Quit)
2025-03-21 13:50:45 +0100dolio(~dolio@130.44.140.168) dolio
2025-03-21 13:50:48 +0100hughjfchen(~hughjfche@vmi2417424.contaboserver.net) hughjfchen
2025-03-21 13:54:03 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) jespada
2025-03-21 13:54:44 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Client Quit)
2025-03-21 13:55:41 +0100ash3en(~Thunderbi@89.56.182.235) (Quit: ash3en)
2025-03-21 13:55:50 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) jespada
2025-03-21 13:55:57 +0100ash3en(~Thunderbi@89.56.182.235) ash3en
2025-03-21 13:56:41 +0100kh0d(~kh0d@109.111.226.14)
2025-03-21 14:01:20 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi)
2025-03-21 14:03:04 +0100ash3en(~Thunderbi@89.56.182.235) (Ping timeout: 260 seconds)
2025-03-21 14:04:08 +0100ash3en(~Thunderbi@89.56.182.235) ash3en
2025-03-21 14:05:42 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 14:06:26 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 248 seconds)
2025-03-21 14:10:09 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 248 seconds)
2025-03-21 14:18:22 +0100alp(~alp@2001:861:8ca0:4940:ce87:6c75:c7a9:f360)
2025-03-21 14:23:37 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi)
2025-03-21 14:29:01 +0100weary-traveler(~user@user/user363627) user363627
2025-03-21 14:30:51 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 244 seconds)
2025-03-21 14:32:49 +0100Guest84(~Guest84@14.139.38.105)
2025-03-21 14:36:19 +0100lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 260 seconds)
2025-03-21 14:42:58 +0100califax(~califax@user/califx) (Remote host closed the connection)
2025-03-21 14:43:02 +0100alp(~alp@2001:861:8ca0:4940:ce87:6c75:c7a9:f360) (Ping timeout: 272 seconds)
2025-03-21 14:43:14 +0100califax(~califax@user/califx) califx
2025-03-21 14:44:46 +0100L29Ah(~L29Ah@wikipedia/L29Ah) ()
2025-03-21 14:45:41 +0100wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-03-21 14:45:44 +0100Guest84(~Guest84@14.139.38.105) (Quit: Client closed)
2025-03-21 14:50:45 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 14:52:00 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer)
2025-03-21 14:55:34 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-03-21 14:56:06 +0100sabathan(~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr)
2025-03-21 15:03:51 +0100poscat(~poscat@user/poscat) (Quit: Bye)
2025-03-21 15:11:22 +0100Digitteknohippie(~user@user/digit) Digit
2025-03-21 15:11:40 +0100Digit(~user@user/digit) (Ping timeout: 244 seconds)
2025-03-21 15:11:50 +0100Sgeo(~Sgeo@user/sgeo) Sgeo
2025-03-21 15:12:36 +0100lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-03-21 15:15:26 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi)
2025-03-21 15:17:20 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-03-21 15:20:16 +0100poscat(~poscat@user/poscat) poscat
2025-03-21 15:21:02 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 272 seconds)
2025-03-21 15:24:03 +0100kh0d(~kh0d@109.111.226.14) (Remote host closed the connection)
2025-03-21 15:26:37 +0100kh0d(~kh0d@109.111.226.14)
2025-03-21 15:31:13 +0100kh0d(~kh0d@109.111.226.14) (Ping timeout: 245 seconds)
2025-03-21 15:31:14 +0100adamCS(~adamCS@pool-100-33-104-162.nycmny.fios.verizon.net) (Ping timeout: 252 seconds)
2025-03-21 15:31:14 +0100doyougnu-(~doyougnu@syn-045-046-170-068.res.spectrum.com) (Ping timeout: 252 seconds)
2025-03-21 15:31:23 +0100adamCS(~adamCS@pool-100-33-104-162.nycmny.fios.verizon.net) adamCS
2025-03-21 15:32:48 +0100vanishingideal(~vanishing@user/vanishingideal) (Ping timeout: 246 seconds)
2025-03-21 15:33:16 +0100doyougnu(~doyougnu@syn-045-046-170-068.res.spectrum.com)
2025-03-21 15:33:40 +0100DigitteknohippieDigit
2025-03-21 15:35:33 +0100noteness_(~noteness@user/noteness) (Ping timeout: 248 seconds)
2025-03-21 15:35:50 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 15:36:39 +0100CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 252 seconds)
2025-03-21 15:37:51 +0100noteness(~noteness@user/noteness) nessessary129
2025-03-21 15:38:17 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Quit: My Mac has gone to sleep. ZZZzzz…)
2025-03-21 15:40:29 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-03-21 15:46:35 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) jespada
2025-03-21 15:49:02 +0100myme(~myme@2a01:799:d5e:5f00:69c6:1b0c:ff6d:bdea) myme
2025-03-21 15:49:15 +0100Buliarou1(~gypsydang@46.232.210.139) Buliarous
2025-03-21 15:49:51 +0100kh0d(~kh0d@109.111.226.14) kh0d
2025-03-21 15:50:06 +0100as__(~as@2800:a4:396:c900:c2ca:9624:369a:7d24)
2025-03-21 15:51:04 +0100SlackCoder(~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder
2025-03-21 15:52:53 +0100euleritian(~euleritia@95.90.214.149) (Read error: Connection reset by peer)
2025-03-21 15:54:42 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de)
2025-03-21 15:57:03 +0100ft(~ft@p508db463.dip0.t-ipconnect.de) ft
2025-03-21 15:58:04 +0100JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-03-21 15:59:01 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 15:59:19 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 16:02:14 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-03-21 16:02:16 +0100notdabs(~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4)
2025-03-21 16:02:24 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 16:06:48 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-03-21 16:07:07 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de)
2025-03-21 16:07:58 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 16:08:17 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de)
2025-03-21 16:11:49 +0100as__(~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 244 seconds)
2025-03-21 16:12:25 +0100as___(~as@2800:a4:396:c900:c2ca:9624:369a:7d24)
2025-03-21 16:14:20 +0100berzerk(~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24)
2025-03-21 16:15:06 +0100bsima(~bsima@143.198.118.179) (Quit: ZNC 1.8.2 - https://znc.in)
2025-03-21 16:15:31 +0100bsima(~bsima@143.198.118.179) bsima
2025-03-21 16:16:48 +0100robobub(uid248673@id-248673.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
2025-03-21 16:16:55 +0100 <absence> When using a constraint called Subset, which takes two type-level lists, I find myself having to use "Subset (x : list1) (x : list2) => ..." instead of just "Subset list1 list2". Is there a way to convince the type checker that the x is superfluous?
2025-03-21 16:17:53 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi)
2025-03-21 16:18:44 +0100 <tomsmeding> absence: I have a feeling that this is an X-Y problem, and that the answer is a common-ish trick that I don't know a name for: define an associated type family to your class where the right-hand sides are precisely the instance contexts, then add that type family as a _superclass_ constraint to the class
2025-03-21 16:19:26 +0100 <tomsmeding> that allows ghc to, given an `instance C A => C T` not only infer `C T` from `C A`, but furthermore conclude from evidence of `C T` that `C A` must also hold
2025-03-21 16:19:35 +0100 <tomsmeding> the latter is normally _not_ what GHC does
2025-03-21 16:19:58 +0100 <tomsmeding> if you don't know what I'm talking about, or don't know how it applies to your case, you'll have to share the definition of that Subset thing
2025-03-21 16:20:11 +0100 <absence> Can I do that if the constraint and the function that needs it are defined in a third-party library?
2025-03-21 16:20:29 +0100 <tomsmeding> no
2025-03-21 16:20:33 +0100 <tomsmeding> you have to modify the class
2025-03-21 16:20:50 +0100 <tomsmeding> I'm not 100% sure this is what you are running into, but it has a similar "vibe" :p
2025-03-21 16:20:54 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 16:21:17 +0100 <absence> Here's the constraint by the way: https://hackage.haskell.org/package/effectful-core-2.5.1.0/docs/src/Effectful.Internal.Effect.html…
2025-03-21 16:21:38 +0100taktoa[c](sid282096@id-282096.tinside.irccloud.com) (Ping timeout: 244 seconds)
2025-03-21 16:22:45 +0100 <tomsmeding> ah, so `Subset list1 list2 => Subset (x : list1) (x : list2)` itself isn't even directly derivable
2025-03-21 16:22:57 +0100taktoa[c](sid282096@id-282096.tinside.irccloud.com) taktoa[c]
2025-03-21 16:23:29 +0100 <absence> Speaking of vibes, it feels vaguely similar to "(Monad (t m), Monad m, MonadTrans t) =>", so maybe something something QuantifiedConstraints...?
2025-03-21 16:23:42 +0100jackdk(sid373013@cssa/jackdk) (Ping timeout: 244 seconds)
2025-03-21 16:23:43 +0100aristid(sid1599@id-1599.uxbridge.irccloud.com) (Ping timeout: 268 seconds)
2025-03-21 16:24:29 +0100 <int-e> Looks like Subset (x : list1) (x : list2) should simplify to Subset list1 (x : list2), but there's nothing that ensures that list1 doesn't contain another x...
2025-03-21 16:24:37 +0100 <tomsmeding> absence: Note that `Subset (x : list1) (x : list2)` is NOT equivalent to `Subset list1 list2`: the former allows elements of list1 to be equal to x, whereas the latter only allows that if x is in list2
2025-03-21 16:24:44 +0100 <tomsmeding> that
2025-03-21 16:25:08 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-03-21 16:25:56 +0100jackdk(sid373013@cssa/jackdk) jackdk
2025-03-21 16:26:47 +0100aristid(sid1599@id-1599.uxbridge.irccloud.com)
2025-03-21 16:28:31 +0100berzerk(~berzerk@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds)
2025-03-21 16:30:27 +0100as___(~as@2800:a4:396:c900:c2ca:9624:369a:7d24) (Ping timeout: 265 seconds)
2025-03-21 16:31:12 +0100 <absence> I'm not sure I see how adding an x to both of them breaks the subset relationship...
2025-03-21 16:31:36 +0100 <tomsmeding> absence: sure, Subset a b implies Subset (x:a) (x:b). But the other way round does not hold
2025-03-21 16:32:01 +0100 <tomsmeding> [1,1] is a subset of [1,2], but [1] is not a subset of [2]
2025-03-21 16:32:49 +0100 <absence> Oh right, that makes sense.
2025-03-21 16:33:18 +0100 <tomsmeding> Now, even the implication `Subset a b => Subset (x:a) (x:b)` is not directly inferrable from the given instances, but you could prove it perhaps, given singletons for those lists
2025-03-21 16:33:35 +0100 <EvanR> x = x ?
2025-03-21 16:33:54 +0100 <tomsmeding> > x == x
2025-03-21 16:33:55 +0100 <lambdabot> True
2025-03-21 16:33:57 +0100 <tomsmeding> seems so
2025-03-21 16:33:58 +0100 <EvanR> oh was reading : as "type off"
2025-03-21 16:34:00 +0100 <EvanR> er
2025-03-21 16:34:04 +0100 <EvanR> type O
2025-03-21 16:34:24 +0100 <tomsmeding> we're in #haskell, not in #agda ;)
2025-03-21 16:36:10 +0100 <absence> Proving things with singletons sounds like it will quickly escalate into "not worth it". :p
2025-03-21 16:37:14 +0100 <tomsmeding> also not particularly efficient.
2025-03-21 16:37:28 +0100 <EvanR> was just reading about "presets" which are setoids (a set that comes equipped with an equivalence relation) without the equivalence relation provided. And then it explained "a preset becomes a set if you give it a relation which.... is reflexive (x = x)"
2025-03-21 16:38:11 +0100 <EvanR> xD
2025-03-21 16:38:41 +0100 <EvanR> (and other properties but, they also involve "=")
2025-03-21 16:40:22 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 268 seconds)
2025-03-21 16:41:13 +0100L29Ah(~L29Ah@wikipedia/L29Ah) ()
2025-03-21 16:41:51 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) (Quit: My Mac has gone to sleep. ZZZzzz…)
2025-03-21 16:42:54 +0100 <EvanR> ok I got confused, = is the relation being defined
2025-03-21 16:43:13 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 16:43:39 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 16:45:40 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi)
2025-03-21 16:50:04 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-03-21 16:50:26 +0100wildsalander(~wildsalan@81-175-155-97.bb.dnainternet.fi) (Ping timeout: 252 seconds)
2025-03-21 16:50:52 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de)
2025-03-21 16:51:18 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-03-21 16:55:39 +0100vpan(~vpan@212.117.1.172)
2025-03-21 17:00:29 +0100 <roconnor> EvanR: PERs: Partial Equivalence Relations
2025-03-21 17:01:17 +0100 <EvanR> yes?
2025-03-21 17:03:14 +0100 <roconnor> Oh I misunderstood what your presets were.
2025-03-21 17:03:29 +0100 <roconnor> I though they were setoids without reflexivity.
2025-03-21 17:04:31 +0100 <EvanR> I actually veered off, the presets are "sets" without equality among the elements
2025-03-21 17:04:57 +0100 <EvanR> (yet)
2025-03-21 17:05:51 +0100 <EvanR> so x doesn't equal x because equal doesn't exist
2025-03-21 17:06:58 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 17:07:55 +0100euleritian(~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Ping timeout: 244 seconds)
2025-03-21 17:07:55 +0100Square(~Square@user/square) Square
2025-03-21 17:11:20 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 252 seconds)
2025-03-21 17:23:03 +0100notdabs(~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) (Remote host closed the connection)
2025-03-21 17:23:06 +0100 <haskellbridge> <Bowuigi> How are those useful? I mean, order dependency is nice but do they make something more elegant?
2025-03-21 17:23:25 +0100notdabs(~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4)
2025-03-21 17:24:58 +0100 <haskellbridge> <Bowuigi> Quotients become central in proofs, that's nice
2025-03-21 17:26:29 +0100acidjnk(~acidjnk@p200300d6e71c4f937555fc5a67c80b19.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-03-21 17:27:09 +0100euleritian(~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de)
2025-03-21 17:27:37 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac
2025-03-21 17:28:33 +0100lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Client Quit)
2025-03-21 17:29:23 +0100 <EvanR> something about foundations https://ncatlab.org/nlab/show/preset
2025-03-21 17:30:05 +0100 <EvanR> it was the 60s, so maybe they were tripping AF
2025-03-21 17:31:49 +0100 <EvanR> also you could attempt to construe haskell's datatypes as presets because not all of them have a way to, at least decidably, know two values are equal
2025-03-21 17:32:20 +0100 <EvanR> either because there's no Eq instance or because more serious issues
2025-03-21 17:33:10 +0100 <haskellbridge> <Bowuigi> The concept of prefunction seems useful
2025-03-21 17:33:58 +0100 <EvanR> yes we have functions between types that might not agree with one or more notions of equality we have in mind on the domains
2025-03-21 17:34:03 +0100 <haskellbridge> <Bowuigi> Being able to ignore equality means that you can inspect the internal structure of something without that being in "normal form"
2025-03-21 17:35:25 +0100 <EvanR> or you could talk about, however you did it, any function you manage to define automatically preserves (a) notion of equality
2025-03-21 17:35:41 +0100 <EvanR> which we might take for granted and otherwise never had language for
2025-03-21 17:36:30 +0100 <EvanR> (automatically preserves equality, perhaps without using normal forms)
2025-03-21 17:36:42 +0100 <haskellbridge> <Bowuigi> That's usually called congruence I think
2025-03-21 17:37:58 +0100 <EvanR> sounds like a luxury to be able to pick a "real" equality relation so you can call other mappings congruence
2025-03-21 17:38:10 +0100 <EvanR> or homomorphism
2025-03-21 17:43:58 +0100chele(~chele@user/chele) (Remote host closed the connection)
2025-03-21 17:45:23 +0100machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-03-21 17:48:56 +0100vpan(~vpan@212.117.1.172) (Quit: Leaving.)
2025-03-21 17:49:50 +0100Square(~Square@user/square) (Ping timeout: 252 seconds)
2025-03-21 17:50:19 +0100L29Ah(~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer)
2025-03-21 17:52:42 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 17:56:34 +0100j1n37(~j1n37@user/j1n37) j1n37
2025-03-21 17:56:59 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 260 seconds)
2025-03-21 17:57:27 +0100j1n37-(~j1n37@user/j1n37) (Ping timeout: 268 seconds)
2025-03-21 18:10:09 +0100econo_(uid147250@id-147250.tinside.irccloud.com)
2025-03-21 18:11:14 +0100euleritian(~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 18:11:33 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de)
2025-03-21 18:11:36 +0100kuribas(~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection)
2025-03-21 18:12:31 +0100chiselfu1echiselfuse
2025-03-21 18:16:30 +0100euleritian(~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds)
2025-03-21 18:16:52 +0100euleritian(~euleritia@95.90.214.149)
2025-03-21 18:17:25 +0100tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2025-03-21 18:20:59 +0100euleritian(~euleritia@95.90.214.149) (Ping timeout: 252 seconds)
2025-03-21 18:21:55 +0100euleritian(~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de)
2025-03-21 18:24:29 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2025-03-21 18:25:41 +0100L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-03-21 18:26:44 +0100wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2025-03-21 18:27:28 +0100 <EvanR> so we can go from, imperative language with "functions" doesn't have real functions because they do side effects, or depend on invisible state, etc. to functional language with "functions" futhermore doesn't have functions because it doesn't preserve the equality xD
2025-03-21 18:27:34 +0100 <EvanR> no true function
2025-03-21 18:32:56 +0100JuanDaugherty(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-03-21 18:37:44 +0100jespada(~jespada@2800:a4:228e:4800:8c77:166d:4542:2a56) jespada
2025-03-21 18:38:46 +0100alfiee(~alfiee@user/alfiee) alfiee
2025-03-21 18:41:16 +0100 <__monty__> I'm not sure that's entirely rigorous. Nowhere do the definitions require that the notion of equality is part of the language of the functions, right?
2025-03-21 18:43:12 +0100alfiee(~alfiee@user/alfiee) (Ping timeout: 244 seconds)
2025-03-21 18:43:26 +0100 <c_wraith> No, though if you're strictly in math... If the objects in the pairs that make up a formal function can be compared for equality, then functions are equal if they contain the same set of pairs.
2025-03-21 18:43:41 +0100 <c_wraith> It gets much harder when you want equality to be computable
2025-03-21 18:43:59 +0100euleritian(~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) (Read error: Connection reset by peer)
2025-03-21 18:44:03 +0100 <EvanR> if x = y then f(x) = f(y) can be
2025-03-21 18:44:22 +0100 <EvanR> derived from the usual definition of functions in set theory