| 2025-01-28 00:02:43 +0100 | Midjak | (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep) |
| 2025-01-28 00:07:46 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-01-28 00:20:28 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 00:22:15 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) alecs |
| 2025-01-28 00:22:20 +0100 | cheater_ | (~Username@user/cheater) cheater |
| 2025-01-28 00:22:34 +0100 | mange | (~user@user/mange) mange |
| 2025-01-28 00:24:25 +0100 | anpad | (~pandeyan@user/anpad) anpad |
| 2025-01-28 00:24:33 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 2025-01-28 00:24:36 +0100 | cheater_ | cheater |
| 2025-01-28 00:25:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 00:27:04 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2025-01-28 00:29:18 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 00:33:42 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 00:34:12 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) (Quit: alecs) |
| 2025-01-28 00:36:16 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 00:41:08 +0100 | kmein | (~weechat@user/kmein) (Quit: ciao kakao) |
| 2025-01-28 00:41:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 00:43:15 +0100 | kmein | (~weechat@user/kmein) kmein |
| 2025-01-28 00:48:37 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-01-28 00:48:51 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 2025-01-28 00:49:01 +0100 | cheater_ | (~Username@user/cheater) cheater |
| 2025-01-28 00:50:55 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 244 seconds) |
| 2025-01-28 00:50:56 +0100 | cheater_ | cheater |
| 2025-01-28 00:52:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 00:56:25 +0100 | bgamari | (~bgamari@64.223.233.64) (Ping timeout: 252 seconds) |
| 2025-01-28 00:57:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 00:58:32 +0100 | bgamari | (~bgamari@64.223.225.174) |
| 2025-01-28 01:00:54 +0100 | cheater_ | (~Username@user/cheater) cheater |
| 2025-01-28 01:03:01 +0100 | cheater | (~Username@user/cheater) (Ping timeout: 248 seconds) |
| 2025-01-28 01:03:10 +0100 | cheater_ | cheater |
| 2025-01-28 01:07:10 +0100 | talismanick | (~user@2601:644:937c:ed10::ae5) talismanick |
| 2025-01-28 01:07:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 01:08:50 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-01-28 01:12:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 01:16:12 +0100 | jumper | (~pcx180e@131.216.14.87) pcx180e |
| 2025-01-28 01:18:22 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 01:21:38 +0100 | xff0x | (~xff0x@2405:6580:b080:900:ee1a:7699:189f:a423) (Ping timeout: 245 seconds) |
| 2025-01-28 01:22:49 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 2025-01-28 01:23:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 01:23:41 +0100 | anpad | (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-01-28 01:26:31 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) acidjnk |
| 2025-01-28 01:28:14 +0100 | acidjnk_new | (~acidjnk@p200300d6e7283f58f85d99c5648cf6f8.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-01-28 01:28:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 01:28:48 +0100 | califax | (~califax@user/califx) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-01-28 01:29:10 +0100 | califax | (~califax@user/califx) califx |
| 2025-01-28 01:29:24 +0100 | malte | (~malte@mal.tc) (Ping timeout: 260 seconds) |
| 2025-01-28 01:30:22 +0100 | malte | (~malte@mal.tc) malte |
| 2025-01-28 01:39:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 01:44:08 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-28 01:45:11 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 252 seconds) |
| 2025-01-28 01:46:44 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2025-01-28 01:49:48 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 01:51:42 +0100 | anpad | (~pandeyan@user/anpad) anpad |
| 2025-01-28 01:54:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 02:05:10 +0100 | sprotte24 | (~sprotte24@p200300d16f2a5f00a9408391bb436145.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-01-28 02:05:19 +0100 | jumper | (~pcx180e@131.216.14.87) (Quit: WeeChat 4.5.1) |
| 2025-01-28 02:05:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 02:07:05 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 02:10:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 02:11:24 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 02:13:33 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2025-01-28 02:19:37 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-01-28 02:20:27 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-28 02:21:22 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 02:22:57 +0100 | otto_s | (~user@p5b044aa1.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-01-28 02:24:07 +0100 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-01-28 02:24:20 +0100 | otto_s | (~user@p4ff270b9.dip0.t-ipconnect.de) |
| 2025-01-28 02:25:19 +0100 | Guest40 | (~Guest40@2a04:cec0:100f:ae5c:92e8:68ff:fe40:e023) |
| 2025-01-28 02:25:25 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Remote host closed the connection) |
| 2025-01-28 02:25:44 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-28 02:25:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 02:36:49 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 02:37:11 +0100 | jumper | (~pcx180e@131.216.14.87) |
| 2025-01-28 02:37:58 +0100 | malte | (~malte@mal.tc) (Read error: Connection reset by peer) |
| 2025-01-28 02:38:23 +0100 | teesquare_ | (~teesquare@user/teesquare) teesquare |
| 2025-01-28 02:39:24 +0100 | euouae | (~euouae@user/euouae) (Ping timeout: 260 seconds) |
| 2025-01-28 02:39:29 +0100 | teesquare | (~teesquare@user/teesquare) (Ping timeout: 252 seconds) |
| 2025-01-28 02:40:34 +0100 | alx741 | (~alx741@186.33.188.229) (Ping timeout: 252 seconds) |
| 2025-01-28 02:42:30 +0100 | jumper | (~pcx180e@131.216.14.87) (Quit: WeeChat 4.5.1) |
| 2025-01-28 02:43:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 02:47:10 +0100 | malte | (~malte@mal.tc) malte |
| 2025-01-28 02:54:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 02:55:48 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-28 02:56:10 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 02:58:40 +0100 | euouae | (~euouae@user/euouae) euouae |
| 2025-01-28 03:00:06 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-01-28 03:00:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 03:00:39 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 03:03:03 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-28 03:10:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 03:15:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 03:21:16 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 252 seconds) |
| 2025-01-28 03:21:50 +0100 | tavare | (~tavare@user/tavare) tavare |
| 2025-01-28 03:26:25 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 03:27:53 +0100 | tabaqui1 | (~root@87.200.129.102) (Ping timeout: 245 seconds) |
| 2025-01-28 03:30:25 +0100 | notzmv | (~umar@user/notzmv) (Remote host closed the connection) |
| 2025-01-28 03:31:19 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 03:32:05 +0100 | internatetional | (~internate@2001:448a:20a3:c2e5:1c8c:35b1:e1f9:b138) internatetional |
| 2025-01-28 03:35:59 +0100 | euouae | (~euouae@user/euouae) (Ping timeout: 260 seconds) |
| 2025-01-28 03:42:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 03:45:15 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 03:47:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-28 03:48:21 +0100 | euouae | (~euouae@user/euouae) euouae |
| 2025-01-28 03:49:30 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 03:53:25 +0100 | Guest40 | (~Guest40@2a04:cec0:100f:ae5c:92e8:68ff:fe40:e023) (Quit: Client closed) |
| 2025-01-28 03:56:35 +0100 | internatetional | (~internate@2001:448a:20a3:c2e5:1c8c:35b1:e1f9:b138) (Quit: Leaving) |
| 2025-01-28 03:57:59 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 03:59:49 +0100 | Guest93 | (~Guest93@syn-074-076-186-205.res.spectrum.com) |
| 2025-01-28 04:03:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 04:07:20 +0100 | AvengingFemme | (~avengingf@syn-074-076-186-205.res.spectrum.com) |
| 2025-01-28 04:07:40 +0100 | Guest93 | (~Guest93@syn-074-076-186-205.res.spectrum.com) (Quit: Client closed) |
| 2025-01-28 04:12:51 +0100 | AvengingFemme | (~avengingf@syn-074-076-186-205.res.spectrum.com) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-28 04:13:46 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 04:19:09 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 04:27:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 04:32:46 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 04:34:18 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 04:37:32 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2025-01-28 04:38:59 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 04:43:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 04:46:15 +0100 | ensyde | (~ensyde@2601:5c6:c200:6dc0::3cb6) ensyde |
| 2025-01-28 04:48:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 04:50:38 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-01-28 04:58:52 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 265 seconds) |
| 2025-01-28 04:59:28 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 05:00:13 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) (Read error: Connection reset by peer) |
| 2025-01-28 05:00:30 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-28 05:00:37 +0100 | alp_ | (~alp@2001:861:8ca0:4940:3dda:cd0f:afd0:a6c6) (Ping timeout: 252 seconds) |
| 2025-01-28 05:04:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-28 05:15:14 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 05:22:09 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 05:22:33 +0100 | ensyde | (~ensyde@2601:5c6:c200:6dc0::3cb6) (Ping timeout: 252 seconds) |
| 2025-01-28 05:23:23 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 05:27:45 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 05:33:17 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 05:38:29 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 05:40:06 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-28 05:45:18 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-01-28 05:49:05 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 05:51:36 +0100 | lythienne | (~lythieme@user/lythienne) lythienne |
| 2025-01-28 05:54:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-28 05:57:40 +0100 | lythienne | (~lythieme@user/lythienne) (Ping timeout: 240 seconds) |
| 2025-01-28 06:04:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 06:06:50 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-01-28 06:07:17 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-01-28 06:08:47 +0100 | lythieme | (~lythieme@c-24-6-125-113.hsd1.ca.comcast.net) |
| 2025-01-28 06:09:56 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 06:12:46 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 06:17:34 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 06:19:11 +0100 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2025-01-28 06:19:37 +0100 | ec | (~ec@gateway/tor-sasl/ec) ec |
| 2025-01-28 06:28:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 06:34:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2025-01-28 06:37:55 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2025-01-28 06:37:55 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-01-28 06:38:08 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2025-01-28 06:38:37 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-01-28 06:39:42 +0100 | michalz | (~michalz@185.246.207.193) |
| 2025-01-28 06:41:55 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-28 06:44:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 06:49:32 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 06:59:47 +0100 | euouae | (~euouae@user/euouae) () |
| 2025-01-28 07:00:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 07:01:11 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 07:05:24 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 07:05:59 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 07:12:23 +0100 | echoreply | (~echoreply@45.32.163.16) (Quit: WeeChat 2.8) |
| 2025-01-28 07:13:18 +0100 | echoreply | (~echoreply@45.32.163.16) echoreply |
| 2025-01-28 07:16:16 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 07:17:12 +0100 | alp_ | (~alp@2001:861:8ca0:4940:7256:930c:e9bd:85d0) |
| 2025-01-28 07:18:14 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) |
| 2025-01-28 07:21:06 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-28 07:24:13 +0100 | ft | (~ft@p3e9bcd97.dip0.t-ipconnect.de) (Quit: leaving) |
| 2025-01-28 07:25:22 +0100 | anpad | (~pandeyan@user/anpad) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2025-01-28 07:26:14 +0100 | anpad | (~pandeyan@user/anpad) anpad |
| 2025-01-28 07:28:43 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 245 seconds) |
| 2025-01-28 07:29:43 +0100 | euleritian | (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) |
| 2025-01-28 07:29:52 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 07:34:38 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 07:37:38 +0100 | hgolden_ | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) (Remote host closed the connection) |
| 2025-01-28 07:40:19 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-28 07:40:22 +0100 | hgolden | (~hgolden@2603:8000:9d00:3ed1:6ff3:8389:b901:6363) hgolden |
| 2025-01-28 07:40:43 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-28 07:45:41 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 07:49:56 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 07:50:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 07:54:13 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-01-28 07:56:23 +0100 | hawer | (~newyear@2.219.56.221) |
| 2025-01-28 07:58:59 +0100 | fp | (~Thunderbi@87-94-148-3.rev.dnainternet.fi) fp |
| 2025-01-28 08:01:28 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 08:07:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2025-01-28 08:09:30 +0100 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2025-01-28 08:10:01 +0100 | rvalue | (~rvalue@user/rvalue) rvalue |
| 2025-01-28 08:10:53 +0100 | CiaoSen | (~Jura@2a05:5800:238:6500:ca4b:d6ff:fec1:99da) CiaoSen |
| 2025-01-28 08:11:07 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 244 seconds) |
| 2025-01-28 08:12:27 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) |
| 2025-01-28 08:15:01 +0100 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2025-01-28 08:19:30 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 08:20:21 +0100 | fp | (~Thunderbi@87-94-148-3.rev.dnainternet.fi) (Ping timeout: 248 seconds) |
| 2025-01-28 08:21:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-01-28 08:21:51 +0100 | sawilagar | (~sawilagar@user/sawilagar) sawilagar |
| 2025-01-28 08:22:27 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-01-28 08:24:44 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 08:30:53 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 08:35:51 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 08:38:39 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 08:39:19 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2025-01-28 08:40:43 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-28 08:43:02 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2025-01-28 08:43:24 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 08:43:53 +0100 | Digit | (~user@user/digit) (Ping timeout: 244 seconds) |
| 2025-01-28 08:46:40 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 08:49:53 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-01-28 08:51:20 +0100 | euleritian | (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-28 08:51:34 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 08:51:37 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-28 08:53:59 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2025-01-28 09:00:00 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-01-28 09:00:41 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-01-28 09:02:26 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 09:06:56 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-28 09:07:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2025-01-28 09:08:20 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2025-01-28 09:18:13 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-28 09:18:23 +0100 | ash3en | (~Thunderbi@2a02:8108:2810:ab00::4c86) ash3en |
| 2025-01-28 09:23:39 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 09:24:41 +0100 | gentauro | (~gentauro@user/gentauro) (Read error: Connection reset by peer) |
| 2025-01-28 09:27:12 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2025-01-28 09:27:24 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 09:30:45 +0100 | gentauro | (~gentauro@user/gentauro) gentauro |
| 2025-01-28 09:30:50 +0100 | monochrm | (trebla@216.138.220.146) |
| 2025-01-28 09:31:10 +0100 | monochrom | (trebla@216.138.220.146) (Ping timeout: 272 seconds) |
| 2025-01-28 09:31:13 +0100 | monochrm | monochrom |
| 2025-01-28 09:31:35 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 09:33:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds) |
| 2025-01-28 09:34:58 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-01-28 09:37:08 +0100 | monochrm | (trebla@216.138.220.146) |
| 2025-01-28 09:37:55 +0100 | monochrom | (trebla@216.138.220.146) (Ping timeout: 244 seconds) |
| 2025-01-28 09:37:55 +0100 | monochrm | monochrom |
| 2025-01-28 09:41:20 +0100 | chele | (~chele@user/chele) chele |
| 2025-01-28 09:43:30 +0100 | notzmv | (~umar@user/notzmv) (Read error: Connection reset by peer) |
| 2025-01-28 09:44:41 +0100 | smalltalkman | (uid545680@id-545680.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-28 09:55:05 +0100 | Digitteknohippie | Digit |
| 2025-01-28 09:55:09 +0100 | <dminuoso> | sm: Neither megaparsec nor flatparse have good documentation. The former is too overwhelming and not intuitive, and the latter has too little.o |
| 2025-01-28 09:55:29 +0100 | <dminuoso> | But in the domain of parser generators and libraries that seems to fit well within the norm. |
| 2025-01-28 09:55:39 +0100 | tnt1 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-28 09:56:47 +0100 | sarna | (~sarna@d224-221.icpnet.pl) sarna |
| 2025-01-28 10:01:13 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-01-28 10:01:18 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 10:06:11 +0100 | <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? |
| 2025-01-28 10:06:41 +0100 | <sarna> | (the thing I'm working on it's not in haskell, but I figured y'all would have lots of experience with this) |
| 2025-01-28 10:07:55 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-01-28 10:09:16 +0100 | <merijn> | sarna: In Haskell i'd probably rewrite that into something like conduit |
| 2025-01-28 10:09:43 +0100 | <merijn> | But whether that's relevant depends on whatever language you have having something equivalent of conduit :p |
| 2025-01-28 10:09:56 +0100 | <ColinRobinson> | why would we care in some arbitrary lang, that doesn have the propoerties hs labors to have? |
| 2025-01-28 10:10:52 +0100 | <ColinRobinson> | also hs only seperates application logic into its pure form |
| 2025-01-28 10:11:56 +0100 | <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 |
| 2025-01-28 10:12:03 +0100 | <sarna> | merijn: thanks, I'll read about it! looks promising so far |
| 2025-01-28 10:12:43 +0100 | <sarna> | ColinRobinson: are you draining me right now? |
| 2025-01-28 10:13:20 +0100 | <ColinRobinson> | sorta, this is my factitious persona and normies find that super draining |
| 2025-01-28 10:13:40 +0100 | <sarna> | I'm working in a dynamically typed language, but I want to separate IO out mainly for better/simpler testing |
| 2025-01-28 10:14:31 +0100 | <haskellbridge> | <magic_rb> in a dynamically typed language, mocks are common place i feel like. Essentially passing around fake instances of certain classes |
| 2025-01-28 10:14:46 +0100 | <haskellbridge> | <magic_rb> at least thats how people do it in python, dunno about lisps for example |
| 2025-01-28 10:15:04 +0100 | fp | (~Thunderbi@cib5.wlan.kyla.fi) fp |
| 2025-01-28 10:16:29 +0100 | <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 |
| 2025-01-28 10:16:36 +0100 | <sarna> | I know, but I don't want to mock stuff. and not all dynamic lang ppl love mocks (see Gary Bernhardt) |
| 2025-01-28 10:17:09 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 10:17:22 +0100 | <ColinRobinson> | generally in lisp i'm not concerned to separate io into some hermetic cell or whatever |
| 2025-01-28 10:17:55 +0100 | <ColinRobinson> | but if i were then id do a seperation of classes or generic functions |
| 2025-01-28 10:19:16 +0100 | fp | (~Thunderbi@cib5.wlan.kyla.fi) (Ping timeout: 252 seconds) |
| 2025-01-28 10:21:44 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 265 seconds) |
| 2025-01-28 10:21:45 +0100 | <merijn> | sarna: tbh, in most dynamically typed languages it's rather hard to stop IO from intermingling with business logic |
| 2025-01-28 10:24:11 +0100 | <sarna> | merijn: well yeah there's no type system to enforce that, but it's not inherently impossible |
| 2025-01-28 10:25:54 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-01-28 10:26:06 +0100 | <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 |
| 2025-01-28 10:26:43 +0100 | euleritian | (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) |
| 2025-01-28 10:27:03 +0100 | <haskellbridge> | <sm> you can still move the bits that don't require IO into callable pure functions |
| 2025-01-28 10:27:13 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-01-28 10:27:41 +0100 | lisbeths | (~user@2603:3023:4be:4000:216:3eff:fe17:d69d) lisbeths |
| 2025-01-28 10:29:45 +0100 | absence_ | (torgeihe@hildring.pvv.ntnu.no) |
| 2025-01-28 10:29:45 +0100 | absence | (torgeihe@hildring.pvv.ntnu.no) (Read error: Connection reset by peer) |
| 2025-01-28 10:34:14 +0100 | absence_ | (torgeihe@hildring.pvv.ntnu.no) (Ping timeout: 244 seconds) |
| 2025-01-28 10:35:14 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-01-28 10:41:35 +0100 | fp | (~Thunderbi@cib5.wlan.kyla.fi) fp |
| 2025-01-28 10:41:52 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 10:44:15 +0100 | <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 |
| 2025-01-28 10:44:38 +0100 | <sarna> | this way I have no branching/logic in the IO function and can move it to the edge |
| 2025-01-28 10:44:40 +0100 | <sarna> | thanks! |
| 2025-01-28 10:44:45 +0100 | <haskellbridge> | <sm> sounds good! |
| 2025-01-28 10:45:03 +0100 | absence | (torgeihe@hildring.pvv.ntnu.no) |
| 2025-01-28 10:46:02 +0100 | fp | (~Thunderbi@cib5.wlan.kyla.fi) (Ping timeout: 252 seconds) |
| 2025-01-28 10:47:04 +0100 | acarrico | (~acarrico@dhcp-209-99-192-63.greenmountainaccess.net) (Ping timeout: 260 seconds) |
| 2025-01-28 10:47:34 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-01-28 10:49:29 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) SlackCoder |
| 2025-01-28 10:49:49 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-01-28 11:00:05 +0100 | acarrico | (~acarrico@pppoe-209-99-221-107.greenmountainaccess.net) |
| 2025-01-28 11:00:43 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 11:05:52 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 11:10:24 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 11:10:49 +0100 | euleritian | (~euleritia@dynamic-176-006-134-178.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-28 11:11:07 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-28 11:17:28 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 245 seconds) |
| 2025-01-28 11:17:54 +0100 | fp | (~Thunderbi@cib5.wlan.kyla.fi) fp |
| 2025-01-28 11:22:09 +0100 | fp | (~Thunderbi@cib5.wlan.kyla.fi) (Ping timeout: 246 seconds) |
| 2025-01-28 11:34:41 +0100 | lisbeths | (~user@2603:3023:4be:4000:216:3eff:fe17:d69d) (Remote host closed the connection) |
| 2025-01-28 11:41:29 +0100 | tavare | (~tavare@user/tavare) (Ping timeout: 265 seconds) |
| 2025-01-28 11:42:29 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-01-28 11:48:37 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 11:54:37 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 11:57:33 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) kuribas |
| 2025-01-28 11:58:45 +0100 | <kuribas> | Is this project dead? https://hackage.haskell.org/package/caledon |
| 2025-01-28 11:59:01 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-01-28 11:59:34 +0100 | ash3en | (~Thunderbi@2a02:8108:2810:ab00::4c86) (Quit: ash3en) |
| 2025-01-28 12:01:45 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-28 12:01:54 +0100 | <dminuoso> | Well you can see yourself when it was last uploaded to hackage, and when the package received commits last... |
| 2025-01-28 12:02:00 +0100 | <dminuoso> | What is it that you want to know? |
| 2025-01-28 12:02:34 +0100 | <kuribas> | If it makes sense to invest some time in it... |
| 2025-01-28 12:02:44 +0100 | <kuribas> | It looks like a successor of twelf. |
| 2025-01-28 12:04:38 +0100 | <kuribas> | dminuoso: what interests me is using a dependently type languages for logic. |
| 2025-01-28 12:06:44 +0100 | mange | (~user@user/mange) (Remote host closed the connection) |
| 2025-01-28 12:10:17 +0100 | xff0x | (~xff0x@ai096095.d.east.v6connect.net) |
| 2025-01-28 12:10:48 +0100 | tavare | (~tavare@user/tavare) tavare |
| 2025-01-28 12:30:19 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2025-01-28 12:30:19 +0100 | lockywolf | (~lockywolf@coconut.lockywolf.net) (Read error: Connection reset by peer) |
| 2025-01-28 12:39:47 +0100 | monochrm | (trebla@216.138.220.146) |
| 2025-01-28 12:41:49 +0100 | monochrom | (trebla@216.138.220.146) (Ping timeout: 260 seconds) |
| 2025-01-28 12:41:49 +0100 | monochrm | monochrom |
| 2025-01-28 12:43:01 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 12:43:29 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 12:45:12 +0100 | monochrm | (trebla@216.138.220.146) |
| 2025-01-28 12:45:21 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:e9b3:4a8b:794e:b4a) ubert |
| 2025-01-28 12:46:43 +0100 | monochrom | (trebla@216.138.220.146) (Ping timeout: 265 seconds) |
| 2025-01-28 12:46:44 +0100 | monochrm | monochrom |
| 2025-01-28 12:47:24 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 12:47:54 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2025-01-28 13:00:05 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-01-28 13:00:38 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 13:02:41 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2025-01-28 13:03:56 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-01-28 13:05:23 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 245 seconds) |
| 2025-01-28 13:08:26 +0100 | rvalue- | (~rvalue@user/rvalue) rvalue |
| 2025-01-28 13:09:24 +0100 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 260 seconds) |
| 2025-01-28 13:15:03 +0100 | rvalue- | rvalue |
| 2025-01-28 13:17:31 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 13:22:09 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 244 seconds) |
| 2025-01-28 13:25:48 +0100 | Guest72 | (~Guest28@conect.gtstelecom.ro) |
| 2025-01-28 13:27:29 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-01-28 13:32:24 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 13:34:11 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 13:36:49 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 13:38:56 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 265 seconds) |
| 2025-01-28 13:39:56 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) |
| 2025-01-28 13:51:22 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 13:54:48 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2025-01-28 13:57:13 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-01-28 14:02:16 +0100 | tabaqui1 | (~root@87.200.129.102) tabaqui |
| 2025-01-28 14:05:57 +0100 | yin | (~z@user/zero) (Ping timeout: 248 seconds) |
| 2025-01-28 14:07:11 +0100 | zero | (~z@user/zero) zero |
| 2025-01-28 14:10:33 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2025-01-28 14:11:37 +0100 | jespada | (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) jespada |
| 2025-01-28 14:16:23 +0100 | alx741 | (~alx741@186.33.188.229) |
| 2025-01-28 14:20:38 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-01-28 14:21:09 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 14:25:12 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
| 2025-01-28 14:32:38 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2025-01-28 14:34:24 +0100 | CiaoSen | (~Jura@2a05:5800:238:6500:ca4b:d6ff:fec1:99da) (Ping timeout: 260 seconds) |
| 2025-01-28 14:37:24 +0100 | merijn | (~merijn@77.242.116.146) merijn |
| 2025-01-28 14:45:03 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-01-28 14:51:55 +0100 | terrorjack45 | (~terrorjac@2a01:4f8:c17:a66e::) (Ping timeout: 265 seconds) |
| 2025-01-28 14:55:27 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-01-28 15:09:34 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 15:13:43 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 2025-01-28 15:23:14 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-01-28 15:24:08 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Remote host closed the connection) |
| 2025-01-28 15:24:32 +0100 | euleritian | (~euleritia@dynamic-176-006-133-195.176.6.pool.telefonica.de) |
| 2025-01-28 15:25:49 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-28 15:26:45 +0100 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-01-28 15:28:06 +0100 | AvengingFemme | (~avengingf@syn-074-076-186-205.res.spectrum.com) |
| 2025-01-28 15:29:34 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2025-01-28 15:33:41 +0100 | lythieme | (~lythieme@c-24-6-125-113.hsd1.ca.comcast.net) (Quit: Client closed) |
| 2025-01-28 15:40:10 +0100 | <kuribas> | I want to write a formal proof (in idris), then port it to clojure. |
| 2025-01-28 15:40:41 +0100 | <kuribas> | Hm, I might create an inductive type family in idris, create a prove, and port to minikanren in clojure (core.logic). |
| 2025-01-28 15:41:27 +0100 | <kuribas> | That could make for an easy (almost) mechanical translation. |
| 2025-01-28 15:41:58 +0100 | <kuribas> | But I guess I am in the wrong channel for this discussion... |
| 2025-01-28 15:43:11 +0100 | terrorjack45 | (~terrorjac@2a01:4f8:c17:a66e::) terrorjack |
| 2025-01-28 15:43:37 +0100 | <ski> | proofs in Twelf tends to consist of the system checking mode of some hand-crafted relation/predicate you've defined |
| 2025-01-28 15:45:26 +0100 | <kuribas> | ski: but can it proof a complicated type checker? (with parametricity, rank-n types, ...) |
| 2025-01-28 15:48:21 +0100 | <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') |
| 2025-01-28 15:49:05 +0100 | <ski> | (and the definition of this relation would basically amount to the steps required for this proof) |
| 2025-01-28 15:49:15 +0100 | <kuribas> | ski: I want a declarative specification of a type inference algorithm, then prove that the result is well typed. |
| 2025-01-28 15:49:16 +0100 | euleritian | (~euleritia@dynamic-176-006-133-195.176.6.pool.telefonica.de) (Ping timeout: 272 seconds) |
| 2025-01-28 15:49:23 +0100 | <kuribas> | ski: and if possible complete (though much harder). |
| 2025-01-28 15:49:45 +0100 | <kuribas> | like this paper: https://www.cl.cam.ac.uk/~nk480/bidir.pdf |
| 2025-01-28 15:49:47 +0100 | <ski> | Twelf only has three levels, terms, families (types), and kinds |
| 2025-01-28 15:51:25 +0100 | terrorjack45 | terrorjack |
| 2025-01-28 15:52:02 +0100 | <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 |
| 2025-01-28 15:52:08 +0100 | <ski> | *encoding* polymorphism in an object language, though) |
| 2025-01-28 15:52:54 +0100 | <ski> | mm. i don't see why one couldn't do bidirectional |
| 2025-01-28 15:53:32 +0100 | <ski> | iirc, some of the metatheory of Olli was formalized in Twelf, including stuff related to bidirectional |
| 2025-01-28 15:54:02 +0100 | <kuribas> | ski: Is it hard to hand craft proofs in twelf? |
| 2025-01-28 15:54:17 +0100 | <kuribas> | Does it offer the same features as idris2/agda, like showing goals? |
| 2025-01-28 15:54:28 +0100 | <kuribas> | And typed holes. |
| 2025-01-28 15:54:44 +0100 | <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) |
| 2025-01-28 15:55:45 +0100 | <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 |
| 2025-01-28 15:56:00 +0100 | <ski> | can't recall seeing anything about holes |
| 2025-01-28 15:56:12 +0100 | nschoe- | (~nschoe@82-65-202-30.subs.proxad.net) (Ping timeout: 246 seconds) |
| 2025-01-28 15:56:18 +0100 | nschoe | (~nschoe@2a01:e0a:8e:a190:15d4:9b4c:59c3:ed22) nschoe |
| 2025-01-28 15:56:48 +0100 | <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 |
| 2025-01-28 15:57:56 +0100 | <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 |
| 2025-01-28 15:59:18 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 15:59:20 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-01-28 15:59:36 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 2025-01-28 16:00:37 +0100 | <kuribas> | idris has proof search, but it's not very powerful. |
| 2025-01-28 16:00:54 +0100 | <kuribas> | perhaps twelf does that better. |
| 2025-01-28 16:01:01 +0100 | <ski> | not backtracking ? |
| 2025-01-28 16:01:10 +0100 | <ski> | Twelf does backtracking |
| 2025-01-28 16:01:17 +0100 | <kuribas> | It does. |
| 2025-01-28 16:01:51 +0100 | <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 |
| 2025-01-28 16:02:30 +0100 | <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) |
| 2025-01-28 16:03:49 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 16:04:16 +0100 | <ski> | a `:- mode append(out,out,in) is multi.' mode meta-proves `forall [XsYs] at_least [Xs,Ys] append(Xs,Ys,XsYs).' |
| 2025-01-28 16:05:03 +0100 | <ski> | s/at_least/at_least_one/ |
| 2025-01-28 16:05:03 +0100 | <kuribas> | ski: twelf does have modes? |
| 2025-01-28 16:05:12 +0100 | <ski> | while `:- mode append(in,out,in) is semidet.' meta-proves `forall [Xs,XsYs] at_most_one [Ys] append(Xs,Ys,XsYs).' |
| 2025-01-28 16:05:22 +0100 | <ski> | kuribas : yes, but only rather restricted |
| 2025-01-28 16:05:35 +0100 | <ski> | (the two examples above are from Mercury) |
| 2025-01-28 16:06:23 +0100 | <ski> | and `:- mode append(in,in,out) is det.' meta-proves `forall [Xs,Ys] exactly_one [XsYs] append(Xs,Ys,XsYs).' |
| 2025-01-28 16:08:00 +0100 | <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 |
| 2025-01-28 16:08:04 +0100 | <kuribas> | ski: should I look at mercury? |
| 2025-01-28 16:08:10 +0100 | <kuribas> | ski: but it's not dependently typed, right? |
| 2025-01-28 16:08:53 +0100 | <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) |
| 2025-01-28 16:09:48 +0100 | AvengingFemme | (~avengingf@syn-074-076-186-205.res.spectrum.com) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-28 16:09:52 +0100 | <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) |
| 2025-01-28 16:10:28 +0100 | <ski> | Mercury is highly interesting, i'd say, yes. not so much from a type theory perspective, though. but from a logic programming one |
| 2025-01-28 16:12:16 +0100 | <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 |
| 2025-01-28 16:14:24 +0100 | <kuribas> | right |
| 2025-01-28 16:16:29 +0100 | SlackCoder | (~SlackCode@64-94-63-8.ip.weststar.net.ky) (Quit: Leaving) |
| 2025-01-28 16:16:54 +0100 | Guest72 | (~Guest28@conect.gtstelecom.ro) (Quit: Client closed) |
| 2025-01-28 16:19:10 +0100 | <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 |
| 2025-01-28 16:19:30 +0100 | <ski> | it also has some support for constraint logic programming |
| 2025-01-28 16:21:27 +0100 | <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)))) |
| 2025-01-28 16:24:00 +0100 | <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 |
| 2025-01-28 16:24:06 +0100 | <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 |
| 2025-01-28 16:26:12 +0100 | <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) |
| 2025-01-28 16:27:18 +0100 | <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 |
| 2025-01-28 16:30:31 +0100 | <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 |
| 2025-01-28 16:30:37 +0100 | <ski> | `promise_equivalent_solutions' construct at the point where you believe the internal details can no longer be observed) |
| 2025-01-28 16:31:41 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2025-01-28 16:31:41 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-01-28 16:31:42 +0100 | <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 |
| 2025-01-28 16:31:57 +0100 | chexum | (~quassel@gateway/tor-sasl/chexum) chexum |
| 2025-01-28 16:32:00 +0100 | califax_ | (~califax@user/califx) califx |
| 2025-01-28 16:32:26 +0100 | gehmehgeh | (~user@user/gehmehgeh) gehmehgeh |
| 2025-01-28 16:32:43 +0100 | <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)) |
| 2025-01-28 16:33:34 +0100 | gmg | (~user@user/gehmehgeh) (Killed (NickServ (Forcing logout gmg -> gehmehgeh))) |
| 2025-01-28 16:33:34 +0100 | gehmehgeh | gmg |
| 2025-01-28 16:33:43 +0100 | user_ | (~user@user/fmira) fmira |
| 2025-01-28 16:34:24 +0100 | califax | (~califax@user/califx) (Ping timeout: 264 seconds) |
| 2025-01-28 16:34:24 +0100 | califax_ | califax |
| 2025-01-28 16:35:36 +0100 | ec | (~ec@gateway/tor-sasl/ec) (Ping timeout: 264 seconds) |
| 2025-01-28 16:35:36 +0100 | fmira | (~user@user/fmira) (Ping timeout: 264 seconds) |
| 2025-01-28 16:37:09 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-01-28 16:37:31 +0100 | ec | (~ec@gateway/tor-sasl/ec) ec |
| 2025-01-28 16:37:45 +0100 | mesaoptimizer | (~mesa@user/PapuaHardyNet) (Quit: WeeChat 4.0.4) |
| 2025-01-28 16:38:08 +0100 | mesaoptimizer | (~mesa@user/PapuaHardyNet) PapuaHardyNet |
| 2025-01-28 16:39:59 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-01-28 16:40:19 +0100 | mesaoptimizer | (~mesa@user/PapuaHardyNet) (Client Quit) |
| 2025-01-28 16:40:32 +0100 | mesaoptimizer | (~mesa@user/PapuaHardyNet) PapuaHardyNet |
| 2025-01-28 16:48:43 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 16:49:55 +0100 | <kuribas> | ski: so (==) is DecEq ? |
| 2025-01-28 16:53:03 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 16:53:52 +0100 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess |
| 2025-01-28 16:57:05 +0100 | <ski> | in Haskell, basically yes (modulo infinite data) |
| 2025-01-28 16:57:17 +0100 | <ski> | in Mercury, there is no `==', only `=' |
| 2025-01-28 16:57:51 +0100 | <kuribas> | ski: in haskell (a == b) doesn't mean (a = b). |
| 2025-01-28 16:58:20 +0100 | <kuribas> | For example HashSet (a == b) may not mean (a = b) because of internal representation differences. |
| 2025-01-28 17:00:13 +0100 | <ski> | yes and no |
| 2025-01-28 17:01:00 +0100 | <ski> | conceptually, the representation differences are not supposed to be considered for the semantic value (enforced by not leaking such implementation from the operations) |
| 2025-01-28 17:02:25 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) (Remote host closed the connection) |
| 2025-01-28 17:02:49 +0100 | <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) |
| 2025-01-28 17:04:06 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-28 17:04:20 +0100 | TheCoffeMaker | (~TheCoffeM@user/thecoffemaker) TheCoffeMaker |
| 2025-01-28 17:04:30 +0100 | <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 |
| 2025-01-28 17:05:24 +0100 | euleritian | (~euleritia@dynamic-176-006-133-249.176.6.pool.telefonica.de) |
| 2025-01-28 17:06:01 +0100 | <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 |
| 2025-01-28 17:07:43 +0100 | <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 |
| 2025-01-28 17:07:49 +0100 | <ski> | away from it |
| 2025-01-28 17:18:16 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-01-28 17:18:33 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 2025-01-28 17:20:37 +0100 | <ski> | (in Mercury, `make_set(L0) = make_set(L1)' does not mean `L0 = L1' .. which is what non-injectivity means) |
| 2025-01-28 17:21:23 +0100 | ft | (~ft@p3e9bcd97.dip0.t-ipconnect.de) ft |
| 2025-01-28 17:23:58 +0100 | jespada | (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-28 17:24:58 +0100 | euleritian | (~euleritia@dynamic-176-006-133-249.176.6.pool.telefonica.de) (Ping timeout: 252 seconds) |
| 2025-01-28 17:31:14 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-28 17:35:53 +0100 | ColinRobinson | (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org)) |
| 2025-01-28 17:38:26 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 17:40:28 +0100 | <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 ? |
| 2025-01-28 17:40:34 +0100 | <ski> | possible deadlock or unexpected indeterminacy ?) |
| 2025-01-28 17:41:21 +0100 | <ski> | `promise_XXX' brings the attention more to what your proof obligations, as a programmer are, encourages expressing that in the `XXX' part |
| 2025-01-28 17:42:33 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2025-01-28 17:42:56 +0100 | <ski> | (e.g. `unsafePerformIO' could perhaps be called `promisePureIO', here. with `promisePureIO (return x)' being equivalent to `x') |
| 2025-01-28 17:42:59 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 17:48:27 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 244 seconds) |
| 2025-01-28 17:56:21 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2025-01-28 17:57:10 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-28 18:06:21 +0100 | <haskellbridge> | <Bowuigi> ski Twelf has unique modes and a separate metatheorem prover if that's not enough |
| 2025-01-28 18:07:11 +0100 | <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 |
| 2025-01-28 18:08:02 +0100 | <ski> | "unique modes" referring to ? |
| 2025-01-28 18:08:23 +0100 | <haskellbridge> | <Bowuigi> Unique outputs, mainly |
| 2025-01-28 18:08:29 +0100 | <ski> | and yea, it has some more advanced meta-stuff as well |
| 2025-01-28 18:08:40 +0100 | <ski> | ah, right |
| 2025-01-28 18:09:13 +0100 | <haskellbridge> | <Bowuigi> https://twelf.org/wiki/percent-unique/ |
| 2025-01-28 18:09:22 +0100 | <ski> | i recall reading some papers about a functional programming language for meta-programming proofs over Twelf terms |
| 2025-01-28 18:10:59 +0100 | jespada | (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) jespada |
| 2025-01-28 18:11:49 +0100 | <haskellbridge> | <Bowuigi> The metatheorem stuff is specially interesting because it automagically proves stuff https://twelf.org/wiki/theorem-prover/ |
| 2025-01-28 18:13:21 +0100 | merijn | (~merijn@77.242.116.146) (Ping timeout: 248 seconds) |
| 2025-01-28 18:13:25 +0100 | <haskellbridge> | <Bowuigi> Twelf is by far my favourite theorem prover. Is Mercury a similar alternative? Agda and friends are more cumbersome tbh |
| 2025-01-28 18:16:35 +0100 | <ski> | "Delphin" by Adam Brett Poswolsky at <https://delphin.poswolsky.com/> |
| 2025-01-28 18:18:00 +0100 | <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 |
| 2025-01-28 18:19:02 +0100 | <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)) |
| 2025-01-28 18:20:37 +0100 | <ski> | (the representation and handling of lambdas in Twelf is quite similar to that in LambdaProlog, based largely on the same ideas) |
| 2025-01-28 18:22:53 +0100 | <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)) |
| 2025-01-28 18:24:31 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-28 18:28:55 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-01-28 18:29:16 +0100 | Square | (~Square@user/square) Square |
| 2025-01-28 18:29:30 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 18:30:48 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Ping timeout: 264 seconds) |
| 2025-01-28 18:31:16 +0100 | user_ | (~user@user/fmira) (Remote host closed the connection) |
| 2025-01-28 18:31:25 +0100 | fmira | (~user@user/fmira) fmira |
| 2025-01-28 18:31:49 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-01-28 18:32:33 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-01-28 18:32:45 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 276 seconds) |
| 2025-01-28 18:34:19 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-01-28 18:35:28 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) |
| 2025-01-28 18:36:02 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-28 18:37:49 +0100 | kuribas | (~user@2a02:1808:87:ce4e:1295:6cfb:900:f8a1) kuribas |
| 2025-01-28 18:38:01 +0100 | tavare | (~tavare@user/tavare) (Remote host closed the connection) |
| 2025-01-28 18:38:13 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-28 18:41:59 +0100 | philopsos | (~caecilius@user/philopsos) (Quit: Lost terminal) |
| 2025-01-28 18:44:50 +0100 | <ski> | mm, i see `%unique' was introduced later than the manual i read, and i forgot earlier seeing examples of it, on the wiki |
| 2025-01-28 18:47:53 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 2025-01-28 18:49:28 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-28 18:51:12 +0100 | end | (~end@user/end/x-0094621) (Ping timeout: 246 seconds) |
| 2025-01-28 18:51:54 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh |
| 2025-01-28 18:52:05 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:e9b3:4a8b:794e:b4a) (Quit: ubert) |
| 2025-01-28 18:52:37 +0100 | bcksl | (~bcksl@user/bcksl) (Ping timeout: 265 seconds) |
| 2025-01-28 18:53:06 +0100 | avidseeker | (av@user/avidseeker) (Ping timeout: 265 seconds) |
| 2025-01-28 18:53:15 +0100 | sus0 | (zero@user/zeromomentum) (Ping timeout: 252 seconds) |
| 2025-01-28 19:07:01 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 19:07:30 +0100 | kuribas | (~user@2a02:1808:87:ce4e:1295:6cfb:900:f8a1) (Ping timeout: 244 seconds) |
| 2025-01-28 19:12:14 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f20a18c6ee405b6d296.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2025-01-28 19:13:14 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 19:13:53 +0100 | bcksl | (~bcksl@user/bcksl) bcksl |
| 2025-01-28 19:14:48 +0100 | <haskellbridge> | <Bowuigi> I see, will try Delphin later |
| 2025-01-28 19:15:46 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-01-28 19:15:48 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-28 19:16:20 +0100 | end | (~end@user/end/x-0094621) end^ |
| 2025-01-28 19:16:30 +0100 | <ski> | Delphin is extension of Elphin, which was bundled with Twelf, at one point, i think |
| 2025-01-28 19:16:53 +0100 | <haskellbridge> | <sm> fr33domlover: ping |
| 2025-01-28 19:16:56 +0100 | AvengingFemme | (~avengingf@syn-074-076-186-205.res.spectrum.com) |
| 2025-01-28 19:18:02 +0100 | acidjnk_new3 | (~acidjnk@p200300d6e7283f203076ec74f0f78e66.dip0.t-ipconnect.de) acidjnk |
| 2025-01-28 19:18:35 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 19:19:57 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-01-28 19:20:50 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Remote host closed the connection) |
| 2025-01-28 19:20:59 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds) |
| 2025-01-28 19:21:14 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-28 19:22:44 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 2025-01-28 19:23:14 +0100 | AvengingFemme | (~avengingf@syn-074-076-186-205.res.spectrum.com) (Quit: My Mac has gone to sleep. ZZZzzz…) |
| 2025-01-28 19:23:20 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 272 seconds) |
| 2025-01-28 19:24:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 19:27:47 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-01-28 19:28:59 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-01-28 19:32:48 +0100 | sreaming | (~screaming@37.48.95.216) |
| 2025-01-28 19:33:08 +0100 | <ski> | (older page at <https://web.archive.org/web/20041218030402/http://www.cs.yale.edu/homes/delphin/>) |
| 2025-01-28 19:34:25 +0100 | kuribas | (~user@2a02:1808:87:ce4e:ed8d:3f59:612a:12d6) kuribas |
| 2025-01-28 19:36:06 +0100 | <jle`> | hm...is there a nice `ConstM` type? `newtype ConstM w m a = CostM (m w)` |
| 2025-01-28 19:36:39 +0100 | <jle`> | where ConstM x <> ConstM y = ConstM ((<>) <$> x <*> y) |
| 2025-01-28 19:37:02 +0100 | <jle`> | maybe Const . Ap |
| 2025-01-28 19:39:00 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) wootehfoot |
| 2025-01-28 19:39:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 19:44:08 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2025-01-28 19:46:45 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-01-28 19:47:05 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 19:48:51 +0100 | gehmehgeh | (~user@user/gehmehgeh) gehmehgeh |
| 2025-01-28 19:51:38 +0100 | gehmehgeh | gmg |
| 2025-01-28 19:51:43 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 244 seconds) |
| 2025-01-28 19:52:04 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-01-28 19:53:14 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-28 19:53:55 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |
| 2025-01-28 19:55:24 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2025-01-28 19:58:41 +0100 | lol_ | (~lol@2603:3016:1e01:b9c0:1941:93e:5ca4:6d26) |
| 2025-01-28 19:59:31 +0100 | EvanR_ | (~EvanR@user/evanr) EvanR |
| 2025-01-28 19:59:39 +0100 | kuribas` | (~user@ptr-17d51epnlr9u1hv5k0s.18120a2.ip6.access.telenet.be) kuribas |
| 2025-01-28 20:00:24 +0100 | ell2 | (~ellie@user/ellie) ellie |
| 2025-01-28 20:00:29 +0100 | edmundnoble_ | (sid229620@id-229620.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 2025-01-28 20:00:29 +0100 | albet70 | (~xxx@2400:8905::f03c:92ff:fe60:98d8) (Ping timeout: 260 seconds) |
| 2025-01-28 20:00:29 +0100 | Hobbyboy | (Hobbyboy@hobbyboy.co.uk) (Ping timeout: 260 seconds) |
| 2025-01-28 20:00:29 +0100 | coldmountain | (sid484352@id-484352.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 2025-01-28 20:00:29 +0100 | idnar | (sid12240@debian/mithrandi) (Ping timeout: 260 seconds) |
| 2025-01-28 20:00:51 +0100 | edmundnoble_ | (sid229620@id-229620.helmsley.irccloud.com) edmundnoble_ |
| 2025-01-28 20:01:14 +0100 | kuribas | (~user@2a02:1808:87:ce4e:ed8d:3f59:612a:12d6) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:15 +0100 | [dpk] | (~dpk@jains.nonceword.org) |
| 2025-01-28 20:01:17 +0100 | loonycyborg_ | (loonycybor@chat.chantal.wesnoth.org) |
| 2025-01-28 20:01:39 +0100 | aniketd | (32aa4844cd@2a03:6000:1812:100::dcb) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:39 +0100 | whereiseveryone | (206ba86c98@2a03:6000:1812:100::2e4) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:39 +0100 | probie | (cc0b34050a@user/probie) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:39 +0100 | jleightcap | (7bc4014b62@user/jleightcap) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:39 +0100 | beaky | (~beaky@2a03:b0c0:0:1010::1e:a001) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:39 +0100 | shawwwn | (sid6132@id-6132.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:39 +0100 | sa1 | (sid7690@id-7690.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 2025-01-28 20:01:50 +0100 | beaky | (~beaky@2a03:b0c0:0:1010::1e:a001) beaky |
| 2025-01-28 20:02:14 +0100 | jcarpenter2 | (~lol@2603:3016:1e01:b9c0:f81e:e0f5:bc3d:aa5) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | EvanR | (~EvanR@user/evanr) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | tt12310978324354 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | mustafa | (sid502723@rockylinux/releng/mustafa) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | ZLima12 | (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | dpk | (~dpk@jains.nonceword.org) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | loonycyborg | (loonycybor@wesnoth/developer/loonycyborg) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | Pent | (sid313808@id-313808.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | ell | (~ellie@user/ellie) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | bwe | (~bwe@2a01:4f8:1c1c:4878::2) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:14 +0100 | Hafydd | (~Hafydd@user/hafydd) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:15 +0100 | bailsman | (~ejrietvel@revspace/participant/bailsman) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:15 +0100 | integral | (sid296274@user/integral) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:15 +0100 | ell2 | ell |
| 2025-01-28 20:02:49 +0100 | GdeVolpi1 | (~GdeVolpia@user/GdeVolpiano) (Ping timeout: 260 seconds) |
| 2025-01-28 20:02:50 +0100 | Hobbyboy | (Hobbyboy@hobbyboy.co.uk) Hobbyboy |
| 2025-01-28 20:02:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 20:03:02 +0100 | sprotte24 | (~sprotte24@p200300d16f3179007dc10aa53878022c.dip0.t-ipconnect.de) |
| 2025-01-28 20:03:13 +0100 | jleightcap | (7bc4014b62@user/jleightcap) jleightcap |
| 2025-01-28 20:03:14 +0100 | whereiseveryone | (206ba86c98@2a03:6000:1812:100::2e4) whereiseveryone |
| 2025-01-28 20:03:14 +0100 | aniketd | (32aa4844cd@2a03:6000:1812:100::dcb) aniketd |
| 2025-01-28 20:03:20 +0100 | probie | (cc0b34050a@user/probie) probie |
| 2025-01-28 20:03:32 +0100 | bwe | (~bwe@2a01:4f8:1c1c:4878::2) bwe |
| 2025-01-28 20:03:33 +0100 | coldmountain | (sid484352@id-484352.helmsley.irccloud.com) coldmountain |
| 2025-01-28 20:03:35 +0100 | shawwwn | (sid6132@id-6132.helmsley.irccloud.com) shawwwn |
| 2025-01-28 20:03:36 +0100 | mustafa | (sid502723@rockylinux/releng/mustafa) mustafa |
| 2025-01-28 20:03:40 +0100 | Pent | (sid313808@id-313808.lymington.irccloud.com) Pent____ |
| 2025-01-28 20:03:40 +0100 | integral | (sid296274@user/integral) integral |
| 2025-01-28 20:03:43 +0100 | ejrietveld | (~ejrietvel@revspace/participant/bailsman) bailsman |
| 2025-01-28 20:03:54 +0100 | ZLima12 | (~zlima12@user/meow/ZLima12) ZLima12 |
| 2025-01-28 20:04:14 +0100 | sa1 | (sid7690@id-7690.ilkley.irccloud.com) sa1 |
| 2025-01-28 20:04:14 +0100 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) GdeVolpiano |
| 2025-01-28 20:04:49 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-01-28 20:05:51 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-28 20:06:41 +0100 | albet70 | (~xxx@2400:8905::f03c:92ff:fe60:98d8) |
| 2025-01-28 20:06:55 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds) |
| 2025-01-28 20:06:55 +0100 | tnt2 | tnt1 |
| 2025-01-28 20:07:46 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 20:08:20 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 20:11:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 20:12:32 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 20:14:43 +0100 | idnar | (sid12240@debian/mithrandi) idnar |
| 2025-01-28 20:15:15 +0100 | Midjak | (~MarciZ@82.66.147.146) Midjak |
| 2025-01-28 20:16:49 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 20:17:27 +0100 | Hafydd | (~Hafydd@user/hafydd) Hafydd |
| 2025-01-28 20:17:29 +0100 | sus0 | (zero@user/zeromomentum) zeromomentum |
| 2025-01-28 20:19:17 +0100 | comonad | (~comonad@p200300d027182d00bcfd40be9d94d2dc.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-01-28 20:20:43 +0100 | [dpk] | dpk |
| 2025-01-28 20:23:47 +0100 | <jle`> | that works well enough i guess |
| 2025-01-28 20:27:14 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 20:31:11 +0100 | zero | (~z@user/zero) (Quit: quit) |
| 2025-01-28 20:32:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 20:33:44 +0100 | Digitteknohippie | (~user@user/digit) Digit |
| 2025-01-28 20:34:48 +0100 | Digit | (~user@user/digit) (Ping timeout: 246 seconds) |
| 2025-01-28 20:34:53 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-28 20:36:00 +0100 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-01-28 20:38:57 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-01-28 20:38:57 +0100 | ljdarj1 | ljdarj |
| 2025-01-28 20:43:02 +0100 | jespada | (~jespada@2800:a4:2250:6800:688f:56e1:ca:6e8f) (Quit: Textual IRC Client: www.textualapp.com) |
| 2025-01-28 20:43:05 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 20:45:30 +0100 | jespada | (~jespada@2800:a4:2250:6800:992d:f351:2e1c:1416) jespada |
| 2025-01-28 20:47:44 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-01-28 20:52:36 +0100 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2025-01-28 20:57:44 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 20:58:18 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-01-28 20:58:27 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit) |
| 2025-01-28 20:58:49 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 21:00:00 +0100 | caconym | (~caconym@user/caconym) (Quit: bye) |
| 2025-01-28 21:00:40 +0100 | caconym | (~caconym@user/caconym) caconym |
| 2025-01-28 21:01:45 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 246 seconds) |
| 2025-01-28 21:03:30 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-01-28 21:05:31 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2025-01-28 21:14:38 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 21:16:54 +0100 | zero | (~z@user/zero) zero |
| 2025-01-28 21:19:52 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-01-28 21:20:01 +0100 | jrm | (~jrm@user/jrm) (Quit: ciao) |
| 2025-01-28 21:21:31 +0100 | jrm | (~jrm@user/jrm) jrm |
| 2025-01-28 21:27:18 +0100 | <jle`> | i forgot if ghc does CSE or not |
| 2025-01-28 21:28:05 +0100 | <geekosaur> | not very |
| 2025-01-28 21:28:46 +0100 | <jle`> | i guess when in doubt just explicitly pull out the let? |
| 2025-01-28 21:28:54 +0100 | <geekosaur> | yep |
| 2025-01-28 21:29:03 +0100 | <jle`> | i guess auto-cse could affect space usage in a weird way |
| 2025-01-28 21:30:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 21:31:16 +0100 | <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 |
| 2025-01-28 21:31:17 +0100 | <lambdabot> | error: |
| 2025-01-28 21:31:17 +0100 | <lambdabot> | • Couldn't match expected type ‘Int’ with actual type ‘Expr’ |
| 2025-01-28 21:31:17 +0100 | <lambdabot> | • In the first argument of ‘take’, namely ‘n’ |
| 2025-01-28 21:35:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-01-28 21:36:45 +0100 | Me-me | (~me-me@kc.randomserver.name) (Changing host) |
| 2025-01-28 21:36:45 +0100 | Me-me | (~me-me@user/me-me) Me-me |
| 2025-01-28 21:39:30 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2025-01-28 21:41:19 +0100 | jrm | (~jrm@user/jrm) (Quit: ciao) |
| 2025-01-28 21:42:46 +0100 | jrm | (~jrm@user/jrm) jrm |
| 2025-01-28 21:46:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 21:47:10 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 21:50:06 +0100 | <monochrom> | I saw some CSE done by GHC, but yeah it's rare. |
| 2025-01-28 21:50:40 +0100 | <monochrom> | OTOH for some reason Oleg saw much more, and it hurt his use cases. |
| 2025-01-28 21:51:27 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-01-28 21:51:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-01-28 21:51:49 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-01-28 21:53:15 +0100 | jrm | (~jrm@user/jrm) (Quit: ciao) |
| 2025-01-28 21:53:36 +0100 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) (Quit: Bye!) |
| 2025-01-28 21:54:44 +0100 | jrm | (~jrm@user/jrm) jrm |
| 2025-01-28 21:55:05 +0100 | remedan | (~remedan@ip-62-245-108-153.bb.vodafone.cz) remedan |
| 2025-01-28 21:59:33 +0100 | jespada | (~jespada@2800:a4:2250:6800:992d:f351:2e1c:1416) (Ping timeout: 248 seconds) |
| 2025-01-28 21:59:48 +0100 | <tomsmeding> | GHC does CSE sometimes, mostly when you don't expect it, and it doesn't when you do |
| 2025-01-28 22:00:31 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-01-28 22:02:01 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 22:03:28 +0100 | jespada | (~jespada@r190-133-42-215.dialup.adsl.anteldata.net.uy) jespada |
| 2025-01-28 22:06:02 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2025-01-28 22:06:34 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-01-28 22:09:48 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.4.2) |
| 2025-01-28 22:10:34 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-01-28 22:11:48 +0100 | Digitteknohippie | Digit |
| 2025-01-28 22:16:05 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 244 seconds) |
| 2025-01-28 22:17:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 22:21:50 +0100 | lol_ | jcarpenter2 |
| 2025-01-28 22:23:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-01-28 22:24:22 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-01-28 22:24:37 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 2025-01-28 22:30:59 +0100 | notzmv | (~umar@user/notzmv) (Ping timeout: 260 seconds) |
| 2025-01-28 22:33:35 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 22:33:48 +0100 | <monochrom> | That sounds about right. :) |
| 2025-01-28 22:36:40 +0100 | <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 |
| 2025-01-28 22:37:15 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-01-28 22:38:05 +0100 | <haskellbridge> | <thirdofmay18081814goya> is there a recursion scheme I should look into for a lookup operation on a tree of labeled nodes? |
| 2025-01-28 22:38:15 +0100 | <int-e> | (If you *need* sharing, use `let`.) |
| 2025-01-28 22:38:20 +0100 | notzmv | (~umar@user/notzmv) notzmv |
| 2025-01-28 22:38:24 +0100 | <haskellbridge> | <thirdofmay18081814goya> so given a string and a tree of labeled nodes, return the first subtree that matches the string |
| 2025-01-28 22:38:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> or return some subtree that matches the string |
| 2025-01-28 22:39:04 +0100 | <tomsmeding> | binary tree search or the first hit in an pre-order (or in-order?) traversal? |
| 2025-01-28 22:39:07 +0100 | <int-e> | how does a subtree match a string |
| 2025-01-28 22:39:35 +0100 | <haskellbridge> | <thirdofmay18081814goya> tomsmeding: structural recursion over rose tree |
| 2025-01-28 22:39:51 +0100 | <tomsmeding> | I repeat my question :p |
| 2025-01-28 22:40:10 +0100 | <haskellbridge> | <thirdofmay18081814goya> structural recursion over inductively defined rosetree |
| 2025-01-28 22:40:13 +0100 | <haskellbridge> | <thirdofmay18081814goya> so uh |
| 2025-01-28 22:40:17 +0100 | <haskellbridge> | <thirdofmay18081814goya> I'm not sure |
| 2025-01-28 22:40:17 +0100 | <tomsmeding> | I was asking _which_ hit you want, not what the tree is defined like |
| 2025-01-28 22:40:29 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 22:40:52 +0100 | Square2 | (~Square4@user/square) Square |
| 2025-01-28 22:40:52 +0100 | <tomsmeding> | what if you search for "a" and the tree contains "a" 5 times? Which do you want to get? |
| 2025-01-28 22:41:05 +0100 | <tomsmeding> | Is that even valid? (It might not be if you intend this to be a binary search tree) |
| 2025-01-28 22:41:19 +0100 | <int-e> | What if the string is "aaa"? Does that also produce matches? |
| 2025-01-28 22:41:30 +0100 | <int-e> | We're asking for a specification. |
| 2025-01-28 22:41:37 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-01-28 22:42:47 +0100 | <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)" |
| 2025-01-28 22:43:08 +0100 | <int-e> | but wtf is a match |
| 2025-01-28 22:43:22 +0100 | <haskellbridge> | <thirdofmay18081814goya> a subtree satisfies the condition if "Tree nodeString _ _" and "mystring = givenString" |
| 2025-01-28 22:43:45 +0100 | <haskellbridge> | <thirdofmay18081814goya> i meant if it matches "Node nodeString _ _" and "nodeString = givenString" |
| 2025-01-28 22:43:49 +0100 | Square | (~Square@user/square) (Ping timeout: 248 seconds) |
| 2025-01-28 22:44:40 +0100 | <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? |
| 2025-01-28 22:44:41 +0100 | <haskellbridge> | <thirdofmay18081814goya> as a first approximation i'd be interested in any method that does this in any order |
| 2025-01-28 22:44:51 +0100 | <tomsmeding> | is this even valid? |
| 2025-01-28 22:44:53 +0100 | <haskellbridge> | <thirdofmay18081814goya> with any match |
| 2025-01-28 22:45:00 +0100 | <tomsmeding> | you first have to decide what you _want_ :p |
| 2025-01-28 22:45:08 +0100 | <tomsmeding> | what's the X problem here? |
| 2025-01-28 22:45:24 +0100 | <haskellbridge> | <thirdofmay18081814goya> determining whether you can solve this with a catamorphism |
| 2025-01-28 22:45:46 +0100 | <tomsmeding> | you probably can |
| 2025-01-28 22:45:50 +0100 | <int-e> | A source of confusion here is that strings can be concatenated. So "matching" grows some extra dimensions of freedom. |
| 2025-01-28 22:45:52 +0100 | <haskellbridge> | <thirdofmay18081814goya> this constraint might limit what sort of match or order we might be able to get |
| 2025-01-28 22:46:04 +0100 | michalz | (~michalz@185.246.207.193) (Remote host closed the connection) |
| 2025-01-28 22:46:21 +0100 | <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 |
| 2025-01-28 22:47:35 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-01-28 22:47:47 +0100 | <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. |
| 2025-01-28 22:48:32 +0100 | <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. |
| 2025-01-28 22:49:17 +0100 | <haskellbridge> | <thirdofmay18081814goya> well the issue is we expect a tree to be returned |
| 2025-01-28 22:49:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> and as we fold there's no way to stop with just a fold |
| 2025-01-28 22:49:42 +0100 | <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. |
| 2025-01-28 22:50:12 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Quit: Client closed) |
| 2025-01-28 22:50:36 +0100 | <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 |
| 2025-01-28 22:50:47 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) |
| 2025-01-28 22:51:05 +0100 | <tomsmeding> | goya: https://play.haskell.org/saved/KMCLVKww |
| 2025-01-28 22:51:08 +0100 | <monochrom> | Lazy evaluation easily stops early when something is found. |
| 2025-01-28 22:51:15 +0100 | <tomsmeding> | what monochrom says |
| 2025-01-28 22:51:25 +0100 | <monochrom> | > foldr (&&) undefined (False : undefined) |
| 2025-01-28 22:51:27 +0100 | <lambdabot> | False |
| 2025-01-28 22:51:31 +0100 | <c_wraith> | Yeah, you don't need to work for that. You need to work to avoid it. |
| 2025-01-28 22:51:32 +0100 | <monochrom> | Stops early. |
| 2025-01-28 22:51:38 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-01-28 22:52:00 +0100 | <haskellbridge> | <thirdofmay18081814goya> oh neat |
| 2025-01-28 22:52:03 +0100 | <haskellbridge> | <thirdofmay18081814goya> will be studying that example |
| 2025-01-28 22:52:08 +0100 | <tomsmeding> | use Maybe instead of [] to get only the first / last / ... match |
| 2025-01-28 22:52:23 +0100 | <monochrom> | Oh! To avoid lazy evaluation, just lift to liftA2 (&&) for a suitable Applicative instance. >:) |
| 2025-01-28 22:52:42 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2025-01-28 22:53:10 +0100 | <int-e> | strictly awful? |
| 2025-01-28 22:53:16 +0100 | <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 |
| 2025-01-28 22:53:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm I see |
| 2025-01-28 22:53:33 +0100 | <tomsmeding> | to do better in terms of space usage, you'll have to augment the folder |
| 2025-01-28 22:53:38 +0100 | <haskellbridge> | <thirdofmay18081814goya> thanks a lot for the example! |
| 2025-01-28 22:53:55 +0100 | <tomsmeding> | :) |
| 2025-01-28 22:54:48 +0100 | <c_wraith> | monochrom: paramorphisms can be an efficiency win, even if they have the same computational power as catamorphisms. |
| 2025-01-28 22:54:58 +0100 | Googulator | (~Googulato@2a01-036d-0106-1666-e945-fd21-b920-9aa7.pool6.digikabel.hu) (Client Quit) |
| 2025-01-28 22:55:06 +0100 | <c_wraith> | (at least in a non-strict language) |
| 2025-01-28 22:55:44 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds) |
| 2025-01-28 22:55:44 +0100 | tnt2 | tnt1 |
| 2025-01-28 22:56:39 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-01-28 22:57:02 +0100 | Midjak | (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep) |
| 2025-01-28 22:57:31 +0100 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 2025-01-28 22:59:01 +0100 | <EvanR_> | monochrom, stuff like recursion schemes might fall under programming geography |
| 2025-01-28 22:59:43 +0100 | <EvanR_> | the effect of code on humans and vice versa |
| 2025-01-28 23:00:50 +0100 | <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. |