| 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) |