| 2024-05-16 00:00:22 +0200 | gamja19 | (~gamja@103.166.150.118) |
| 2024-05-16 00:01:32 +0200 | gamja19 | (~gamja@103.166.150.118) (Client Quit) |
| 2024-05-16 00:01:55 +0200 | gamja17 | (~gamja@103.166.150.118) |
| 2024-05-16 00:02:11 +0200 | phma_ | phma |
| 2024-05-16 00:02:29 +0200 | gamja17 | (~gamja@103.166.150.118) (Write error: Broken pipe) |
| 2024-05-16 00:02:49 +0200 | mailman03 | (~mailman03@103.166.150.118) |
| 2024-05-16 00:02:53 +0200 | qqq | (~qqq@92.43.167.61) (Remote host closed the connection) |
| 2024-05-16 00:03:48 +0200 | sixfourtwelve | (~ethanmorg@pnwn-04-b2-v4wan-162727-cust211.vm43.cable.virginm.net) () |
| 2024-05-16 00:04:12 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Quit: WeeChat 4.1.2) |
| 2024-05-16 00:10:17 +0200 | zzz | (~yin@user/zero) |
| 2024-05-16 00:13:12 +0200 | mailman03 | (~mailman03@103.166.150.118) (Quit: Client closed) |
| 2024-05-16 00:13:37 +0200 | mailman03 | (~mailman03@103.166.150.118) |
| 2024-05-16 00:23:43 +0200 | mailman03 | (~mailman03@103.166.150.118) (Ping timeout: 250 seconds) |
| 2024-05-16 00:27:32 +0200 | zzz | (~yin@user/zero) (Ping timeout: 252 seconds) |
| 2024-05-16 00:32:01 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc380dd5b841c8115985.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2024-05-16 00:35:29 +0200 | yin | (~yin@user/zero) |
| 2024-05-16 00:39:57 +0200 | mei | (~mei@user/mei) (Remote host closed the connection) |
| 2024-05-16 00:40:22 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 255 seconds) |
| 2024-05-16 00:41:05 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc38a510b4bd44380922.dip0.t-ipconnect.de) |
| 2024-05-16 00:42:20 +0200 | mei | (~mei@user/mei) |
| 2024-05-16 00:49:03 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection timed out) |
| 2024-05-16 00:50:46 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-05-16 00:53:32 +0200 | yin | (~yin@user/zero) (Killed (NickServ (GHOST command used by yin_))) |
| 2024-05-16 01:02:04 +0200 | aku | (~aku@65.108.245.241) (Remote host closed the connection) |
| 2024-05-16 01:02:43 +0200 | aku | (~aku@65.108.245.241) |
| 2024-05-16 01:03:15 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-05-16 01:05:33 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 255 seconds) |
| 2024-05-16 01:09:56 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-16 01:12:49 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-05-16 01:41:06 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-05-16 01:48:49 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 2024-05-16 01:49:30 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-16 01:51:07 +0200 | acidjnk_new | (~acidjnk@p200300d6e714dc38a510b4bd44380922.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2024-05-16 01:54:50 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 2024-05-16 01:59:50 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-05-16 02:11:59 +0200 | troydm | (~troydm@user/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 2024-05-16 02:40:05 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) (Ping timeout: 256 seconds) |
| 2024-05-16 02:41:39 +0200 | visilii | (~visilii@188.254.110.43) (Read error: Connection reset by peer) |
| 2024-05-16 02:42:14 +0200 | visilii | (~visilii@217.107.125.158) |
| 2024-05-16 02:48:36 +0200 | <Axman6> | IORef + atomicModifyIORef['] is actually a very useful tool for concurrent programs which also has quite good performance |
| 2024-05-16 02:50:29 +0200 | <Axman6> | Hmm, I shoudl check timestamps before replying to discussions from last night =) |
| 2024-05-16 02:52:39 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 255 seconds) |
| 2024-05-16 02:59:31 +0200 | yin_ | (~yin@user/zero) |
| 2024-05-16 03:09:02 +0200 | otto_s | (~user@p5de2fa8d.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2024-05-16 03:10:55 +0200 | otto_s | (~user@p4ff27827.dip0.t-ipconnect.de) |
| 2024-05-16 03:17:32 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 260 seconds) |
| 2024-05-16 03:21:33 +0200 | philopsos | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) |
| 2024-05-16 03:25:29 +0200 | xff0x | (~xff0x@2405:6580:b080:900:8cc9:e47c:f89a:15ee) (Ping timeout: 268 seconds) |
| 2024-05-16 03:25:43 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) |
| 2024-05-16 03:26:51 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:e61a:851b:d7b:27e8) |
| 2024-05-16 03:34:03 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:a104:ac74:dd16:a7df) (Ping timeout: 256 seconds) |
| 2024-05-16 03:38:02 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Quit: Lost terminal) |
| 2024-05-16 03:39:35 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-16 03:40:13 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Quit: leaving) |
| 2024-05-16 03:41:25 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-16 03:47:16 +0200 | bilegeek | (~bilegeek@2600:1008:b010:1cfe:3776:17b8:1dc2:3fdf) |
| 2024-05-16 03:52:56 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:e61a:851b:d7b:27e8) (Ping timeout: 268 seconds) |
| 2024-05-16 03:53:14 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 256 seconds) |
| 2024-05-16 04:00:11 +0200 | Axman6 | (~Axman6@user/axman6) (Server closed connection) |
| 2024-05-16 04:05:00 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-05-16 04:12:35 +0200 | td_ | (~td@i53870936.versanet.de) (Ping timeout: 256 seconds) |
| 2024-05-16 04:12:42 +0200 | discuss9128 | (~discuss91@137.132.213.131) |
| 2024-05-16 04:14:01 +0200 | td_ | (~td@i53870936.versanet.de) |
| 2024-05-16 04:25:21 +0200 | gorignak | (~gorignak@user/gorignak) |
| 2024-05-16 04:33:36 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:7d90:75c4:66ca:204a) |
| 2024-05-16 04:39:59 +0200 | yin_ | (~yin@user/zero) (Ping timeout: 252 seconds) |
| 2024-05-16 04:43:13 +0200 | terrorjack | (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 2024-05-16 04:46:06 +0200 | terrorjack | (~terrorjac@2a01:4f8:c17:87f8::) |
| 2024-05-16 04:51:41 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 240 seconds) |
| 2024-05-16 05:06:59 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Ping timeout: 272 seconds) |
| 2024-05-16 05:14:11 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-05-16 05:30:37 +0200 | discuss9128 | (~discuss91@137.132.213.131) (Quit: Client closed) |
| 2024-05-16 05:32:48 +0200 | ystael | (~ystael@user/ystael) |
| 2024-05-16 05:37:30 +0200 | ystael | (~ystael@user/ystael) (Ping timeout: 256 seconds) |
| 2024-05-16 05:45:21 +0200 | Axman6 | (~Axman6@user/axman6) |
| 2024-05-16 05:50:24 +0200 | EvanR | (~EvanR@user/evanr) (Ping timeout: 255 seconds) |
| 2024-05-16 05:53:41 +0200 | aforemny_ | (~aforemny@2001:9e8:6cd4:e700:d233:e5e6:582d:855) |
| 2024-05-16 05:54:30 +0200 | aforemny | (~aforemny@2001:9e8:6ced:bf00:55ed:d004:4aaa:1f0a) (Ping timeout: 256 seconds) |
| 2024-05-16 06:07:40 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:7d90:75c4:66ca:204a) (Ping timeout: 268 seconds) |
| 2024-05-16 06:09:38 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-05-16 06:15:30 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-16 06:16:20 +0200 | Square | (~Square@user/square) |
| 2024-05-16 06:20:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-05-16 06:23:39 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-16 06:24:19 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:913:214a:315:2891) |
| 2024-05-16 06:32:57 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 2024-05-16 06:35:57 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-16 06:42:49 +0200 | causal | (~eric@50.35.88.207) |
| 2024-05-16 06:42:49 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds) |
| 2024-05-16 06:48:44 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-16 06:51:13 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-05-16 06:56:43 +0200 | gorignak | (~gorignak@user/gorignak) (Quit: quit) |
| 2024-05-16 07:00:08 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:913:214a:315:2891) (Ping timeout: 260 seconds) |
| 2024-05-16 07:02:39 +0200 | philopsos | (~caecilius@pool-71-183-97-38.nycmny.fios.verizon.net) (Remote host closed the connection) |
| 2024-05-16 07:03:16 +0200 | philopsos | (~caecilius@user/philopsos) |
| 2024-05-16 07:12:01 +0200 | jjnkn | (~jjnkn@46.150.73.222.kyiv.volia.net) |
| 2024-05-16 07:12:05 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 256 seconds) |
| 2024-05-16 07:19:31 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-05-16 07:19:35 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-05-16 07:20:18 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-05-16 07:20:43 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 256 seconds) |
| 2024-05-16 07:28:47 +0200 | jinsun | (~jinsun@user/jinsun) |
| 2024-05-16 07:30:04 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-05-16 07:40:44 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-05-16 07:41:49 +0200 | euleritian | (~euleritia@dynamic-176-006-196-153.176.6.pool.telefonica.de) |
| 2024-05-16 08:00:42 +0200 | sroso | (~sroso@user/SrOso) |
| 2024-05-16 08:03:31 +0200 | acidjnk | (~acidjnk@p200300d6e714dc32b43b4fa4bda78a3a.dip0.t-ipconnect.de) |
| 2024-05-16 08:11:25 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:a189:af79:61c5:4ba2) |
| 2024-05-16 08:16:23 +0200 | superbil | (~superbil@1-34-176-171.hinet-ip.hinet.net) (Quit: WeeChat 4.2.2) |
| 2024-05-16 08:19:14 +0200 | internatetional | (~nate@2001:448a:20a3:c2e5:9ba2:a48e:b934:7d97) |
| 2024-05-16 08:30:09 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b940:9e16:4716:cb0d:9d39) (Read error: Connection reset by peer) |
| 2024-05-16 08:32:26 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-05-16 08:36:28 +0200 | internatetional | (~nate@2001:448a:20a3:c2e5:9ba2:a48e:b934:7d97) (Quit: WeeChat 4.2.2) |
| 2024-05-16 08:36:41 +0200 | internatetional | (~nate@2001:448a:20a3:c2e5:9ba2:a48e:b934:7d97) |
| 2024-05-16 08:44:39 +0200 | fendor | (~fendor@2a02:8388:1605:ce00:24e2:c141:1f86:a346) |
| 2024-05-16 08:44:51 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-05-16 08:47:48 +0200 | m1dnight | (~christoph@82.146.125.185) (Quit: WeeChat 4.2.2) |
| 2024-05-16 08:48:13 +0200 | califax | (~califax@user/califx) |
| 2024-05-16 08:48:29 +0200 | m1dnight | (~christoph@82.146.125.185) |
| 2024-05-16 08:49:24 +0200 | califax | (~califax@user/califx) (Read error: Connection reset by peer) |
| 2024-05-16 08:50:36 +0200 | kuribas | (~user@2a02:1808:2:a50c:ee7a:245e:1a98:7ade) |
| 2024-05-16 08:51:28 +0200 | califax | (~califax@user/califx) |
| 2024-05-16 08:55:51 +0200 | Square2 | (~Square4@user/square) |
| 2024-05-16 08:58:09 +0200 | ft | (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-05-16 08:58:10 +0200 | Square | (~Square@user/square) (Ping timeout: 246 seconds) |
| 2024-05-16 09:00:11 +0200 | <tomsmeding> | the memory model thing with IORefs indeed refers to the methods outside of the atomic* family |
| 2024-05-16 09:00:33 +0200 | <tomsmeding> | atomicModifyIORef is a great building block for concurrent programs, but sometimes you need more |
| 2024-05-16 09:00:37 +0200 | kuribas` | (~user@2a02:1808:8:dd22:98a8:ccd5:a4c3:db95) |
| 2024-05-16 09:01:27 +0200 | <tomsmeding> | in concurrency terminology, atomicModifyIORef is non-blocking, which means a certain progress guarantee for your program (as long as you don't go implementing a lock yourself using atomicModifyIORef, which is possible) |
| 2024-05-16 09:02:07 +0200 | kuribas | (~user@2a02:1808:2:a50c:ee7a:245e:1a98:7ade) (Ping timeout: 255 seconds) |
| 2024-05-16 09:02:13 +0200 | <tomsmeding> | many concurrent algorithms can be written in a non-blocking way (there's even a theorem that "all" can, in some sense, iirc), but that's not always the most efficient or most understandable way |
| 2024-05-16 09:02:41 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-05-16 09:03:05 +0200 | <tomsmeding> | having transactions sometimes relieves you of a whole lot of trouble in designing your data structures and methods |
| 2024-05-16 09:06:00 +0200 | euleritian | (~euleritia@dynamic-176-006-196-153.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-05-16 09:06:18 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-16 09:08:08 +0200 | <Axman6> | yeah definitely, and can also lead to less contention on shared values - the difference between n IORef (Map Key Value) and Map Key (IORef value) (or even IORef (Map Key (IORef Value)) might make significant performance differences. |
| 2024-05-16 09:08:57 +0200 | kuribas` | (~user@2a02:1808:8:dd22:98a8:ccd5:a4c3:db95) (Ping timeout: 256 seconds) |
| 2024-05-16 09:09:40 +0200 | <c_wraith> | that last one is dangerous |
| 2024-05-16 09:10:14 +0200 | <c_wraith> | It's begging to introduce race conditions |
| 2024-05-16 09:11:56 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-05-16 09:13:09 +0200 | <Axman6> | it can be used safely, you just wrap things in a safe interface |
| 2024-05-16 09:15:20 +0200 | <Axman6> | getRefForKey outer key = do exists <- Map.lookup key <$> readIORef ref; case exists of Nothing -> do newRef <- newIORef; atomicModifyIORef ref (\old -> case Map.lookup key old of Nothing -> (Map.insert key newRef, newRef); Just race -> (old, race)) |
| 2024-05-16 09:15:37 +0200 | <c_wraith> | I'm not even sure it can be used safely. If you look at the Map and determine you need to insert a new key/value pair, you can't do that from within an atomicModifyIORef |
| 2024-05-16 09:16:28 +0200 | <Axman6> | (missing `old` in the Map.insert but that should work) |
| 2024-05-16 09:16:46 +0200 | <Axman6> | oh and the Just case for the first case uses the value returned |
| 2024-05-16 09:17:14 +0200 | <Axman6> | this also assumes you never delete keys (use Maybe (IORef Value)) then) |
| 2024-05-16 09:17:43 +0200 | <c_wraith> | It also assumes you never have two threads trying to insert the same key at the same time. |
| 2024-05-16 09:17:53 +0200 | <tomsmeding> | c_wraith: I think Axman6 meant `IORef (Map Key (IORef Value))` |
| 2024-05-16 09:18:03 +0200 | <tomsmeding> | judging from the getRefForKey code |
| 2024-05-16 09:18:08 +0200 | <Axman6> | yes |
| 2024-05-16 09:18:10 +0200 | <c_wraith> | so do I |
| 2024-05-16 09:18:30 +0200 | <tomsmeding> | oh hm fair |
| 2024-05-16 09:18:42 +0200 | <tomsmeding> | time-of-check to time-of-use race condition |
| 2024-05-16 09:19:21 +0200 | <Axman6> | the code above should handle that fine, since it uses atomicModifyIORef in the update case, only one of the can put their key in |
| 2024-05-16 09:19:46 +0200 | <tomsmeding> | interesting |
| 2024-05-16 09:19:49 +0200 | <Axman6> | of the threads* |
| 2024-05-16 09:20:00 +0200 | <Axman6> | but in the case where the key exists no synchronisation is needed |
| 2024-05-16 09:20:20 +0200 | <tomsmeding> | neat |
| 2024-05-16 09:20:27 +0200 | <tomsmeding> | gets you a limited interface though, to the map |
| 2024-05-16 09:20:31 +0200 | <tomsmeding> | but if that's enough, it's nice |
| 2024-05-16 09:20:44 +0200 | <tomsmeding> | also needs a read-heavy workload |
| 2024-05-16 09:21:05 +0200 | <Axman6> | yeah - which my one use case for this particular design was =) |
| 2024-05-16 09:21:39 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-05-16 09:21:41 +0200 | <Axman6> | actually that's not true, since things were only read when a uses used the webservice, which no one ever did =) |
| 2024-05-16 09:22:17 +0200 | <tomsmeding> | :D |
| 2024-05-16 09:22:25 +0200 | <tomsmeding> | write-light, then |
| 2024-05-16 09:23:57 +0200 | frumon | (~Frumon@user/Frumon) |
| 2024-05-16 09:27:07 +0200 | <c_wraith> | Ok, it works on the assumption that the value you want to insert doesn't depend on whether there was already a key there or not (or depends trivially, with some sort of commutative operation) |
| 2024-05-16 09:27:45 +0200 | _bo | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) |
| 2024-05-16 09:28:09 +0200 | <tomsmeding> | I that would be a requirement from the interface of getRefForKey anyway, regardless of the implementation |
| 2024-05-16 09:28:37 +0200 | <c_wraith> | You're adding extra semantics. I'm looking at the type. :P |
| 2024-05-16 09:29:12 +0200 | <tomsmeding> | I'm looking at an idealised implementation in terms of `MVar (Map Key Value)` |
| 2024-05-16 09:29:28 +0200 | kuribas` | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-05-16 09:29:30 +0200 | <tomsmeding> | and observing that this cleverer implementation does not have stronger preconditions than the MVar-based one |
| 2024-05-16 09:30:31 +0200 | <c_wraith> | in practice, an MVar-based implementation will perform way better with heavy writes. |
| 2024-05-16 09:30:38 +0200 | <tomsmeding> | of course |
| 2024-05-16 09:30:46 +0200 | <tomsmeding> | hence the "write-light" observed above |
| 2024-05-16 09:30:55 +0200 | bo_ | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) (Ping timeout: 256 seconds) |
| 2024-05-16 09:32:35 +0200 | <c_wraith> | and a TVar-based approach lets you write much more obviously-correct code that works under the write-light conditions. |
| 2024-05-16 09:33:02 +0200 | <tomsmeding> | with slightly more overhead |
| 2024-05-16 09:33:31 +0200 | <tomsmeding> | but true |
| 2024-05-16 09:36:41 +0200 | bilegeek | (~bilegeek@2600:1008:b010:1cfe:3776:17b8:1dc2:3fdf) (Quit: Leaving) |
| 2024-05-16 09:42:21 +0200 | oo_miguel | (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 2024-05-16 09:44:11 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 09:46:51 +0200 | <kuribas`> | perhaps offtopic, but I looked at twelf, and I am surprised you need to reinvent equality (refl, cong, ...) for each datatype. |
| 2024-05-16 09:49:30 +0200 | <kuribas`> | https://twelf.org/wiki/equality/ |
| 2024-05-16 09:56:54 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-05-16 10:02:03 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-05-16 10:02:54 +0200 | titibandit | (~user@user/titibandit) |
| 2024-05-16 10:03:14 +0200 | danza | (~francesco@an-19-164-164.service.infuturo.it) |
| 2024-05-16 10:15:27 +0200 | danza | (~francesco@an-19-164-164.service.infuturo.it) (Remote host closed the connection) |
| 2024-05-16 10:16:46 +0200 | <ski> | kuribas` : aiui, no parametric polymorphism, types only depend on values, not types; iirc, in original implementation, they had that, but they didn't include it in the reworked implementation (yet at least), because the theory for it was unclear |
| 2024-05-16 10:17:40 +0200 | <kuribas`> | ski: so types are not values then? |
| 2024-05-16 10:18:19 +0200 | <ski> | there are three levels, values, types, and kinds |
| 2024-05-16 10:19:01 +0200 | <ski> | (in LF, the Logical Framework system, that Elf is based on, and of which Twelf is an implementation of) |
| 2024-05-16 10:19:22 +0200 | <kuribas`> | Twelf is dependently typed Elf? |
| 2024-05-16 10:19:35 +0200 | <ski> | no, LF is dependently typed to begin with |
| 2024-05-16 10:19:44 +0200 | <ski> | bu there's no infinite tower of sorts |
| 2024-05-16 10:20:15 +0200 | <ski> | it's a fairly conservative/restrictive theory |
| 2024-05-16 10:20:24 +0200 | <kuribas`> | right, no type 1, type 2, ... as in idris2 |
| 2024-05-16 10:20:54 +0200 | <ski> | yep |
| 2024-05-16 10:22:36 +0200 | <ski> | aiui, this is because (a) they purposely want a rather weak theory, to not assume too much, when representing object systems (logics, type systems, operational semantics, &c.); but also (b) in order to keep unification and type checking decidable |
| 2024-05-16 10:24:19 +0200 | <ski> | (they have unification of lambda terms, up to alpha-, beta-, and eta- conversion. but lambda terms are rather weak, can't compute on sum types, and no recursion. you do computation not with functions, but with predicates/relations, iow logic programming, searching for proofs/values of propositions/types) |
| 2024-05-16 10:25:53 +0200 | <ski> | (i may be missing some detail, or getting some details wrong, but that's my impression, from reading some papers about it, semi-recently .. still need to play around more in the implementation, though) |
| 2024-05-16 10:32:39 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) |
| 2024-05-16 10:37:04 +0200 | frumon | (~Frumon@user/Frumon) (Leaving) |
| 2024-05-16 10:40:45 +0200 | _bo | (~bo@198.red-83-56-252.dynamicip.rima-tde.net) (Quit: Leaving) |
| 2024-05-16 10:41:05 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-05-16 10:42:28 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 255 seconds) |
| 2024-05-16 10:45:06 +0200 | chele | (~chele@user/chele) |
| 2024-05-16 10:48:19 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d028:ce6d:23c1:c5bb) |
| 2024-05-16 10:48:21 +0200 | <int-e> | You have to restrict beta for this to be decidable (unification can guess arguments of unbounded size so termination doesn't save you). https://www.cs.cmu.edu/~twelf/guide-1-4/twelf_5.html#SEC27 mentions higher-order pattern unification which IIRC doesn't have beta, and also doesn't guess the head of applications. The type checking/inference might have something a bit more fancy though. |
| 2024-05-16 10:51:23 +0200 | <ski> | yes, the unification is restricted |
| 2024-05-16 10:52:10 +0200 | <ski> | it has beta_0 |
| 2024-05-16 10:53:52 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-16 10:54:09 +0200 | <ski> | (the rules for how it's restricted are somewhat complicated. i read the L-lambda unification paper, and also the details of which unifications are allowed in Twelf, but i don't recall the details of either that well) |
| 2024-05-16 10:54:54 +0200 | ski | idly wonders whether something like L-lambda / higher-order pattern unification, could sensibly be added to GHC |
| 2024-05-16 10:54:55 +0200 | <int-e> | Now what do I google to figure out what beta_0 is :) |
| 2024-05-16 10:55:10 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) |
| 2024-05-16 10:55:21 +0200 | <ski> | basically `(\x. M) y', substituting `x' with another variable `y' |
| 2024-05-16 10:55:54 +0200 | <ski> | (well, more specifically, either with a bound variable, or with a constant. but not with a logic / meta- variable, nor with an arbitrary term) |
| 2024-05-16 10:56:06 +0200 | <int-e> | Ah, yeah supporting that makes sense to me. |
| 2024-05-16 10:56:44 +0200 | <ski> | (i think in some papers, they also allow substituting like numeric literal, (unapplied) data constructors) |
| 2024-05-16 10:57:47 +0200 | <int-e> | And I think it's a detail of the pattern unification that I forgot. Yeah I do remember support for constructors too. |
| 2024-05-16 10:58:45 +0200 | ski | read it like last month or so |
| 2024-05-16 10:59:40 +0200 | <ski> | the "unification under a mixed prefix" paper by Dale Miller is also relevant |
| 2024-05-16 11:00:09 +0200 | <ski> | .. as well as the tutorial interpreter paper for lambdaProlog (which implements that idea, amongst various other stuff) |
| 2024-05-16 11:02:22 +0200 | <ski> | (they implement in SML, using a one-level continuation-passing style. success means calling continuation deeper. failure means returning. initial continuation will print out answer substitution, and query if user wants to search for more solutions. they implement cut by throwing exception) |
| 2024-05-16 11:07:53 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-05-16 11:17:51 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:a189:af79:61c5:4ba2) (Ping timeout: 268 seconds) |
| 2024-05-16 11:20:41 +0200 | <kuribas`> | ski: it looks like lists are parametric? https://twelf.org/wiki/lists/ |
| 2024-05-16 11:21:37 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-05-16 11:21:59 +0200 | destituion | (~destituio@2a02:2121:10b:62ca:bae7:e090:21e:1459) (Ping timeout: 256 seconds) |
| 2024-05-16 11:22:50 +0200 | destituion | (~destituio@85.221.111.174) |
| 2024-05-16 11:24:47 +0200 | <ski> | "Unification Under a Mixed Prefix" by Dale Miller in 1992-07-08 at <https://www.lix.polytechnique.fr/~dale/papers/jsc92.pdf> |
| 2024-05-16 11:24:50 +0200 | <ski> | "A Semi-Functional Implementation of a Higher-Order Logic Programming Language" by Conal Elliott,Frank Pfenning in 1990-02 (draft) at <http://www.cs.cmu.edu/~fp/papers/elpsml90.pdf>,<http://www.cs.cmu.edu/~fp/papers/elpsml-paper.tar.gz> |
| 2024-05-16 11:25:30 +0200 | <ski> | kuribas` : sure, it's parametric in the sense of ML functors (parameterized modules), you can assume anything you like about the element type `elem'. but `list' has type `type', not `type -> type' |
| 2024-05-16 11:26:22 +0200 | <ski> | (so `list' itself is not a parameterized type, and relations/predicates operating over it won't be parametrically polymorphic in the element type) |
| 2024-05-16 11:26:57 +0200 | <kuribas`> | ski: If if I need 5 different types of lists, I need to load the module 5 times? |
| 2024-05-16 11:30:50 +0200 | <ski> | (btw .. an LF program is basically a signature, a list of type signatures of constants (value constants and type constants) .. you can interpret this as something quite close to an ML module signature, and then you can introduce ML module functors into the picture, implementing the constants of one signature in terms of those of another. this is e.g. useful when you specify a type system using "declarative" |
| 2024-05-16 11:30:56 +0200 | <ski> | inference rules (comprising one signature), and then also specify an alternative set of "algorithmic" inference rules (avoiding ambiguity, and allowing the type signatures to be effectively be interpreted as a logic program, something the declarative version often doesn't usefully, or at least efficiently, admit) .. and then the functor tells you how to transform a derivation in the algorithmic system (which |
| 2024-05-16 11:31:02 +0200 | <ski> | proof search automatically can find for your), into a derivation in the declarative system) |
| 2024-05-16 11:32:15 +0200 | <ski> | kuribas` : or load five (copy-pasted) versions of it. or perhaps it could be possible to parameterize the whole file on `elem', but aiui, Twelf doesn't currently implement anything like that |
| 2024-05-16 11:33:51 +0200 | barak | (~barak@2a0d:6fc2:68c1:7200:e61a:851b:d7b:27e8) |
| 2024-05-16 11:34:26 +0200 | cfricke | (~cfricke@user/cfricke) (Remote host closed the connection) |
| 2024-05-16 11:34:45 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 11:35:22 +0200 | <ski> | (i guess one should clearly distinguish here between wanting to parameterize an LF program (being a signature), and wanting to parameterize a realization of that signature (which would give a functor). what i meant to say at the end above is that i've seen papers for (and source code implementing) the latter, but not the former) |
| 2024-05-16 11:37:44 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-05-16 11:37:44 +0200 | ec | (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 2024-05-16 11:38:23 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-16 11:38:38 +0200 | ec | (~ec@gateway/tor-sasl/ec) |
| 2024-05-16 11:42:40 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:e4f7:dd84:71b6:db6) |
| 2024-05-16 11:46:26 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-05-16 11:49:41 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 11:52:10 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 2024-05-16 11:53:45 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) |
| 2024-05-16 11:56:18 +0200 | pie_ | (~pie_bnc@user/pie/x-2818909) () |
| 2024-05-16 11:56:36 +0200 | pie_ | (~pie_bnc@user/pie/x-2818909) |
| 2024-05-16 11:58:52 +0200 | libertyprime | (~libertypr@118-92-68-68.dsl.dyn.ihug.co.nz) (Remote host closed the connection) |
| 2024-05-16 12:01:38 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) (Ping timeout: 268 seconds) |
| 2024-05-16 12:02:08 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 2024-05-16 12:08:51 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 255 seconds) |
| 2024-05-16 12:13:28 +0200 | todi | (~todi@p57803331.dip0.t-ipconnect.de) |
| 2024-05-16 12:20:48 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 2024-05-16 12:21:37 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 12:23:19 +0200 | chexum | (~quassel@gateway/tor-sasl/chexum) |
| 2024-05-16 12:24:05 +0200 | patrl | (~patrl@user/patrl) |