Logs on 2025-01-28 (liberachat/#haskell)
| 00:00:54 | → | cheater_ joins (~Username@user/cheater) |
| 00:03:01 | × | cheater quits (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 00:03:10 | cheater_ | is now known as cheater |
| 00:07:10 | → | talismanick joins (~user@2601:644:937c:ed10::ae5) |
| 00:07:53 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:08:50 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 00:12:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:16:12 | → | jumper joins (~pcx180e@131.216.14.87) |
| 00:18:22 | → | alfiee joins (~alfiee@user/alfiee) |
| 00:21:38 | × | xff0x quits (~xff0x@2405:6580:b080:900:ee1a:7699:189f:a423) (Ping timeout: 245 seconds) |
| 00:22:49 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 00:23:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:23:41 | × | anpad quits (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 00:26:31 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) |
| 00:28:14 | × | acidjnk_new quits (~acidjnk@p200300d6e7283f58f85d99c5648cf6f8.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 00:28:19 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 00:28:48 | × | califax quits (~califax@user/califx) (Quit: ZNC 1.8.2 - https://znc.in) |
| 00:29:10 | → | califax joins (~califax@user/califx) |
| 00:29:24 | × | malte quits (~malte@mal.tc) (Ping timeout: 260 seconds) |
| 00:30:22 | → | malte joins (~malte@mal.tc) |
| 00:39:13 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:44:08 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 00:45:11 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 00:46:44 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 00:49:48 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 00:51:42 | → | anpad joins (~pandeyan@user/anpad) |
| 00:54:39 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:05:10 | × | sprotte24 quits (~sprotte24@p200300d16f2a5f00a9408391bb436145.dip0.t-ipconnect.de) (Quit: Leaving) |
| 01:05:19 | × | jumper quits (~pcx180e@131.216.14.87) (Quit: WeeChat 4.5.1) |
| 01:05:35 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:07:05 | → | alfiee joins (~alfiee@user/alfiee) |
| 01:10:49 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 01:11:24 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 01:13:33 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 01:19:37 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 01:20:27 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 01:21:22 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:22:57 | × | otto_s quits (~user@p5b044aa1.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 01:24:07 | × | Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 01:24:20 | → | otto_s joins (~user@p4ff270b9.dip0.t-ipconnect.de) |
| 01:25:19 | → | Guest40 joins (~Guest40@2a04:cec0:100f:ae5c:92e8:68ff:fe40:e023) |
| 01:25:25 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 01:25:44 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 01:25:59 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 01:36:49 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:37:11 | → | jumper joins (~pcx180e@131.216.14.87) |
| 01:37:58 | × | malte quits (~malte@mal.tc) (Read error: Connection reset by peer) |
| 01:38:23 | → | teesquare_ joins (~teesquare@user/teesquare) |
| 01:39:24 | × | euouae quits (~euouae@user/euouae) (Ping timeout: 260 seconds) |
| 01:39:29 | × | teesquare quits (~teesquare@user/teesquare) (Ping timeout: 252 seconds) |
| 01:40:34 | × | alx741 quits (~alx741@186.33.188.229) (Ping timeout: 252 seconds) |
| 01:42:30 | × | jumper quits (~pcx180e@131.216.14.87) (Quit: WeeChat 4.5.1) |
| 01:43:30 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 01:47:10 | → | malte joins (~malte@mal.tc) |
| 01:54:53 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 01:55:48 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 01:56:10 | → | alfiee joins (~alfiee@user/alfiee) |
| 01:58:40 | → | euouae joins (~euouae@user/euouae) |
| 02:00:06 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 02:00:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 02:00:39 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 02:03:03 | → | JuanDaugherty joins (~juan@user/JuanDaugherty) |
| 02:10:38 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:15:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:21:16 | × | Square2 quits (~Square4@user/square) (Ping timeout: 252 seconds) |
| 02:21:50 | → | tavare joins (~tavare@user/tavare) |
| 02:26:25 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:27:53 | × | tabaqui1 quits (~root@87.200.129.102) (Ping timeout: 245 seconds) |
| 02:30:25 | × | notzmv quits (~umar@user/notzmv) (Remote host closed the connection) |
| 02:31:19 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 02:32:05 | → | internatetional joins (~internate@2001:448a:20a3:c2e5:1c8c:35b1:e1f9:b138) |
| 02:35:59 | × | euouae quits (~euouae@user/euouae) (Ping timeout: 260 seconds) |
| 02:42:12 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:45:15 | → | alfiee joins (~alfiee@user/alfiee) |
| 02:47:13 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 02:48:21 | → | euouae joins (~euouae@user/euouae) |
| 02:49:30 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 02:53:25 | × | Guest40 quits (~Guest40@2a04:cec0:100f:ae5c:92e8:68ff:fe40:e023) (Quit: Client closed) |
| 02:56:35 | × | internatetional quits (~internate@2001:448a:20a3:c2e5:1c8c:35b1:e1f9:b138) (Quit: Leaving) |
| 02:57:59 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 02:59:49 | → | Guest93 joins (~Guest93@syn-074-076-186-205.res.spectrum.com) |
| 03:03:24 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 03:07:20 | → | AvengingFemme joins (~avengingf@syn-074-076-186-205.res.spectrum.com) |
| 03:07:40 | × | Guest93 quits (~Guest93@syn-074-076-186-205.res.spectrum.com) (Quit: Client closed) |
| 03:12:51 | × | AvengingFemme quits (~avengingf@syn-074-076-186-205.res.spectrum.com) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 03:13:46 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:19:09 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 03:27:53 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:32:46 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 03:34:18 | → | alfiee joins (~alfiee@user/alfiee) |
| 03:37:32 | → | notzmv joins (~umar@user/notzmv) |
| 03:38:59 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 03:43:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 03:46:15 | → | ensyde joins (~ensyde@2601:5c6:c200:6dc0::3cb6) |
| 03:48:54 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 03:50:38 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 03:58:52 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 03:59:28 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:00:13 | × | JuanDaugherty quits (~juan@user/JuanDaugherty) (Read error: Connection reset by peer) |
| 04:00:30 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 04:00:37 | × | alp_ quits (~alp@2001:861:8ca0:4940:3dda:cd0f:afd0:a6c6) (Ping timeout: 252 seconds) |
| 04:04:05 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 04:15:14 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:22:09 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 04:22:33 | × | ensyde quits (~ensyde@2601:5c6:c200:6dc0::3cb6) (Ping timeout: 252 seconds) |
| 04:23:23 | → | alfiee joins (~alfiee@user/alfiee) |
| 04:27:45 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 04:33:17 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:38:29 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 04:40:06 | → | weary-traveler joins (~user@user/user363627) |
| 04:45:18 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:49:05 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 04:51:36 | → | lythienne joins (~lythieme@user/lythienne) |
| 04:54:13 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 04:57:40 | × | lythienne quits (~lythieme@user/lythienne) (Ping timeout: 240 seconds) |
| 05:04:52 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:06:50 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 05:07:17 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 05:08:47 | → | lythieme joins (~lythieme@c-24-6-125-113.hsd1.ca.comcast.net) |
| 05:09:56 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:12:46 | → | alfiee joins (~alfiee@user/alfiee) |
| 05:17:34 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 05:19:11 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 05:19:37 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 05:28:53 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:34:04 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 05:37:55 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 05:37:55 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 05:38:08 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 05:38:37 | → | gmg joins (~user@user/gehmehgeh) |
| 05:39:42 | → | michalz joins (~michalz@185.246.207.193) |
| 05:41:55 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 05:44:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 05:49:32 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 05:59:47 | × | euouae quits (~euouae@user/euouae) () |
| 06:00:26 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:01:11 | → | alfiee joins (~alfiee@user/alfiee) |
| 06:05:24 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 06:05:59 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 06:12:23 | × | echoreply quits (~echoreply@45.32.163.16) (Quit: WeeChat 2.8) |
| 06:13:18 | → | echoreply joins (~echoreply@45.32.163.16) |
| 06:16:16 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:17:12 | → | alp_ joins (~alp@2001:861:8ca0:4940:7256:930c:e9bd:85d0) |
| 06:18:14 | → | takuan joins (~takuan@d8D86B601.access.telenet.be) |
| 06:21:06 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 06:24:13 | × | ft quits (~ft@p3e9bcd97.dip0.t-ipconnect.de) (Quit: leaving) |
| 06:25:22 | × | anpad quits (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 06:26:14 | → | anpad joins (~pandeyan@user/anpad) |
| 06:28:43 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 06:29:43 | → | euleritian joins (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) |
| 06:29:52 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:34:38 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 06:37:38 | × | hgolden_ quits (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Remote host closed the connection) |
| 06:40:19 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 06:40:22 | → | hgolden joins (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) |
| 06:40:43 | → | ColinRobinson joins (~juan@user/JuanDaugherty) |
| 06:45:41 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 06:49:56 | → | alfiee joins (~alfiee@user/alfiee) |
| 06:50:30 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 06:54:13 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 06:56:23 | → | hawer joins (~newyear@2.219.56.221) |
| 06:58:59 | → | fp joins (~Thunderbi@87-94-148-3.rev.dnainternet.fi) |
| 07:01:28 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:07:53 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 07:09:30 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 07:10:01 | → | rvalue joins (~rvalue@user/rvalue) |
| 07:10:53 | → | CiaoSen joins (~Jura@2a05:5800:238:6500:ca4b:d6ff:fec1:99da) |
| 07:11:07 | × | tomboy64 quits (~tomboy64@user/tomboy64) (Ping timeout: 244 seconds) |
| 07:12:27 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) |
| 07:15:01 | → | tomboy64 joins (~tomboy64@user/tomboy64) |
| 07:19:30 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:20:21 | × | fp quits (~Thunderbi@87-94-148-3.rev.dnainternet.fi) (Ping timeout: 248 seconds) |
| 07:21:12 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 07:21:51 | → | sawilagar joins (~sawilagar@user/sawilagar) |
| 07:22:27 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 07:24:44 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 07:30:53 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:35:51 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 07:38:39 | → | alfiee joins (~alfiee@user/alfiee) |
| 07:39:19 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 07:40:43 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 07:43:02 | → | Digitteknohippie joins (~user@user/digit) |
| 07:43:24 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 07:43:53 | × | Digit quits (~user@user/digit) (Ping timeout: 244 seconds) |
| 07:46:40 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 07:49:53 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 07:51:20 | × | euleritian quits (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 07:51:34 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 07:51:37 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 07:53:59 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 08:00:00 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 08:00:41 | → | caconym joins (~caconym@user/caconym) |
| 08:02:26 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:06:56 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 08:07:13 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 08:08:20 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 08:18:13 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 08:18:23 | → | ash3en joins (~Thunderbi@2a02:8108:2810:ab00::4c86) |
| 08:23:39 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 08:24:41 | × | gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 08:27:12 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 08:27:24 | → | alfiee joins (~alfiee@user/alfiee) |
| 08:30:45 | → | gentauro joins (~gentauro@user/gentauro) |
| 08:30:50 | → | monochrm joins (trebla@216.138.220.146) |
| 08:31:10 | × | monochrom quits (trebla@216.138.220.146) (Ping timeout: 272 seconds) |
| 08:31:13 | monochrm | is now known as monochrom |
| 08:31:35 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 08:33:12 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 08:34:58 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 08:37:08 | → | monochrm joins (trebla@216.138.220.146) |
| 08:37:55 | × | monochrom quits (trebla@216.138.220.146) (Ping timeout: 244 seconds) |
| 08:37:55 | monochrm | is now known as monochrom |
| 08:41:20 | → | chele joins (~chele@user/chele) |
| 08:43:30 | × | notzmv quits (~umar@user/notzmv) (Read error: Connection reset by peer) |
| 08:44:41 | × | smalltalkman quits (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 08:55:05 | Digitteknohippie | is now known as Digit |
| 08:55:09 | <dminuoso> | sm: Neither megaparsec nor flatparse have good documentation. The former is too overwhelming and not intuitive, and the latter has too little.o |
| 08:55:29 | <dminuoso> | But in the domain of parser generators and libraries that seems to fit well within the norm. |
| 08:55:39 | → | tnt1 joins (~Thunderbi@user/tnt1) |
| 08:56:47 | → | sarna joins (~sarna@d224-221.icpnet.pl) |
| 09:01:13 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 09:01:18 | → | merijn joins (~merijn@77.242.116.146) |
| 09:06:11 | <sarna> | hi, how do you guys separate IO from the business logic in your programs? I have a program that fetches a list of stuff, and then for each thing does some processing, and if some condition is true, does more IO to get more details about that thing. separating the initial IO is easy, but how do you factor out that other part that's more "deep in the guts" of the program? |
| 09:06:41 | <sarna> | (the thing I'm working on it's not in haskell, but I figured y'all would have lots of experience with this) |
| 09:07:55 | × | tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 09:09:16 | <merijn> | sarna: In Haskell i'd probably rewrite that into something like conduit |
| 09:09:43 | <merijn> | But whether that's relevant depends on whatever language you have having something equivalent of conduit :p |
| 09:09:56 | <ColinRobinson> | why would we care in some arbitrary lang, that doesn have the propoerties hs labors to have? |
| 09:10:52 | <ColinRobinson> | also hs only seperates application logic into its pure form |
| 09:11:56 | <ColinRobinson> | it doesn exempt or somehow make that logic invioable in the cointingencies of the real world in the way u seem to be seeking |
| 09:12:03 | <sarna> | merijn: thanks, I'll read about it! looks promising so far |
| 09:12:43 | <sarna> | ColinRobinson: are you draining me right now? |
| 09:13:20 | <ColinRobinson> | sorta, this is my factitious persona and normies find that super draining |
| 09:13:40 | <sarna> | I'm working in a dynamically typed language, but I want to separate IO out mainly for better/simpler testing |
| 09:14:31 | <haskellbridge> | <magic_rb> in a dynamically typed language, mocks are common place i feel like. Essentially passing around fake instances of certain classes |
| 09:14:46 | <haskellbridge> | <magic_rb> at least thats how people do it in python, dunno about lisps for example |
| 09:15:04 | → | fp joins (~Thunderbi@cib5.wlan.kyla.fi) |
| 09:16:29 | <ColinRobinson> | iisp is the other kind of FP, the original one in fact but seperation of concerns, layers, etc that's pretty elementary stuff even if some ppl make a career outta it |
| 09:16:36 | <sarna> | I know, but I don't want to mock stuff. and not all dynamic lang ppl love mocks (see Gary Bernhardt) |
| 09:17:09 | → | alfiee joins (~alfiee@user/alfiee) |
| 09:17:22 | <ColinRobinson> | generally in lisp i'm not concerned to separate io into some hermetic cell or whatever |
| 09:17:55 | <ColinRobinson> | but if i were then id do a seperation of classes or generic functions |
| 09:19:16 | × | fp quits (~Thunderbi@cib5.wlan.kyla.fi) (Ping timeout: 252 seconds) |
| 09:21:44 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 09:21:45 | <merijn> | sarna: tbh, in most dynamically typed languages it's rather hard to stop IO from intermingling with business logic |
| 09:24:11 | <sarna> | merijn: well yeah there's no type system to enforce that, but it's not inherently impossible |
| 09:25:54 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 09:26:06 | <haskellbridge> | <sm> sarna: do as much IO up front / at the outer edge as possible, before going into pure code. But if the work requires IO throughout, then that's just the nature of it, it's IO-heavy code |
| 09:26:43 | → | euleritian joins (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) |
| 09:27:03 | <haskellbridge> | <sm> you can still move the bits that don't require IO into callable pure functions |
| 09:27:13 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 09:27:41 | → | lisbeths joins (~user@2603:3023:4be:4000:216:3eff:fe17:d69d) |
| 09:29:45 | → | absence_ joins (torgeihe@hildring.pvv.ntnu.no) |
| 09:29:45 | × | absence quits (torgeihe@hildring.pvv.ntnu.no) (Read error: Connection reset by peer) |
| 09:34:14 | × | absence_ quits (torgeihe@hildring.pvv.ntnu.no) (Ping timeout: 244 seconds) |
| 09:35:14 | × | ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 09:41:35 | → | fp joins (~Thunderbi@cib5.wlan.kyla.fi) |
| 09:41:52 | → | merijn joins (~merijn@77.242.116.146) |
| 09:44:15 | <sarna> | sm: that gave me an idea - I could filter out the items I need to make additional IO for with a pure function, and then perform the IO for the resulting list |
| 09:44:38 | <sarna> | this way I have no branching/logic in the IO function and can move it to the edge |
| 09:44:40 | <sarna> | thanks! |
| 09:44:45 | <haskellbridge> | <sm> sounds good! |
| 09:45:03 | → | absence joins (torgeihe@hildring.pvv.ntnu.no) |
| 09:46:02 | × | fp quits (~Thunderbi@cib5.wlan.kyla.fi) (Ping timeout: 252 seconds) |
| 09:47:04 | × | acarrico quits (~acarrico@dhcp-209-99-192-63.greenmountainaccess.net) (Ping timeout: 260 seconds) |
| 09:47:34 | → | __monty__ joins (~toonn@user/toonn) |
| 09:49:29 | → | SlackCoder joins (~SlackCode@64-94-63-8.ip.weststar.net.ky) |
| 09:49:49 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 10:00:05 | → | acarrico joins (~acarrico@pppoe-209-99-221-107.greenmountainaccess.net) |
| 10:00:43 | → | merijn joins (~merijn@77.242.116.146) |
| 10:05:52 | → | alfiee joins (~alfiee@user/alfiee) |
| 10:10:24 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 10:10:49 | × | euleritian quits (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 10:11:07 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 10:17:28 | × | xff0x quits (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 245 seconds) |
| 10:17:54 | → | fp joins (~Thunderbi@cib5.wlan.kyla.fi) |
| 10:22:09 | × | fp quits (~Thunderbi@cib5.wlan.kyla.fi) (Ping timeout: 246 seconds) |
| 10:34:41 | × | lisbeths quits (~user@2603:3023:4be:4000:216:3eff:fe17:d69d) (Remote host closed the connection) |
| 10:41:29 | × | tavare quits (~tavare@user/tavare) (Ping timeout: 265 seconds) |
| 10:42:29 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 10:48:37 | → | merijn joins (~merijn@77.242.116.146) |
| 10:54:37 | → | alfiee joins (~alfiee@user/alfiee) |
| 10:57:33 | → | kuribas joins (~user@ip-188-118-57-242.reverse.destiny.be) |
| 10:58:45 | <kuribas> | Is this project dead? https://hackage.haskell.org/package/caledon |
| 10:59:01 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 10:59:34 | × | ash3en quits (~Thunderbi@2a02:8108:2810:ab00::4c86) (Quit: ash3en) |
| 11:01:45 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 11:01:54 | <dminuoso> | Well you can see yourself when it was last uploaded to hackage, and when the package received commits last... |
| 11:02:00 | <dminuoso> | What is it that you want to know? |
| 11:02:34 | <kuribas> | If it makes sense to invest some time in it... |
| 11:02:44 | <kuribas> | It looks like a successor of twelf. |
| 11:04:38 | <kuribas> | dminuoso: what interests me is using a dependently type languages for logic. |
| 11:06:44 | × | mange quits (~user@user/mange) (Remote host closed the connection) |
| 11:10:17 | → | xff0x joins (~xff0x@ai096095.d.east.v6connect.net) |
| 11:10:48 | → | tavare joins (~tavare@user/tavare) |
| 11:30:19 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 11:30:19 | × | lockywolf quits (~lockywolf@coconut.lockywolf.net) (Read error: Connection reset by peer) |
| 11:39:47 | → | monochrm joins (trebla@216.138.220.146) |
| 11:41:49 | × | monochrom quits (trebla@216.138.220.146) (Ping timeout: 260 seconds) |
| 11:41:49 | monochrm | is now known as monochrom |
| 11:43:01 | → | alfiee joins (~alfiee@user/alfiee) |
| 11:43:29 | → | merijn joins (~merijn@77.242.116.146) |
| 11:45:12 | → | monochrm joins (trebla@216.138.220.146) |
| 11:45:21 | → | ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:e9b3:4a8b:794e:b4a) |
| 11:46:43 | × | monochrom quits (trebla@216.138.220.146) (Ping timeout: 265 seconds) |
| 11:46:44 | monochrm | is now known as monochrom |
| 11:47:24 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 11:47:54 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 12:00:05 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 12:00:38 | → | merijn joins (~merijn@77.242.116.146) |
| 12:02:41 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 12:03:56 | → | caconym joins (~caconym@user/caconym) |
| 12:05:23 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 12:08:26 | → | rvalue- joins (~rvalue@user/rvalue) |
| 12:09:24 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 12:15:03 | rvalue- | is now known as rvalue |
| 12:17:31 | → | merijn joins (~merijn@77.242.116.146) |
| 12:22:09 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 12:25:48 | → | Guest72 joins (~Guest28@conect.gtstelecom.ro) |
| 12:27:29 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 12:32:24 | → | alfiee joins (~alfiee@user/alfiee) |
| 12:34:11 | → | merijn joins (~merijn@77.242.116.146) |
| 12:36:49 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 12:38:56 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 12:39:56 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) |
| 12:51:22 | → | merijn joins (~merijn@77.242.116.146) |
| 12:54:48 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 12:57:13 | → | ColinRobinson joins (~juan@user/JuanDaugherty) |
| 13:02:16 | → | tabaqui1 joins (~root@87.200.129.102) |
| 13:05:57 | × | yin quits (~z@user/zero) (Ping timeout: 248 seconds) |
| 13:07:11 | → | zero joins (~z@user/zero) |
| 13:10:33 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 13:11:37 | → | jespada joins (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) |
| 13:16:23 | → | alx741 joins (~alx741@186.33.188.229) |
| 13:20:38 | → | Square2 joins (~Square4@user/square) |
| 13:21:09 | → | alfiee joins (~alfiee@user/alfiee) |
| 13:25:12 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
| 13:32:38 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 13:34:24 | × | CiaoSen quits (~Jura@2a05:5800:238:6500:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 13:37:24 | → | merijn joins (~merijn@77.242.116.146) |
| 13:45:03 | → | pavonia joins (~user@user/siracusa) |
| 13:51:55 | × | terrorjack45 quits (~terrorjac@2a01:4f8:c17:a66e::) (Ping timeout: 265 seconds) |
| 13:55:27 | → | weary-traveler joins (~user@user/user363627) |
| 14:09:34 | → | alfiee joins (~alfiee@user/alfiee) |
| 14:13:43 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 14:23:14 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 14:24:08 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 14:24:32 | → | euleritian joins (~euleritia@dynamic-176-006-133-195.176.6.pool.telefonica.de) |
| 14:25:49 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 14:26:45 | × | gmg quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 14:28:06 | → | AvengingFemme joins (~avengingf@syn-074-076-186-205.res.spectrum.com) |
| 14:29:34 | → | gmg joins (~user@user/gehmehgeh) |
| 14:33:41 | × | lythieme quits (~lythieme@c-24-6-125-113.hsd1.ca.comcast.net) (Quit: Client closed) |
| 14:40:10 | <kuribas> | I want to write a formal proof (in idris), then port it to clojure. |
| 14:40:41 | <kuribas> | Hm, I might create an inductive type family in idris, create a prove, and port to minikanren in clojure (core.logic). |
| 14:41:27 | <kuribas> | That could make for an easy (almost) mechanical translation. |
| 14:41:58 | <kuribas> | But I guess I am in the wrong channel for this discussion... |
| 14:43:11 | → | terrorjack45 joins (~terrorjac@2a01:4f8:c17:a66e::) |
| 14:43:37 | <ski> | proofs in Twelf tends to consist of the system checking mode of some hand-crafted relation/predicate you've defined |
| 14:45:26 | <kuribas> | ski: but can it proof a complicated type checker? (with parametricity, rank-n types, ...) |
| 14:48:21 | <ski> | if you want to prove preservation, you'd make a predicate that relates a term `M', a type `T', a proof `D' that `M : T', another term `N', a prood `R' that `M' reduces to `N', and a proof `E' that `N : T', and then the relevant mode would state that `M',`T',`D',`N',`R' together determines `E' (`forall (M : term) (T : type) (D : of M T) (N : term) (R : red M N). exists (E : of N T). true') |
| 14:49:05 | <ski> | (and the definition of this relation would basically amount to the steps required for this proof) |
| 14:49:15 | <kuribas> | ski: I want a declarative specification of a type inference algorithm, then prove that the result is well typed. |
| 14:49:16 | × | euleritian quits (~euleritia@dynamic-176-006-133-195.176.6.pool.telefonica.de) (Ping timeout: 272 seconds) |
| 14:49:23 | <kuribas> | ski: and if possible complete (though much harder). |
| 14:49:45 | <kuribas> | like this paper: https://www.cl.cam.ac.uk/~nk480/bidir.pdf |
| 14:49:47 | <ski> | Twelf only has three levels, terms, families (types), and kinds |
| 14:51:25 | terrorjack45 | is now known as terrorjack |
| 14:52:02 | <ski> | dunno to which extent you could do stuff like rank-n. Twelf itself doesn't have type polymorphism (types can only be parameterized by terms, not other types. original implementation allowed parameterization by types as well, but there were some issues proving relevant properties in the meta-theory of this, and in the next implementation they didn't including polymorphism) (this still wouldn't preclude |
| 14:52:08 | <ski> | *encoding* polymorphism in an object language, though) |
| 14:52:54 | <ski> | mm. i don't see why one couldn't do bidirectional |
| 14:53:32 | <ski> | iirc, some of the metatheory of Olli was formalized in Twelf, including stuff related to bidirectional |
| 14:54:02 | <kuribas> | ski: Is it hard to hand craft proofs in twelf? |
| 14:54:17 | <kuribas> | Does it offer the same features as idris2/agda, like showing goals? |
| 14:54:28 | <kuribas> | And typed holes. |
| 14:54:44 | <ski> | (although, in that case, the aim was more proof search, than type inference. but there does seem to be a clear connection between uniform proofs, and stuff like neutral terms and type inference) |
| 14:55:45 | <ski> | hm, i don't recall seeing interactive development, really. there was at some point an interface to ProofGeneral, but it seem to've been dropped (not maintained, i assume). i dunno to which extent it was interactive |
| 14:56:00 | <ski> | can't recall seeing anything about holes |
| 14:56:12 | × | nschoe- quits (~nschoe@82-65-202-30.subs.proxad.net) (Ping timeout: 246 seconds) |
| 14:56:18 | → | nschoe joins (~nschoe@2a01:e0a:8e:a190:15d4:9b4c:59c3:ed22) |
| 14:56:48 | <ski> | i know you can effectively write queries, have the system solve it for you (proof search), and then name the proof, ior some of the variables of the query, to use further in your source file |
| 14:57:56 | <ski> | so you can effectively do some tactical programming, that way, asking the system to search for a proof for you, possibly by using a restricted, guided (often not complete) algorithm, that you've encoded as a custom relation |
| 14:59:18 | → | alfiee joins (~alfiee@user/alfiee) |
| 14:59:20 | × | Googulator quits (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 14:59:36 | → | Googulator joins (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 15:00:37 | <kuribas> | idris has proof search, but it's not very powerful. |
| 15:00:54 | <kuribas> | perhaps twelf does that better. |
| 15:01:01 | <ski> | not backtracking ? |
| 15:01:10 | <ski> | Twelf does backtracking |
| 15:01:17 | <kuribas> | It does. |
| 15:01:51 | <ski> | although, i think, with naming parts of a solution to a query, you get the first matching solution. so you'll likely want to restrict it so it doesn't find you one that you don't like |
| 15:02:30 | <ski> | .. i've been fantasizing a bit about what it would take to make a mode system, something akin to the one in Mercury, for Twelf (or LambdaProlog, or Lolli, or Olli) |
| 15:03:49 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 15:04:16 | <ski> | a `:- mode append(out,out,in) is multi.' mode meta-proves `forall [XsYs] at_least [Xs,Ys] append(Xs,Ys,XsYs).' |
| 15:05:03 | <ski> | s/at_least/at_least_one/ |
| 15:05:03 | <kuribas> | ski: twelf does have modes? |
| 15:05:12 | <ski> | while `:- mode append(in,out,in) is semidet.' meta-proves `forall [Xs,XsYs] at_most_one [Ys] append(Xs,Ys,XsYs).' |
| 15:05:22 | <ski> | kuribas : yes, but only rather restricted |
| 15:05:35 | <ski> | (the two examples above are from Mercury) |
| 15:06:23 | <ski> | and `:- mode append(in,in,out) is det.' meta-proves `forall [Xs,Ys] exactly_one [XsYs] append(Xs,Ys,XsYs).' |
| 15:08:00 | <ski> | in Twelf, you can have a mode declaration (something like `%mode append +Xs +Ys -XsYs.', iirc), that declares which parameters are to be considered inputs, and which are to be considered outputs. it only allows a single such declaration, per predicate / type family (which are the same thing, in Twelf), which is a bit unfortunate, from a programming (and proof search) standpoint |
| 15:08:04 | <kuribas> | ski: should I look at mercury? |
| 15:08:10 | <kuribas> | ski: but it's not dependently typed, right? |
| 15:08:53 | <ski> | it also does not do goal reordering to satisfy the input & output constraints (which Mercury does do .. has to do, basically, in order for the multiple allowed mode declarations on a predicate to be useful) |
| 15:09:48 | × | AvengingFemme quits (~avengingf@syn-074-076-186-205.res.spectrum.com) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 15:09:52 | <ski> | and Twelf doesn't prove existence of outputs. but there's a separate declaration for that, doing something similar to the `is multi' for Mercury (nothing that does `is det' (unique solution) or `is semidet' (at most one solution), iirc) |
| 15:10:28 | <ski> | Mercury is highly interesting, i'd say, yes. not so much from a type theory perspective, though. but from a logic programming one |
| 15:12:16 | <ski> | and yea, it's not dependently typed. it does have algebraic types, parameterized types, parametric polymorphism (although doesn't enjoy parametricity, you can effectively do "type case"), also has existentials in base language. doesn't have higher-order types (type variables can only be concrete), though. does have type classes, including output type class constraints, on predicates |
| 15:14:24 | <kuribas> | right |
| 15:16:29 | × | SlackCoder quits (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 15:16:54 | × | Guest72 quits (~Guest28@conect.gtstelecom.ro) (Quit: Client closed) |
| 15:19:10 | <ski> | and for logic programming, it has instantiation states, mode declarations for predicates (and functions), determinisms (the `det',`semidet',`multi',`nondet', also `failure' and `erronous'), all of which can be very useful as statically checked documentation, and error-guardrails, for common logic programming issues |
| 15:19:30 | <ski> | it also has some support for constraint logic programming |
| 15:21:27 | <ski> | (otherwise, without constraints, the instantiation state of everything is known exactly (up to allowing different alternative constructors/functors), at each point in time (which greatly improves efficiency), you can't even alias logic variables (as in base Prolog) without using constraints (except for a few "definite alias" exceptions, doing LCMC/TCMC (Last/Tail Call Modulo Cons(tructor)))) |
| 15:24:00 | <ski> | hm, right. it also has determinisms `cc_multi' and `cc_nondet', which are used when there could be multiple solutions, but you don't care about computing (potentially) all of them, just one. e.g. used with existential quantification (don't care, just want to know whether it succeeded or failed), but also used for concurrency (indeterminacy of interleaving of multiprocessing), for collecting all solutions of |
| 15:24:06 | <ski> | a goal in a list (indeterminacy of ordering and duplication, can be affected by compiler optimization), and possibly also indeterminacy of sources of random data |
| 15:26:12 | <ski> | it's way of encoding quotient types is arguably also neater than the way it's done in Haskell. in Haskell, `(==)' is just another library operation, with implied (unchecked) laws that `x == y = True => x = y' and `x == y = False => x =/= y'. in Mercury, `(=)/2' is supposed to be semantic equality, used both for definitions, as well as for equality test and unification (pattern-matching as special case) |
| 15:27:18 | <ski> | in Haskell, you "just" need to make sure that none of the inessential differences of internal alternative representations of the same semantic value leak out, can be observed in the result of some of your exported library operations |
| 15:30:31 | <ski> | in Mercury, you explicitly have to attach a user-defined equality (your own predicate on the representation type, which is semantically kept distinct from the abstract type (think akin to a `newtype'). every time you match on the constructor, that match is `cc_multi' (could potentially give different representations, depending on optimizations), and to get rid of that, you need to use a |
| 15:30:37 | <ski> | `promise_equivalent_solutions' construct at the point where you believe the internal details can no longer be observed) |
| 15:31:41 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 15:31:41 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 15:31:42 | <ski> | .. hm, i also think system's programming languages (including stuff like perfect forwarding, with "rvalue references" in C++) could gainfully use some of the ideas in Mercury's instantiation system |
| 15:31:57 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 15:32:00 | → | califax_ joins (~califax@user/califx) |
| 15:32:26 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 15:32:43 | <ski> | (there's a #mercury channel (not too active), in addition to ##prolog (and #twelf is mostly deserted, it seems, used to be a few more people there)) |
| 15:33:34 | × | gmg quits (~user@user/gehmehgeh) (Killed (NickServ (Forcing logout gmg -> gehmehgeh))) |
| 15:33:34 | gehmehgeh | is now known as gmg |
| 15:33:43 | → | user_ joins (~user@user/fmira) |
| 15:34:24 | × | califax quits (~califax@user/califx) (Ping timeout: 264 seconds) |
| 15:34:24 | califax_ | is now known as califax |
| 15:35:36 | × | ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 264 seconds) |
| 15:35:36 | × | fmira quits (~user@user/fmira) (Ping timeout: 264 seconds) |
| 15:37:09 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 15:37:31 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 15:37:45 | × | mesaoptimizer quits (~mesa@user/PapuaHardyNet) (Quit: WeeChat 4.0.4) |
| 15:38:08 | → | mesaoptimizer joins (~mesa@user/PapuaHardyNet) |
| 15:39:59 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 15:40:19 | × | mesaoptimizer quits (~mesa@user/PapuaHardyNet) (Client Quit) |
| 15:40:32 | → | mesaoptimizer joins (~mesa@user/PapuaHardyNet) |
| 15:48:43 | → | alfiee joins (~alfiee@user/alfiee) |
| 15:49:55 | <kuribas> | ski: so (==) is DecEq ? |
| 15:53:03 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 15:53:52 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 15:57:05 | <ski> | in Haskell, basically yes (modulo infinite data) |
| 15:57:17 | <ski> | in Mercury, there is no `==', only `=' |
| 15:57:51 | <kuribas> | ski: in haskell (a == b) doesn't mean (a = b). |
| 15:58:20 | <kuribas> | For example HashSet (a == b) may not mean (a = b) because of internal representation differences. |
| 16:00:13 | <ski> | yes and no |
| 16:01:00 | <ski> | conceptually, the representation differences are not supposed to be considered for the semantic value (enforced by not leaking such implementation from the operations) |
| 16:02:25 | × | TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Remote host closed the connection) |
| 16:02:49 | <ski> | in Mercury, if you do `:- type set(T) ---> make_set(list(T)) where equality is set_equals.', then the data constructor `make_set' is *non-injective*. different lists are conceptually mapped to the same set. which are considered the same is up to the user-provided relation `set_equals', which ought to be an equivalence relation (not checked) |
| 16:04:06 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 16:04:20 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 16:04:30 | <ski> | and therefore, matching on `make_set(L)' can (conceptually) give multiple alternative `L's as result, for the same set. and to get away from this (comitted-choice) non-determinism, you need to use a `promise_equivalent_solutions' (a proof obligation on the part of the programm) at some point, where it doesn't matter anymore which particular representation was actually picked by the matching |
| 16:05:24 | → | euleritian joins (~euleritia@dynamic-176-006-133-249.176.6.pool.telefonica.de) |
| 16:06:01 | <ski> | Mercury better separates the representation type from the abstract (quotient) type, by the introduction of `cc_multi' determinism, and the accompanied required `promise_equivalent_solutions' to get back to deterministic code |
| 16:07:43 | <ski> | in Haskell, you fully have to rely on your own discipline to hide the representation differences (including not exporting the data constructor), and not leaking such details from exported operations. in Mercury, you also have to do that, but every situation in which you might leak representation details is flagged by `cc_multi', requiring you to insert `promise_equivalent_solutions' in the source code to get |
| 16:07:49 | <ski> | away from it |
| 16:18:16 | × | Googulator quits (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 16:18:33 | → | Googulator joins (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 16:20:37 | <ski> | (in Mercury, `make_set(L0) = make_set(L1)' does not mean `L0 = L1' .. which is what non-injectivity means) |
| 16:21:23 | → | ft joins (~ft@p3e9bcd97.dip0.t-ipconnect.de) |
| 16:23:58 | × | jespada quits (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 16:24:58 | × | euleritian quits (~euleritia@dynamic-176-006-133-249.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 16:31:14 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 16:35:53 | × | ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 16:38:26 | → | alfiee joins (~alfiee@user/alfiee) |
| 16:40:28 | <ski> | hm .. i also prefer Mercury's naming convention, for some pragmas, constructs, and functions, `promise_XXX', as opposed to `unsafeXXX' in Haskell. often it's unclear exactly what is unsafe / which would be safe, and which "degree" of safety is involved (are we talking undefined behaviour ? run-time partiality (exceptions, pattern-match failure, unexpected nontermination) ? internal invariants violated ? |
| 16:40:34 | <ski> | possible deadlock or unexpected indeterminacy ?) |
| 16:41:21 | <ski> | `promise_XXX' brings the attention more to what your proof obligations, as a programmer are, encourages expressing that in the `XXX' part |
| 16:42:33 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:42:56 | <ski> | (e.g. `unsafePerformIO' could perhaps be called `promisePureIO', here. with `promisePureIO (return x)' being equivalent to `x') |
| 16:42:59 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 16:48:27 | × | kuribas quits (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 244 seconds) |
| 16:56:21 | × | euleritian quits (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 16:57:10 | → | euleritian joins (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 17:06:21 | <haskellbridge> | <Bowuigi> ski Twelf has unique modes and a separate metatheorem prover if that's not enough |
| 17:07:11 | <haskellbridge> | <Bowuigi> I find Twelf very intuitive for proving theorems, sadly it only supports one sort so many statements have to be encoded somewhat oddly |
| 17:08:02 | <ski> | "unique modes" referring to ? |
| 17:08:23 | <haskellbridge> | <Bowuigi> Unique outputs, mainly |
| 17:08:29 | <ski> | and yea, it has some more advanced meta-stuff as well |
| 17:08:40 | <ski> | ah, right |
| 17:09:13 | <haskellbridge> | <Bowuigi> https://twelf.org/wiki/percent-unique/ |
| 17:09:22 | <ski> | i recall reading some papers about a functional programming language for meta-programming proofs over Twelf terms |
| 17:10:59 | → | jespada joins (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) |
| 17:11:49 | <haskellbridge> | <Bowuigi> The metatheorem stuff is specially interesting because it automagically proves stuff https://twelf.org/wiki/theorem-prover/ |
| 17:13:21 | × | merijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 17:13:25 | <haskellbridge> | <Bowuigi> Twelf is by far my favourite theorem prover. Is Mercury a similar alternative? Agda and friends are more cumbersome tbh |
| 17:16:35 | <ski> | "Delphin" by Adam Brett Poswolsky at <https://delphin.poswolsky.com/> |
| 17:18:00 | <ski> | Mercury is not a theorem prover. it's a logic (and functional) programming language. LambdaProlog (and Lolli, Olli) also are a bit more of programming languages, but does have nice facilities for HOAS representations, and expressing meta-algorithms |
| 17:19:02 | <ski> | (you can match under lambdas, using L-lambda unification and (limited) higher-order unification (it's necessarily incomplete, being an undecidable problem in general)) |
| 17:20:37 | <ski> | (the representation and handling of lambdas in Twelf is quite similar to that in LambdaProlog, based largely on the same ideas) |
| 17:22:53 | <ski> | (there are no built-in theorem proving facilities in LambdaProlog (unless static type checking, non-dependant, although with parameterized types and polymorphism, if you count this), and there's no mode or determinism checking either (would be useful, both from a programming standpoint, and from a theorem proving standpoint, as in Twelf)) |
| 17:24:31 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:28:55 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 17:29:16 | → | Square joins (~Square@user/square) |
| 17:29:30 | → | alfiee joins (~alfiee@user/alfiee) |
| 17:30:48 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 264 seconds) |
| 17:31:16 | × | user_ quits (~user@user/fmira) (Remote host closed the connection) |
| 17:31:25 | → | fmira joins (~user@user/fmira) |
| 17:31:49 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 17:32:33 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 17:32:45 | × | Square2 quits (~Square4@user/square) (Ping timeout: 276 seconds) |
| 17:34:19 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 17:35:28 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) |
| 17:36:02 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 17:37:49 | → | kuribas joins (~user@2a02:1808:87:ce4e:1295:6cfb:900:f8a1) |
| 17:38:01 | × | tavare quits (~tavare@user/tavare) (Remote host closed the connection) |
| 17:38:13 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:41:59 | × | philopsos quits (~caecilius@user/philopsos) (Quit: Lost terminal) |
| 17:44:50 | <ski> | mm, i see `%unique' was introduced later than the manual i read, and i forgot earlier seeing examples of it, on the wiki |
| 17:47:53 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 17:49:28 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 17:51:12 | × | end quits (~end@user/end/x-0094621) (Ping timeout: 246 seconds) |
| 17:51:54 | → | tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 17:52:05 | × | ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:e9b3:4a8b:794e:b4a) (Quit: ubert) |
| 17:52:37 | × | bcksl quits (~bcksl@user/bcksl) (Ping timeout: 265 seconds) |
| 17:53:06 | × | avidseeker quits (av@user/avidseeker) (Ping timeout: 265 seconds) |
| 17:53:15 | × | sus0 quits (zero@user/zeromomentum) (Ping timeout: 252 seconds) |
| 18:07:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:07:30 | × | kuribas quits (~user@2a02:1808:87:ce4e:1295:6cfb:900:f8a1) (Ping timeout: 244 seconds) |
| 18:12:14 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 18:13:14 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 18:13:53 | → | bcksl joins (~bcksl@user/bcksl) |
| 18:14:48 | <haskellbridge> | <Bowuigi> I see, will try Delphin later |
| 18:15:46 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 18:15:48 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 18:16:20 | → | end joins (~end@user/end/x-0094621) |
| 18:16:30 | <ski> | Delphin is extension of Elphin, which was bundled with Twelf, at one point, i think |
| 18:16:53 | <haskellbridge> | <sm> fr33domlover: ping |
| 18:16:56 | → | AvengingFemme joins (~avengingf@syn-074-076-186-205.res.spectrum.com) |
| 18:18:02 | → | acidjnk_new3 joins (~acidjnk@p200300d6e7283f203076ec74f0f78e66.dip0.t-ipconnect.de) |
| 18:18:35 | → | alfiee joins (~alfiee@user/alfiee) |
| 18:19:57 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 18:20:50 | × | simplystuart quits (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection) |
| 18:20:59 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 18:21:14 | → | simplystuart joins (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 18:22:44 | × | Lord_of_Life_ quits (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 18:23:14 | × | AvengingFemme quits (~avengingf@syn-074-076-186-205.res.spectrum.com) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 18:23:20 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 272 seconds) |
| 18:24:04 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:27:47 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 18:28:59 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 18:32:48 | → | sreaming joins (~screaming@37.48.95.216) |
| 18:33:08 | <ski> | (older page at <https://web.archive.org/web/20041218030402/http://www.cs.yale.edu/homes/delphin/>) |
| 18:34:25 | → | kuribas joins (~user@2a02:1808:87:ce4e:ed8d:3f59:612a:12d6) |
| 18:36:06 | <jle`> | hm...is there a nice `ConstM` type? `newtype ConstM w m a = CostM (m w)` |
| 18:36:39 | <jle`> | where ConstM x <> ConstM y = ConstM ((<>) <$> x <*> y) |
| 18:37:02 | <jle`> | maybe Const . Ap |
| 18:39:00 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 18:39:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:44:08 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 18:46:45 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 18:47:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 18:48:51 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 18:51:38 | gehmehgeh | is now known as gmg |
| 18:51:43 | × | vanishingideal quits (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds) |
| 18:52:04 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 18:53:14 | → | Smiles joins (uid551636@id-551636.lymington.irccloud.com) |
| 18:53:55 | → | vanishingideal joins (~vanishing@user/vanishingideal) |
| 18:55:24 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 18:58:41 | → | lol_ joins (~lol@2603:3016:1e01:b9c0:1941:93e:5ca4:6d26) |
| 18:59:31 | → | EvanR_ joins (~EvanR@user/evanr) |
| 18:59:39 | → | kuribas` joins (~user@ptr-17d51epnlr9u1hv5k0s.18120a2.ip6.access.telenet.be) |
| 19:00:24 | → | ell2 joins (~ellie@user/ellie) |
| 19:00:29 | × | edmundnoble_ quits (sid229620@id-229620.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 19:00:29 | × | albet70 quits (~xxx@2400:8905::f03c:92ff:fe60:98d8) (Ping timeout: 260 seconds) |
| 19:00:29 | × | Hobbyboy quits (Hobbyboy@hobbyboy.co.uk) (Ping timeout: 260 seconds) |
| 19:00:29 | × | coldmountain quits (sid484352@id-484352.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 19:00:29 | × | idnar quits (sid12240@debian/mithrandi) (Ping timeout: 260 seconds) |
| 19:00:51 | → | edmundnoble_ joins (sid229620@id-229620.helmsley.irccloud.com) |
| 19:01:14 | × | kuribas quits (~user@2a02:1808:87:ce4e:ed8d:3f59:612a:12d6) (Ping timeout: 260 seconds) |
| 19:01:15 | → | [dpk] joins (~dpk@jains.nonceword.org) |
| 19:01:17 | → | loonycyborg_ joins (loonycybor@chat.chantal.wesnoth.org) |
| 19:01:39 | × | aniketd quits (32aa4844cd@2a03:6000:1812:100::dcb) (Ping timeout: 260 seconds) |
| 19:01:39 | × | whereiseveryone quits (206ba86c98@2a03:6000:1812:100::2e4) (Ping timeout: 260 seconds) |
| 19:01:39 | × | probie quits (cc0b34050a@user/probie) (Ping timeout: 260 seconds) |
| 19:01:39 | × | jleightcap quits (7bc4014b62@user/jleightcap) (Ping timeout: 260 seconds) |
| 19:01:39 | × | beaky quits (~beaky@2a03:b0c0:0:1010::1e:a001) (Ping timeout: 260 seconds) |
| 19:01:39 | × | shawwwn quits (sid6132@id-6132.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 19:01:39 | × | sa1 quits (sid7690@id-7690.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 19:01:50 | → | beaky joins (~beaky@2a03:b0c0:0:1010::1e:a001) |
| 19:02:14 | × | jcarpenter2 quits (~lol@2603:3016:1e01:b9c0:f81e:e0f5:bc3d:aa5) (Ping timeout: 260 seconds) |
| 19:02:14 | × | EvanR quits (~EvanR@user/evanr) (Ping timeout: 260 seconds) |
| 19:02:14 | × | tt12310978324354 quits (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 260 seconds) |
| 19:02:14 | × | mustafa quits (sid502723@rockylinux/releng/mustafa) (Ping timeout: 260 seconds) |
| 19:02:14 | × | ZLima12 quits (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 19:02:14 | × | dpk quits (~dpk@jains.nonceword.org) (Ping timeout: 260 seconds) |
| 19:02:14 | × | loonycyborg quits (loonycybor@wesnoth/developer/loonycyborg) (Ping timeout: 260 seconds) |
| 19:02:14 | × | Pent quits (sid313808@id-313808.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 19:02:14 | × | ell quits (~ellie@user/ellie) (Ping timeout: 260 seconds) |
| 19:02:14 | × | bwe quits (~bwe@2a01:4f8:1c1c:4878::2) (Ping timeout: 260 seconds) |
| 19:02:14 | × | Hafydd quits (~Hafydd@user/hafydd) (Ping timeout: 260 seconds) |
| 19:02:15 | × | bailsman quits (~ejrietvel@revspace/participant/bailsman) (Ping timeout: 260 seconds) |
| 19:02:15 | × | integral quits (sid296274@user/integral) (Ping timeout: 260 seconds) |
| 19:02:15 | ell2 | is now known as ell |
| 19:02:49 | × | GdeVolpi1 quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 260 seconds) |
| 19:02:50 | → | Hobbyboy joins (Hobbyboy@hobbyboy.co.uk) |
| 19:02:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:03:02 | → | sprotte24 joins (~sprotte24@p200300d16f3179007dc10aa53878022c.dip0.t-ipconnect.de) |
| 19:03:13 | → | jleightcap joins (7bc4014b62@user/jleightcap) |
| 19:03:14 | → | whereiseveryone joins (206ba86c98@2a03:6000:1812:100::2e4) |
| 19:03:14 | → | aniketd joins (32aa4844cd@2a03:6000:1812:100::dcb) |
| 19:03:20 | → | probie joins (cc0b34050a@user/probie) |
| 19:03:32 | → | bwe joins (~bwe@2a01:4f8:1c1c:4878::2) |
| 19:03:33 | → | coldmountain joins (sid484352@id-484352.helmsley.irccloud.com) |
| 19:03:35 | → | shawwwn joins (sid6132@id-6132.helmsley.irccloud.com) |
| 19:03:36 | → | mustafa joins (sid502723@rockylinux/releng/mustafa) |
| 19:03:40 | → | Pent joins (sid313808@id-313808.lymington.irccloud.com) |
| 19:03:40 | → | integral joins (sid296274@user/integral) |
| 19:03:43 | → | ejrietveld joins (~ejrietvel@revspace/participant/bailsman) |
| 19:03:54 | → | ZLima12 joins (~zlima12@user/meow/ZLima12) |
| 19:04:14 | → | sa1 joins (sid7690@id-7690.ilkley.irccloud.com) |
| 19:04:14 | → | GdeVolpiano joins (~GdeVolpia@user/GdeVolpiano) |
| 19:04:49 | × | chele quits (~chele@user/chele) (Remote host closed the connection) |
| 19:05:51 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 19:06:41 | → | albet70 joins (~xxx@2400:8905::f03c:92ff:fe60:98d8) |
| 19:06:55 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 19:06:55 | tnt2 | is now known as tnt1 |
| 19:07:46 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 19:08:20 | → | alfiee joins (~alfiee@user/alfiee) |
| 19:11:52 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:12:32 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 19:14:43 | → | idnar joins (sid12240@debian/mithrandi) |
| 19:15:15 | → | Midjak joins (~MarciZ@82.66.147.146) |
| 19:16:49 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 19:17:27 | → | Hafydd joins (~Hafydd@user/hafydd) |
| 19:17:29 | → | sus0 joins (zero@user/zeromomentum) |
| 19:19:17 | × | comonad quits (~comonad@p200300d027182d00bcfd40be9d94d2dc.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 19:20:43 | [dpk] | is now known as dpk |
| 19:23:47 | <jle`> | that works well enough i guess |
| 19:27:14 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:31:11 | × | zero quits (~z@user/zero) (Quit: quit) |
| 19:32:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 19:33:44 | → | Digitteknohippie joins (~user@user/digit) |
| 19:34:48 | × | Digit quits (~user@user/digit) (Ping timeout: 246 seconds) |
| 19:34:53 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 19:36:00 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 19:38:57 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 19:38:57 | ljdarj1 | is now known as ljdarj |
| 19:43:02 | × | jespada quits (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) (Quit: Textual IRC Client: www.textualapp.com) |
| 19:43:05 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 19:45:30 | → | jespada joins (~jespada@2800:a4:2250:6800:992d:f351:2e1c:1416) |
| 19:47:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 19:52:36 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 19:57:44 | → | alfiee joins (~alfiee@user/alfiee) |
| 19:58:18 | → | ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) |
| 19:58:27 | × | ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit) |
| 19:58:49 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:00:00 | × | caconym quits (~caconym@user/caconym) (Quit: bye) |
| 20:00:40 | → | caconym joins (~caconym@user/caconym) |
| 20:01:45 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
| 20:03:30 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 20:05:31 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 20:14:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:16:54 | → | zero joins (~z@user/zero) |
| 20:19:52 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 20:20:01 | × | jrm quits (~jrm@user/jrm) (Quit: ciao) |
| 20:21:31 | → | jrm joins (~jrm@user/jrm) |
| 20:27:18 | <jle`> | i forgot if ghc does CSE or not |
| 20:28:05 | <geekosaur> | not very |
| 20:28:46 | <jle`> | i guess when in doubt just explicitly pull out the let? |
| 20:28:54 | <geekosaur> | yep |
| 20:29:03 | <jle`> | i guess auto-cse could affect space usage in a weird way |
| 20:30:25 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:31:16 | <jle`> | > let foo = sum (take n (iterate (+1) 0)) + sum (take (2*n) (iterate (+1) 0)) in foo 10 -- would become non-constant space presumably |
| 20:31:17 | <lambdabot> | error: |
| 20:31:17 | <lambdabot> | • Couldn't match expected type ‘Int’ with actual type ‘Expr’ |
| 20:31:17 | <lambdabot> | • In the first argument of ‘take’, namely ‘n’ |
| 20:35:03 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 20:36:45 | × | Me-me quits (~me-me@kc.randomserver.name) (Changing host) |
| 20:36:45 | → | Me-me joins (~me-me@user/me-me) |
| 20:39:30 | → | notzmv joins (~umar@user/notzmv) |
| 20:41:19 | × | jrm quits (~jrm@user/jrm) (Quit: ciao) |
| 20:42:46 | → | jrm joins (~jrm@user/jrm) |
| 20:46:12 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 20:47:10 | → | alfiee joins (~alfiee@user/alfiee) |
| 20:50:06 | <monochrom> | I saw some CSE done by GHC, but yeah it's rare. |
| 20:50:40 | <monochrom> | OTOH for some reason Oleg saw much more, and it hurt his use cases. |
| 20:51:27 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 20:51:27 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 20:51:49 | → | lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 20:53:15 | × | jrm quits (~jrm@user/jrm) (Quit: ciao) |
| 20:53:36 | × | remedan quits (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!) |
| 20:54:44 | → | jrm joins (~jrm@user/jrm) |
| 20:55:05 | → | remedan joins (~remedan@ip-62-245-108-153.bb.vodafone.cz) |
| 20:59:33 | × | jespada quits (~jespada@2800:a4:2250:6800:992d:f351:2e1c:1416) (Ping timeout: 248 seconds) |
| 20:59:48 | <tomsmeding> | GHC does CSE sometimes, mostly when you don't expect it, and it doesn't when you do |
| 21:00:31 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 21:02:01 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:03:28 | → | jespada joins (~jespada@r190-133-42-215.dialup.adsl.anteldata.net.uy) |
| 21:06:02 | × | Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 21:06:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 21:09:48 | × | lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 21:10:34 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 21:11:48 | Digitteknohippie | is now known as Digit |
| 21:16:05 | × | machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 244 seconds) |
| 21:17:48 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:21:50 | lol_ | is now known as jcarpenter2 |
| 21:23:12 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 21:24:22 | × | Googulator quits (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 21:24:37 | → | Googulator joins (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 21:30:59 | × | notzmv quits (~umar@user/notzmv) (Ping timeout: 260 seconds) |
| 21:33:35 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:33:48 | <monochrom> | That sounds about right. :) |
| 21:36:40 | <int-e> | I wonder how accurate https://wiki.haskell.org/Performance/GHC#Common_subexpressions is these days. Note that this is in combination with heavy inlining so you still won't be able to reliably predict any of this |
| 21:37:15 | → | alfiee joins (~alfiee@user/alfiee) |
| 21:38:05 | <haskellbridge> | <thirdofmay18081814goya> is there a recursion scheme I should look into for a lookup operation on a tree of labeled nodes? |
| 21:38:15 | <int-e> | (If you *need* sharing, use `let`.) |
| 21:38:20 | → | notzmv joins (~umar@user/notzmv) |
| 21:38:24 | <haskellbridge> | <thirdofmay18081814goya> so given a string and a tree of labeled nodes, return the first subtree that matches the string |
| 21:38:35 | <haskellbridge> | <thirdofmay18081814goya> or return some subtree that matches the string |
| 21:39:04 | <tomsmeding> | binary tree search or the first hit in an pre-order (or in-order?) traversal? |
| 21:39:07 | <int-e> | how does a subtree match a string |
| 21:39:35 | <haskellbridge> | <thirdofmay18081814goya> tomsmeding: structural recursion over rose tree |
| 21:39:51 | <tomsmeding> | I repeat my question :p |
| 21:40:10 | <haskellbridge> | <thirdofmay18081814goya> structural recursion over inductively defined rosetree |
| 21:40:13 | <haskellbridge> | <thirdofmay18081814goya> so uh |
| 21:40:17 | <haskellbridge> | <thirdofmay18081814goya> I'm not sure |
| 21:40:17 | <tomsmeding> | I was asking _which_ hit you want, not what the tree is defined like |
| 21:40:29 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 21:40:52 | → | Square2 joins (~Square4@user/square) |
| 21:40:52 | <tomsmeding> | what if you search for "a" and the tree contains "a" 5 times? Which do you want to get? |
| 21:41:05 | <tomsmeding> | Is that even valid? (It might not be if you intend this to be a binary search tree) |
| 21:41:19 | <int-e> | What if the string is "aaa"? Does that also produce matches? |
| 21:41:30 | <int-e> | We're asking for a specification. |
| 21:41:37 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 21:42:47 | <haskellbridge> | <thirdofmay18081814goya> the inductive tree is a free monad, "pure" is defined "String -> Tree" and "data Tree a = Nil | Node a (Tree a) (Tree a)" |
| 21:43:08 | <int-e> | but wtf is a match |
| 21:43:22 | <haskellbridge> | <thirdofmay18081814goya> a subtree satisfies the condition if "Tree nodeString _ _" and "mystring = givenString" |
| 21:43:45 | <haskellbridge> | <thirdofmay18081814goya> i meant if it matches "Node nodeString _ _" and "nodeString = givenString" |
| 21:43:49 | × | Square quits (~Square@user/square) (Ping timeout: 248 seconds) |
| 21:44:40 | <tomsmeding> | if you bave `Node "a" (Node "b" (Node "c" Nil Nil) Nil) (Node "b" (Node "d" Nil Nil) Nil)`, and you search for "b", which of the two matching subtrees do you want? |
| 21:44:41 | <haskellbridge> | <thirdofmay18081814goya> as a first approximation i'd be interested in any method that does this in any order |
| 21:44:51 | <tomsmeding> | is this even valid? |
| 21:44:53 | <haskellbridge> | <thirdofmay18081814goya> with any match |
| 21:45:00 | <tomsmeding> | you first have to decide what you _want_ :p |
| 21:45:08 | <tomsmeding> | what's the X problem here? |
| 21:45:24 | <haskellbridge> | <thirdofmay18081814goya> determining whether you can solve this with a catamorphism |
| 21:45:46 | <tomsmeding> | you probably can |
| 21:45:50 | <int-e> | A source of confusion here is that strings can be concatenated. So "matching" grows some extra dimensions of freedom. |
| 21:45:52 | <haskellbridge> | <thirdofmay18081814goya> this constraint might limit what sort of match or order we might be able to get |
| 21:46:04 | × | michalz quits (~michalz@185.246.207.193) (Remote host closed the connection) |
| 21:46:21 | <c_wraith> | for anyone following along, both the psqueues and PSQueue packages now have releases with my tree-balancing fix in them, so they no longer decay to O(n) operations after a long sequence of monotonic inserts |
| 21:47:35 | → | peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 21:47:47 | <c_wraith> | I still don't actually understand the underlying data structure. I just know how to detect divergences from the code in the paper. |
| 21:48:32 | <int-e> | Anyway, this sounds like it's just matching the keys at each node so the natural fold foldTree :: b -> (a -> b -> b -> b) -> Tree a -> b should work just fine for this. Unless you want it to be efficient, in which case it becomes a data structure problem where you probably want some more bookkeeping that track keys and associated subtrees. |
| 21:49:17 | <haskellbridge> | <thirdofmay18081814goya> well the issue is we expect a tree to be returned |
| 21:49:38 | <haskellbridge> | <thirdofmay18081814goya> and as we fold there's no way to stop with just a fold |
| 21:49:42 | <monochrom> | Data.Tree has a foldTree. I believe that it is sufficient for looking for a node by label. I don't really care about other recursion schemes, they are sociology not math. |
| 21:50:12 | × | Googulator quits (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 21:50:36 | <haskellbridge> | <thirdofmay18081814goya> i.e., the challenge is to use one of the fixpoints of the datastructure to recurse structurally, and have a way to stop the recursion |
| 21:50:47 | → | Googulator joins (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 21:51:05 | <tomsmeding> | goya: https://play.haskell.org/saved/KMCLVKww |
| 21:51:08 | <monochrom> | Lazy evaluation easily stops early when something is found. |
| 21:51:15 | <tomsmeding> | what monochrom says |
| 21:51:25 | <monochrom> | > foldr (&&) undefined (False : undefined) |
| 21:51:27 | <lambdabot> | False |
| 21:51:31 | <c_wraith> | Yeah, you don't need to work for that. You need to work to avoid it. |
| 21:51:32 | <monochrom> | Stops early. |
| 21:51:38 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 21:52:00 | <haskellbridge> | <thirdofmay18081814goya> oh neat |
| 21:52:03 | <haskellbridge> | <thirdofmay18081814goya> will be studying that example |
| 21:52:08 | <tomsmeding> | use Maybe instead of [] to get only the first / last / ... match |
| 21:52:23 | <monochrom> | Oh! To avoid lazy evaluation, just lift to liftA2 (&&) for a suitable Applicative instance. >:) |
| 21:52:42 | → | tnt2 joins (~Thunderbi@user/tnt1) |
| 21:53:10 | <int-e> | strictly awful? |
| 21:53:16 | <tomsmeding> | goya: note that my code has to reconstruct the tree in the fold, even though there is already one in memory: the one we're folding over. So this returns new copies of each subtree instead of shared subtrees |
| 21:53:33 | <haskellbridge> | <thirdofmay18081814goya> hm I see |
| 21:53:33 | <tomsmeding> | to do better in terms of space usage, you'll have to augment the folder |
| 21:53:38 | <haskellbridge> | <thirdofmay18081814goya> thanks a lot for the example! |
| 21:53:55 | <tomsmeding> | :) |
| 21:54:48 | <c_wraith> | monochrom: paramorphisms can be an efficiency win, even if they have the same computational power as catamorphisms. |
| 21:54:58 | × | Googulator quits (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Client Quit) |
| 21:55:06 | <c_wraith> | (at least in a non-strict language) |
| 21:55:44 | × | tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 21:55:44 | tnt2 | is now known as tnt1 |
| 21:56:39 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 21:57:02 | × | Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep) |
| 21:57:31 | × | sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 21:59:01 | <EvanR_> | monochrom, stuff like recursion schemes might fall under programming geography |
| 21:59:43 | <EvanR_> | the effect of code on humans and vice versa |
| 22:00:50 | <monochrom> | Ah, I need to respect that. But only out of a mathematical/logical reason: In type theory with user-definable algebraic types (e.g. Agda, Lean), the auto-gen'ed induction principle is a para. |
| 22:02:07 | <int-e> | Recursion schemes are silly; explicit recursion is underrated. Change my mind. |
| 22:03:13 | → | machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net) |
| 22:04:36 | <tomsmeding> | int-e: foldMap is quite useful. |
| 22:04:55 | <mauke> | map is quite useful |
| 22:05:06 | <monochrom> | I consider foldMap to be under monoidology not recursion schemes. >:) |
| 22:05:33 | <tomsmeding> | I guess foldMap is a little less powerful than a full catamorphism would be |
| 22:05:35 | <haskellbridge> | <alexfmpe> Fold *is* recursion |
| 22:05:49 | <haskellbridge> | <alexfmpe> You can write all the other ones via it |
| 22:06:09 | → | img_ joins (~img@user/img) |
| 22:06:18 | <int-e> | It does get interesting when you compose these things... one early showcase is build/foldr fusion. |
| 22:06:51 | <haskellbridge> | <alexfmpe> Might need some unsafe functions in there for traverse-ish if you only require Foldable |
| 22:07:02 | <int-e> | The serious part though is that when figuring out algorithms on simple data structures... "what recursion scheme is this" doesn't seem like a helpful question. |
| 22:07:19 | → | confused_rust_en joins (~confused_@2603:7081:1600:6425:187f:fcc6:e582:3131) |
| 22:07:19 | <tomsmeding> | agreed |
| 22:07:24 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:08:43 | × | img quits (~img@user/img) (Ping timeout: 245 seconds) |
| 22:08:58 | <monochrom> | Related unhelpful theorem: For every computable function, there exists an intermediate data structure T such that the function is composed of ana'ing input into T and then cata'ing T into output. |
| 22:09:25 | <tomsmeding> | if the function goes A -> B, set T = A. |
| 22:09:46 | <tomsmeding> | ah, that's wrong. Set `data T = T A`. |
| 22:11:18 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 22:11:28 | <monochrom> | IIRC it's even worse. The only known proof is non-constructive, or only relatively constructive. It goes: since we are told it's computable, someone must have found an algorithm, now just turn that into T. |
| 22:11:40 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 22:11:59 | × | jespada quits (~jespada@r190-133-42-215.dialup.adsl.anteldata.net.uy) (Ping timeout: 260 seconds) |
| 22:12:00 | <monochrom> | So the theorem doesn't tell you how to design T. Instead, you have to design T and then the theorem just plagiarizes you! |
| 22:12:28 | <monochrom> | Hence completely unhelpful even though sounding very elegant and unifying. |
| 22:12:34 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 22:12:37 | <tomsmeding> | doesn't my T work? |
| 22:12:44 | × | takuan quits (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 22:12:49 | <monochrom> | I don't know. Too lazy to check. :) |
| 22:13:23 | <monochrom> | OTOH I am not sure how to kind-check "T = T A" :) |
| 22:13:29 | <tomsmeding> | if I read the venerable wikipedia correctly, the ana of my T would just be `ana :: (x -> A) -> x -> T` and the cata would be `cata :: (A -> r) -> T -> r` |
| 22:13:44 | <tomsmeding> | monochrom: `data T = MkT A`, happy now? :p |
| 22:13:55 | <monochrom> | Oh wait, yeah, I misread, sorry! |
| 22:14:18 | <tomsmeding> | given `f :: A -> B`, do `cata f . ana id` |
| 22:14:25 | <tomsmeding> | which is extremely unhelpful |
| 22:15:17 | <tomsmeding> | your non-constructive proof is probably about a more subtle statement where T is forced do actually be something useful somehow |
| 22:15:24 | <tomsmeding> | s/do/to/ |
| 22:15:36 | <monochrom> | OK right but my point stands with errata on wording. Someone else has coded up f, so you just plagiarize that in the cata stage. |
| 22:15:46 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 22:16:09 | × | confused_rust_en quits (~confused_@2603:7081:1600:6425:187f:fcc6:e582:3131) (Quit: Client closed) |
| 22:16:30 | <tomsmeding> | I'd say the plagiarism is not the part that's most useless about my construction |
| 22:16:50 | × | peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 22:16:55 | <tomsmeding> | (that's a fun phrase out of context) |
| 22:17:07 | <monochrom> | OTOH this kind of normal-form theorems are always welcome in theoretical work. |
| 22:17:14 | haritz | is now known as saimazoon |
| 22:17:32 | <tomsmeding> | this is not a normal form, this is just a triviality. I maintain that the theorem you're thinking of is probably slightly more subtle so that it doesn't allow my cop-out :) |
| 22:17:48 | <monochrom> | Probably. It's been a while. |
| 22:22:54 | × | mulk quits (~mulk@pd9514894.dip0.t-ipconnect.de) (Remote host closed the connection) |
| 22:23:13 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 22:23:22 | → | nckx_ joins (nckx@libera/staff/owl/nckx) |
| 22:23:55 | × | nckx quits (nckx@libera/staff/owl/nckx) (Ping timeout: 608 seconds) |
| 22:24:17 | nckx_ | is now known as nckx |
| 22:25:40 | → | alfiee joins (~alfiee@user/alfiee) |
| 22:27:53 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 22:30:29 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 22:35:30 | <mauke> | dead poset society |
| 22:39:00 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 22:43:39 | × | myme quits (~myme@40.51-175-185.customer.lyse.net) (Ping timeout: 252 seconds) |
| 22:43:44 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 22:59:58 | × | kuribas` quits (~user@ptr-17d51epnlr9u1hv5k0s.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 23:04:15 | → | weary-traveler joins (~user@user/user363627) |
| 23:07:30 | → | mulk joins (~mulk@pd9514894.dip0.t-ipconnect.de) |
| 23:09:59 | × | Ranhir quits (~Ranhir@157.97.53.139) (Quit: KVIrc 5.0.0 Aria http://www.kvirc.net/) |
| 23:10:35 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:11:58 | → | lythieme joins (~lythieme@209.214.83.194) |
| 23:13:37 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 23:14:43 | → | alfiee joins (~alfiee@user/alfiee) |
| 23:17:28 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 23:17:43 | → | Ranhir joins (~Ranhir@157.97.53.139) |
| 23:19:29 | × | alfiee quits (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 23:20:08 | × | lythieme quits (~lythieme@209.214.83.194) (Quit: Client closed) |
| 23:24:05 | <haskellbridge> | <Bowuigi> foldr/build-like theorems are pretty interesting. On Mendler-encoded data it holds for mcata/mbuild by beta reduction (mbuild is just id but fancy) |
| 23:24:45 | <haskellbridge> | <Bowuigi> Not sure how a paramorphism can be encoded in the same style tho, probably some messing around with the parameters |
| 23:26:26 | <haskellbridge> | <Bowuigi> Histomorphisms can be encoded Mendler-style but not in a total language. Some subset might be able to be encoded tho, haven't checked |
| 23:26:50 | → | ljdarj1 joins (~Thunderbi@user/ljdarj) |
| 23:28:37 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:28:45 | <haskellbridge> | <Bowuigi> I'm actually really interested in those because they are essential in my lang. It's the best lambda encoding without recursive types that I've found |
| 23:29:54 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 23:29:54 | ljdarj1 | is now known as ljdarj |
| 23:33:29 | × | merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 23:33:41 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:44:23 | → | merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl) |
| 23:49:05 | × | merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 23:50:08 | × | acidjnk_new3 quits (~acidjnk@p200300d6e7283f203076ec74f0f78e66.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 23:50:13 | <EvanR_> | mendler-encoding ? |
| 23:55:16 | → | merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl) |
| 23:56:15 | × | GdeVolpiano quits (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 276 seconds) |
All times are in UTC on 2025-01-28.