| 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) |
| 2024-05-16 12:26:29 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 12:28:55 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 260 seconds) |
| 2024-05-16 12:33:26 +0200 | famubu | (~julinuser@user/famubu) |
| 2024-05-16 12:37:33 +0200 | <famubu> | Hi. I had been trying to make a megaparsec parser to parse regular expression. I got atoms and concatenation working. Now I'm trying to get repetition like `r{2,4}` but couldn't finish it. |
| 2024-05-16 12:38:01 +0200 | <famubu> | This is what I have: https://bpa.st/5O4Q |
| 2024-05-16 12:38:31 +0200 | <famubu> | I wasn't sure how to add `rep` to the operator table (`optab`) |
| 2024-05-16 12:41:15 +0200 | <famubu> | Saw this (parsec): https://stackoverflow.com/questions/9020254/using-parsec-to-parse-regular-expressions |
| 2024-05-16 12:41:39 +0200 | <famubu> | where they mention it for `+`, and `*`. But still couldn't figure how to make it more general. |
| 2024-05-16 12:44:01 +0200 | yin | (~yin@user/zero) |
| 2024-05-16 12:49:06 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:d028:ce6d:23c1:c5bb) (Remote host closed the connection) |
| 2024-05-16 12:49:14 +0200 | <tomsmeding> | famubu: `Postfix rep` doesn't work? |
| 2024-05-16 12:49:42 +0200 | <tomsmeding> | note the type of Postfix here https://hackage.haskell.org/package/parser-combinators-1.3.0/docs/Control-Monad-Combinators-Expr.h… |
| 2024-05-16 12:50:46 +0200 | <tomsmeding> | I wonder if your :- parsing is working though; should it not parse a '-'? |
| 2024-05-16 12:53:57 +0200 | neiluj | (~neiluj@193.203.71.162) |
| 2024-05-16 12:55:45 +0200 | <famubu> | Symbols are single characters. So ABC should become like `A :- B :- C`. So no need to explicitly parse a hyphen. Is that what you meant? |
| 2024-05-16 12:56:02 +0200 | <tomsmeding> | ah I see |
| 2024-05-16 12:56:04 +0200 | <tomsmeding> | sure |
| 2024-05-16 12:56:09 +0200 | <famubu> | Postfix rep didn't work. Because of the extra `Integer -> Integer`. |
| 2024-05-16 12:56:20 +0200 | <tomsmeding> | (I wasn't reading carefully and assumed (:-) was for e.g. `[a-z]` |
| 2024-05-16 12:56:22 +0200 | <tomsmeding> | ) |
| 2024-05-16 12:56:33 +0200 | <famubu> | Yeah. |
| 2024-05-16 12:56:52 +0200 | <famubu> | Rep constructor is like `Re a -> Integer -> Integer` |
| 2024-05-16 12:56:54 +0200 | rvalue | (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 2024-05-16 12:57:23 +0200 | <famubu> | This was the error: https://bpa.st/U6MQ |
| 2024-05-16 12:57:32 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-05-16 12:57:40 +0200 | <tomsmeding> | famubu: Postfix (Rep <$ rep) is not the same as Postfix rep |
| 2024-05-16 12:57:43 +0200 | <tomsmeding> | I meant the latter |
| 2024-05-16 12:57:54 +0200 | <tomsmeding> | <$ is for if you don't care about the result of 'rep' and want it to be Rep anyway |
| 2024-05-16 12:57:58 +0200 | <neiluj> | hey! ocaml guy here! I'd like to deepen my knowledge by playing with haskell advanced features such as liquid haskell, category theory stuff. Which projects/reading material would you recommend to achieve this goal? |
| 2024-05-16 12:58:00 +0200 | <tomsmeding> | but Rep is not fully applied so that fails |
| 2024-05-16 12:58:03 +0200 | <tomsmeding> | :t (<$) |
| 2024-05-16 12:58:04 +0200 | <lambdabot> | Functor f => a -> f b -> f a |
| 2024-05-16 12:58:23 +0200 | <tomsmeding> | famubu: `rep` returns useful info here so you shouldn't use (<$) |
| 2024-05-16 12:59:37 +0200 | <famubu> | Oh.. sorry. That worked. I'm not yet that good at extracting the correct info from the types.. 😬 |
| 2024-05-16 12:59:41 +0200 | <famubu> | Thanks. |
| 2024-05-16 13:00:01 +0200 | <tomsmeding> | famubu: every time you figure something like this out, you gain a little more intuition for what the types meant :) |
| 2024-05-16 13:00:08 +0200 | <famubu> | :) |
| 2024-05-16 13:00:14 +0200 | <famubu> | Yeah |
| 2024-05-16 13:02:20 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 256 seconds) |
| 2024-05-16 13:02:50 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-05-16 13:07:27 +0200 | xff0x | (~xff0x@2405:6580:b080:900:25be:f228:ec64:b69c) |
| 2024-05-16 13:12:25 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:c695:1779:f1ed:a0d3) |
| 2024-05-16 13:18:09 +0200 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2024-05-16 13:21:56 +0200 | patrl | (~patrl@user/patrl) |
| 2024-05-16 13:26:21 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 13:28:44 +0200 | patrl | (~patrl@user/patrl) |
| 2024-05-16 13:32:53 +0200 | koz | (~koz@121.99.240.58) (Ping timeout: 256 seconds) |
| 2024-05-16 13:33:27 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) (Ping timeout: 256 seconds) |
| 2024-05-16 13:34:09 +0200 | cfricke | (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2) |
| 2024-05-16 13:34:35 +0200 | koz | (~koz@121.99.240.58) |
| 2024-05-16 13:35:46 +0200 | bolivood1 | (~bolivood@2a0d:6fc2:5d10:8200:11e8:e299:e23d:e488) |
| 2024-05-16 13:37:37 +0200 | Maxdamantus | (~Maxdamant@user/maxdamantus) |
| 2024-05-16 13:37:59 +0200 | bolivood | (~bolivood@2a0d:6fc2:5d10:8200:e4f7:dd84:71b6:db6) (Ping timeout: 256 seconds) |
| 2024-05-16 13:39:43 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) |
| 2024-05-16 13:41:02 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2024-05-16 13:44:38 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) |
| 2024-05-16 13:47:31 +0200 | xdminsy | (~xdminsy@117.147.70.240) (Quit: Konversation terminated!) |
| 2024-05-16 13:47:54 +0200 | xdminsy | (~xdminsy@117.147.70.240) |
| 2024-05-16 13:57:11 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-05-16 14:04:03 +0200 | neiluj | (~neiluj@193.203.71.162) (Ping timeout: 255 seconds) |
| 2024-05-16 14:05:29 +0200 | neiluj | (~neiluj@193.203.71.162) |
| 2024-05-16 14:05:59 +0200 | danse-nr3 | (~danse-nr3@an-19-164-164.service.infuturo.it) (Read error: Connection reset by peer) |
| 2024-05-16 14:06:15 +0200 | danse-nr3 | (~danse-nr3@151.43.160.43) |
| 2024-05-16 14:19:47 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) (Ping timeout: 264 seconds) |
| 2024-05-16 14:20:23 +0200 | ezzieyguywuf | (~Unknown@user/ezzieyguywuf) |
| 2024-05-16 14:30:52 +0200 | danse-nr3 | (~danse-nr3@151.43.160.43) (Read error: Connection reset by peer) |
| 2024-05-16 14:31:07 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-05-16 14:31:09 +0200 | danse-nr3 | (~danse-nr3@151.43.160.43) |
| 2024-05-16 14:36:38 +0200 | Square2 | (~Square4@user/square) |
| 2024-05-16 14:39:14 +0200 | destituion | (~destituio@85.221.111.174) (Ping timeout: 256 seconds) |
| 2024-05-16 14:41:58 +0200 | bolivood1 | (~bolivood@2a0d:6fc2:5d10:8200:11e8:e299:e23d:e488) (Ping timeout: 268 seconds) |
| 2024-05-16 14:42:27 +0200 | destituion | (~destituio@2a02:2121:10b:62ca:10a5:f759:7fb5:9fb1) |
| 2024-05-16 14:46:05 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2024-05-16 14:47:13 +0200 | __monty__ | (~toonn@user/toonn) (Ping timeout: 268 seconds) |
| 2024-05-16 14:55:11 +0200 | neiluj | (~neiluj@193.203.71.162) (Ping timeout: 264 seconds) |
| 2024-05-16 15:06:47 +0200 | neiluj | (~neiluj@193.203.71.162) |
| 2024-05-16 15:11:23 +0200 | neiluj | (~neiluj@193.203.71.162) (Ping timeout: 252 seconds) |
| 2024-05-16 15:17:14 +0200 | neiluj | (~neiluj@193.203.71.162) |
| 2024-05-16 15:19:12 +0200 | bolivood1 | (~bolivood@2a0d:6fc2:5d10:8200:95cf:c099:dbf9:bb2d) |
| 2024-05-16 15:19:45 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-05-16 15:34:36 +0200 | ystael | (~ystael@user/ystael) |
| 2024-05-16 15:41:57 +0200 | yin | zzz |
| 2024-05-16 15:42:22 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-05-16 15:51:43 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 256 seconds) |
| 2024-05-16 15:56:22 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-05-16 15:59:45 +0200 | neiluj_ | (~neiluj@193.203.71.162) |
| 2024-05-16 16:00:47 +0200 | <Athas> | tomsmeding: does Accelerate work with CUDA 12? |
| 2024-05-16 16:02:08 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-05-16 16:02:32 +0200 | neiluj | (~neiluj@193.203.71.162) (Ping timeout: 252 seconds) |
| 2024-05-16 16:05:27 +0200 | neiluj_ | (~neiluj@193.203.71.162) (Ping timeout: 256 seconds) |
| 2024-05-16 16:05:50 +0200 | bolivood1 | (~bolivood@2a0d:6fc2:5d10:8200:95cf:c099:dbf9:bb2d) (Ping timeout: 268 seconds) |
| 2024-05-16 16:06:17 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 272 seconds) |
| 2024-05-16 16:10:51 +0200 | <tomsmeding> | Athas: no, <=11 |
| 2024-05-16 16:11:17 +0200 | <tomsmeding> | Indirectly blocked on https://github.com/visq/language-c/pull/94 |
| 2024-05-16 16:11:25 +0200 | <Athas> | That'll be an issue. |
| 2024-05-16 16:11:49 +0200 | <tomsmeding> | I think with sufficient hackery you can take that PR and build with that |
| 2024-05-16 16:12:13 +0200 | <tomsmeding> | The problem is that language-c is a dep of c2hs which is a *build-dependency* of cuda, which is a dep of accelerate |
| 2024-05-16 16:12:32 +0200 | <tomsmeding> | And a simple source-repository-package in cabal.project doesn't override build deps |
| 2024-05-16 16:12:43 +0200 | <Athas> | I hope the Accelerate/CFAL team will do that, because otherwise it will not run on the benchmarking machine. |
| 2024-05-16 16:12:59 +0200 | <tomsmeding> | I think I managed to override it at some point with sufficient vendoring |
| 2024-05-16 16:13:00 +0200 | <tomsmeding> | Ah |
| 2024-05-16 16:13:13 +0200 | <tomsmeding> | We'll have a look, but might take a few days |
| 2024-05-16 16:17:35 +0200 | EvanR | (~EvanR@user/evanr) |
| 2024-05-16 16:23:44 +0200 | billchenchina- | (~billchenc@103.152.35.21) (Remote host closed the connection) |
| 2024-05-16 16:24:12 +0200 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) |
| 2024-05-16 16:24:54 +0200 | billchenchina | (~billchenc@2a0d:2580:ff0c:1:e3c9:c52b:a429:5bfe) (Max SendQ exceeded) |
| 2024-05-16 16:25:18 +0200 | billchenchina | (~billchenc@103.152.35.21) |
| 2024-05-16 16:26:49 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-05-16 16:29:55 +0200 | neiluj | (~neiluj@193.203.71.162) |
| 2024-05-16 16:31:08 +0200 | califax | (~califax@user/califx) |
| 2024-05-16 16:35:06 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-05-16 16:38:14 +0200 | billchenchina | (~billchenc@103.152.35.21) (Remote host closed the connection) |
| 2024-05-16 16:38:47 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-05-16 16:38:56 +0200 | billchenchina | (~billchenc@103.152.35.21) |
| 2024-05-16 16:41:00 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-05-16 16:43:45 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-05-16 16:47:18 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 256 seconds) |
| 2024-05-16 16:48:17 +0200 | califax | (~califax@user/califx) |
| 2024-05-16 16:49:51 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-05-16 16:51:27 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:4e7a:622:23f0:da46) |
| 2024-05-16 16:51:27 +0200 | random-jellyfish | (~developer@2a02:2f04:11e:c600:4e7a:622:23f0:da46) (Changing host) |
| 2024-05-16 16:51:27 +0200 | random-jellyfish | (~developer@user/random-jellyfish) |
| 2024-05-16 16:51:52 +0200 | califax | (~califax@user/califx) |
| 2024-05-16 16:56:41 +0200 | Square2 | (~Square4@user/square) |
| 2024-05-16 17:02:33 +0200 | neiluj | (~neiluj@193.203.71.162) (Ping timeout: 256 seconds) |
| 2024-05-16 17:03:23 +0200 | ocra8 | (ocra8@user/ocra8) |
| 2024-05-16 17:04:30 +0200 | Guest13 | (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) |
| 2024-05-16 17:05:25 +0200 | zzz | (~yin@user/zero) (Ping timeout: 255 seconds) |
| 2024-05-16 17:08:23 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-05-16 17:10:16 +0200 | califax | (~califax@user/califx) |
| 2024-05-16 17:14:18 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-05-16 17:15:01 +0200 | califax | (~califax@user/califx) (Remote host closed the connection) |
| 2024-05-16 17:18:28 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 260 seconds) |
| 2024-05-16 17:18:33 +0200 | neiluj | (~neiluj@193.203.71.162) |
| 2024-05-16 17:18:48 +0200 | califax | (~califax@user/califx) |
| 2024-05-16 17:21:36 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 255 seconds) |
| 2024-05-16 17:23:23 +0200 | <Guest13> | hi, how can I memoize recursive calls that aren't simple like the fibonacci. I see on the wiki for memoization there is an example memo_fib= (map fib [1..] !!), but the problem I am trying to solve has the recursive calls in an order I don't necessarily know |
| 2024-05-16 17:24:21 +0200 | <Guest13> | it is the sort of problem where I would want to have a map to store previous calls |
| 2024-05-16 17:28:48 +0200 | <ski> | so use a map ? |
| 2024-05-16 17:29:08 +0200 | <ski> | .. or how large is your domain ? |
| 2024-05-16 17:30:46 +0200 | <ski> | (oh, and jfyi, that `memo_fib' still uses `fib' (but not `memo_fib') for each individual call, so not reusing the list resulting from the `map' as a cache) |
| 2024-05-16 17:32:32 +0200 | <ski> | anyway, if you already know from the start (perhaps from the initial parameters) how large domain you need for the recursive calls corresponding to subproblems of that initial problem, you can allocate a map (recursively defined) that has an association mapping each element of your domain to the corresponding result value (lazily computed) |
| 2024-05-16 17:33:37 +0200 | <ski> | .. but if your domain is large, the map would also be large. sometimes you can allocate the association structure itself, lazily, incrementally (like the infinite linked list above) |
| 2024-05-16 17:36:42 +0200 | zzz | (~yin@user/zero) |
| 2024-05-16 17:37:26 +0200 | <Guest13> | I understand to use a map but I don't know how I would implement it |
| 2024-05-16 17:38:01 +0200 | <Guest13> | I can't think about it functionally very well, I am thinking that each time it does a call it updates an internal "state" |
| 2024-05-16 17:38:24 +0200 | <Guest13> | ie adds to the map, or checks the map |
| 2024-05-16 17:38:50 +0200 | <Guest13> | I've seen the rec keyword but this is also something I am unsure about |
| 2024-05-16 17:40:41 +0200 | <ski> | there is no state, adding to the map, unless you express this with state in some fashion .. and it's probably better to avoid that, if you can |
| 2024-05-16 17:41:02 +0200 | <ski> | `rec' is for something else (recursive bindings in `do') |
| 2024-05-16 17:42:21 +0200 | <ski> | @let tabulate :: Ix i => (i,i) -> (i -> e) -> Array i e; tabulate ix f = listArray ix [f i | i <- range ix] |
| 2024-05-16 17:42:22 +0200 | <lambdabot> | Defined. |
| 2024-05-16 17:43:49 +0200 | <ski> | > L.tabulate (-2,3) (\i -> i^2) -- construct an array, with each element based on its index |
| 2024-05-16 17:43:51 +0200 | <lambdabot> | array (-2,3) [(-2,4),(-1,1),(0,0),(1,1),(2,4),(3,9)] |
| 2024-05-16 17:46:32 +0200 | <ski> | > let memoFib n | n >= 0 = fibs ! n where fibs = L.tabulate (0,n) fib; fib 0 = 0; fib 1 = 1; fib n = fibs ! (n - 1) + fibs ! (n - 2) in memoFib 12 |
| 2024-05-16 17:46:33 +0200 | <lambdabot> | 144 |
| 2024-05-16 17:48:01 +0200 | <Guest13> | the problem I have is that each recursive call is defined by [Int], Int, [Int] |
| 2024-05-16 17:48:12 +0200 | <ski> | Guest13 : can you follow that ^ example ? given a (non-negative) integer `n', it builds an array (`fibs') with `n+1' elements (indexed from `0' to `1'), with elements set by the fibonacci function (`fib') where recursive calls look up results in the array, and so will be cached (the array elements are lazily computed) |
| 2024-05-16 17:48:44 +0200 | <ski> | the array `fibs' and the function `fib' are mutually recursively defined. you can inline one into the other as |
| 2024-05-16 17:49:28 +0200 | <ski> | > let memoFib n | n >= 0 = fibs ! n where fibs = L.tabulate (0,n) (\n -> case n of 0 -> 0; 1 -> 1; n -> fibs ! (n - 1) + fibs ! (n - 2)) in memoFib 12 -- array `fibs' is (lazily) recursively defined in terms of itself |
| 2024-05-16 17:49:30 +0200 | <lambdabot> | 144 |
| 2024-05-16 17:49:36 +0200 | <Guest13> | im not sure I can, the state I have is 2 arrays which im comparing to each other and an integer to denote a counter and a string |
| 2024-05-16 17:50:00 +0200 | <Guest13> | if it helps, I can explain the problem |
| 2024-05-16 17:50:34 +0200 | <ski> | are `[Int]',`Int',`[Int]' your parameter types ? |
| 2024-05-16 17:50:57 +0200 | <ski> | are you sure you have two arrays, and not two lists ? |
| 2024-05-16 17:51:25 +0200 | <ski> | when you call recursively, which parameters (may) change ? |
| 2024-05-16 17:51:48 +0200 | <ski> | explaining it may help, possibly |
| 2024-05-16 17:51:53 +0200 | danse-nr3 | (~danse-nr3@151.43.160.43) (Remote host closed the connection) |
| 2024-05-16 17:52:17 +0200 | danse-nr3 | (~danse-nr3@151.43.160.43) |
| 2024-05-16 17:53:19 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1) |
| 2024-05-16 17:54:59 +0200 | Guest13 | (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) (Ping timeout: 250 seconds) |
| 2024-05-16 17:56:46 +0200 | jrm | (~jrm@user/jrm) (Quit: ciao) |
| 2024-05-16 17:57:22 +0200 | <EvanR> | "use a map" could be ambiguous |
| 2024-05-16 17:57:41 +0200 | <EvanR> | the function map, the Data.Map container |
| 2024-05-16 17:57:43 +0200 | <ski> | hm, i guess |
| 2024-05-16 17:57:58 +0200 | <EvanR> | both could be used for memoizing |
| 2024-05-16 17:58:17 +0200 | jrm | (~jrm@user/jrm) |
| 2024-05-16 17:58:59 +0200 | <EvanR> | at least other functionalish languages are being consistent in this jargon xD |
| 2024-05-16 17:59:12 +0200 | <EvanR> | map vs map |
| 2024-05-16 18:00:24 +0200 | <ski> | hm ? |
| 2024-05-16 18:02:32 +0200 | <EvanR> | it's been a while since I didn't know jargon but I have to wonder if noobs are confused by the collision of map function and map data structure |
| 2024-05-16 18:02:46 +0200 | <EvanR> | in not just haskell |
| 2024-05-16 18:03:26 +0200 | <dolio> | I can't recall it ever being confusing. |
| 2024-05-16 18:04:57 +0200 | danse-nr3 | (~danse-nr3@151.43.160.43) (Read error: Connection reset by peer) |
| 2024-05-16 18:04:59 +0200 | <ski> | i wonder about the etymology of the `map' function |
| 2024-05-16 18:05:21 +0200 | <ski> | did LISP 1.5 have `MAPCAR' ? |
| 2024-05-16 18:05:31 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-05-16 18:06:07 +0200 | <dolio> | I think it goes pretty far back in lisp. |
| 2024-05-16 18:09:12 +0200 | <dolio> | The lisp 1.6 manual has it. |
| 2024-05-16 18:09:43 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:c695:1779:f1ed:a0d3) (Remote host closed the connection) |
| 2024-05-16 18:10:30 +0200 | <ski> | anyway, for the data structure, surely "(finite) map" is because it's representing a "map" (or "mapping"), being a word that's basically a synonym for "function","transform", the "finite" part referring to that it has a finite domain, or that it's a partial function defined on a finite subset of the domain (sometimes representing a function with "finite support" meaning that it only maps to "nonzero" on a |
| 2024-05-16 18:10:37 +0200 | <ski> | finite subset of the domain) |
| 2024-05-16 18:11:01 +0200 | <ski> | i guess 1.5 probably does then, too |
| 2024-05-16 18:11:28 +0200 | kuribas` | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2024-05-16 18:12:07 +0200 | <ski> | if you think of the list as representing a subset, then the `map' function computes the (existential/direct) image of the function on that subset .. not sure why one would call this "map" |
| 2024-05-16 18:13:11 +0200 | <dolio> | Lists aren't subsets, though. |
| 2024-05-16 18:14:28 +0200 | <c_wraith> | is Int overflow behavior actually specified on overflow? |
| 2024-05-16 18:14:40 +0200 | <ski> | > [0,1,0,2,0,1,0,3] \\ [2,1,0] |
| 2024-05-16 18:14:42 +0200 | <lambdabot> | [0,0,1,0,3] |
| 2024-05-16 18:14:46 +0200 | <c_wraith> | wow, good sentence construction there. |
| 2024-05-16 18:14:58 +0200 | Guest13 | (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) |
| 2024-05-16 18:15:15 +0200 | <Guest13> | sorry ski I had to pick my mum up from station |
| 2024-05-16 18:15:27 +0200 | <dolio> | Anyhow, 'map' doesn't just mean 'function' it's also the act of associating or carrying an input to an output by a function. |
| 2024-05-16 18:15:58 +0200 | <Guest13> | yes, [Int] [Int] int String are the parameters |
| 2024-05-16 18:16:11 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 264 seconds) |
| 2024-05-16 18:16:20 +0200 | <Guest13> | or at least what I had in the recursive call |
| 2024-05-16 18:16:30 +0200 | <dolio> | And that's what 'map' does on all elements of some container. |
| 2024-05-16 18:16:40 +0200 | <dolio> | Lists in the case of old lisp. |
| 2024-05-16 18:16:57 +0200 | <ski> | i guess that's the connection, then |
| 2024-05-16 18:17:10 +0200 | manwithluck | (~manwithlu@149.102.244.20) (Read error: Connection reset by peer) |
| 2024-05-16 18:17:11 +0200 | <ski> | Guest13 : and which of those are actually changing ? |
| 2024-05-16 18:17:19 +0200 | <Guest13> | all of them |
| 2024-05-16 18:18:02 +0200 | <Guest13> | I can simplify it to Int Int [Int] String |
| 2024-05-16 18:18:06 +0200 | <ski> | are you sure dynamic programming would make sense, for your problem, then ? |
| 2024-05-16 18:18:21 +0200 | <Guest13> | yes, but I am probably framing it badly |
| 2024-05-16 18:18:29 +0200 | <ski> | .. or are you just looking for caching results of calls, to avoid recomputing later ? |
| 2024-05-16 18:18:33 +0200 | <Guest13> | to make it easy I just wanted to cache results of calls |
| 2024-05-16 18:18:35 +0200 | <Guest13> | yes |
| 2024-05-16 18:19:47 +0200 | <ski> | oh, and when i asked "which of those are actually changing ?", i specifically had *recursive* calls in mind (not initial/top calls from other places) |
| 2024-05-16 18:20:07 +0200 | <Guest13> | can you explain what is the difference? |
| 2024-05-16 18:20:53 +0200 | <Guest13> | the recursive call changes all of the above, and the top call I believe will start at 0 0 [Int] String |
| 2024-05-16 18:21:26 +0200 | <Guest13> | I could frame it as Int Int Int and have [Int] and String as references |
| 2024-05-16 18:22:10 +0200 | <ski> | if only some of the parameters changed in recursive calls, then you could, within a single toplevel call, only cache for the changing parameters, thereby simplifying the datastructure needed to cache results |
| 2024-05-16 18:22:24 +0200 | <Guest13> | this would be ideal |
| 2024-05-16 18:22:35 +0200 | cfricke | (~cfricke@user/cfricke) (Ping timeout: 256 seconds) |
| 2024-05-16 18:22:38 +0200 | <Guest13> | I can formulate it as Int Int Int, with constant [Int] and String |
| 2024-05-16 18:22:53 +0200 | <ski> | (for each new toplevel call, you'd generate a fresh/new cache, from scratch, whose results would only be reused for recursive calls stemming from that particular toplevel call) |
| 2024-05-16 18:24:25 +0200 | <ski> | ok, maybe it would make sense to cache in a three-dimensional array, or (if you only need sparse inputs) maybe use a `Map (Int,Int,Int) Result' or something like that (that'd still require you to know upfront which triples would be needed, which might not be ideal) |
| 2024-05-16 18:24:35 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2024-05-16 18:24:49 +0200 | <ski> | (or `Map Int (Map Int (Map Int Result))', i guess ..) |
| 2024-05-16 18:24:55 +0200 | <Guest13> | can be sparse or dense depending on input |
| 2024-05-16 18:25:20 +0200 | <Guest13> | I don't know upfront which triples are needed |
| 2024-05-16 18:25:27 +0200 | <ski> | if you're okay with a dense caching space, you could try caching with an array |
| 2024-05-16 18:26:10 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-05-16 18:26:32 +0200 | <ski> | but if your ranges (?) of `Int's are large, the array would contain a lot of elements, take a lot of space (the array itself would be allocated eagerly, only the array elements would be lazily evaluated) |
| 2024-05-16 18:27:00 +0200 | <Guest13> | the ranges aren't large |
| 2024-05-16 18:27:20 +0200 | <Guest13> | at most like 20 |
| 2024-05-16 18:27:21 +0200 | <ski> | so, maybe try `Array (Int,Int,Int) Result' ? |
| 2024-05-16 18:27:31 +0200 | <Guest13> | ok, how can I use this to cache |
| 2024-05-16 18:27:35 +0200 | tomboy64 | (~tomboy64@user/tomboy64) |
| 2024-05-16 18:27:45 +0200 | manwithluck | (~manwithlu@149.102.244.20) |
| 2024-05-16 18:27:57 +0200 | <Guest13> | I understand the map f [1..] for fib, and even the tabulate version you showed me but I don't understand this one |
| 2024-05-16 18:28:03 +0200 | <Guest13> | im not really doing dp |
| 2024-05-16 18:28:06 +0200 | <ski> | you can use `listArray' (or `array'), or the `tabulate' i defined above, to (lazily) populate the array with elements, based on their indices |
| 2024-05-16 18:28:54 +0200 | <ski> | oh, you said "yes, but I am probably framing it badly" just after i asked "are you sure dynamic programming would make sense, for your problem, then ?", so i was taking that for granted |
| 2024-05-16 18:28:58 +0200 | <Guest13> | so I can do a \(x,y,z) -> f x y-1 z + f x-1 y z |
| 2024-05-16 18:29:20 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-05-16 18:29:25 +0200 | <Guest13> | I think I get how to do it |
| 2024-05-16 18:30:11 +0200 | <Guest13> | im trying to count the ways of doing something |
| 2024-05-16 18:31:37 +0200 | <ski> | (i guess you actually meant `f x (y-1) z + f (x-1) y z', btw) |
| 2024-05-16 18:32:10 +0200 | <Guest13> | I will have a go at this |
| 2024-05-16 18:32:25 +0200 | <Guest13> | I need to think about how to implement the "dead ends" of the recursive call |
| 2024-05-16 18:32:56 +0200 | <Guest13> | its basically a "ways if go left" + "ways if go right" recursion |
| 2024-05-16 18:33:11 +0200 | <Guest13> | and you have some calls where you say it has gone wrong and ways = 0 |
| 2024-05-16 18:34:55 +0200 | <ski> | base cases / dead ends, i guess |
| 2024-05-16 18:35:09 +0200 | <Guest13> | this would be setting the value to 0 |
| 2024-05-16 18:35:20 +0200 | <mauke> | dead ends are where the recursion dies :-) |
| 2024-05-16 18:35:38 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-05-16 18:35:53 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-05-16 18:35:55 +0200 | <Guest13> | yeah, for some reason it being in a table confused me |
| 2024-05-16 18:37:05 +0200 | <Guest13> | I think I get it though, my program will query 0 0 0 in the table which will spawn recursive calls and the base case is n m 0 = 1 |
| 2024-05-16 18:37:48 +0200 | <Guest13> | I will try this now thank you for the help ski |
| 2024-05-16 18:39:44 +0200 | <Guest13> | do I need to define my own 3d tabulate? |
| 2024-05-16 18:43:30 +0200 | <ski> | the above should work |
| 2024-05-16 18:44:55 +0200 | hueso | (~root@user/hueso) (Read error: Connection reset by peer) |
| 2024-05-16 18:45:20 +0200 | <ski> | (there are instances like `(Ix a,Ix b,Ix c) => Ix (a,b,c)') |
| 2024-05-16 18:45:44 +0200 | <ski> | > range ((0,0),(1,3)) |
| 2024-05-16 18:45:45 +0200 | <lambdabot> | [(0,0),(0,1),(0,2),(0,3),(1,0),(1,1),(1,2),(1,3)] |
| 2024-05-16 18:45:55 +0200 | <ski> | @type range |
| 2024-05-16 18:45:56 +0200 | <lambdabot> | Ix a => (a, a) -> [a] |
| 2024-05-16 18:46:05 +0200 | hueso | (~root@user/hueso) |
| 2024-05-16 18:46:08 +0200 | <Guest13> | I see |
| 2024-05-16 18:46:21 +0200 | <ski> | that's all indices in a rectangle, with upper left corner `(0,0)', lower right corner `(1,3)' |
| 2024-05-16 18:47:00 +0200 | <ski> | .. and `tabulate' calls `listArray' with a list defined using `range' to generate elements for all valid indices |
| 2024-05-16 18:47:08 +0200 | <ski> | @type listArray |
| 2024-05-16 18:47:09 +0200 | <lambdabot> | Ix i => (i, i) -> [e] -> Array i e |
| 2024-05-16 18:47:15 +0200 | <ski> | @type array |
| 2024-05-16 18:47:16 +0200 | <lambdabot> | Ix i => (i, i) -> [(i, e)] -> Array i e |
| 2024-05-16 18:48:40 +0200 | <ski> | (`listArray' is for when you just want to list the array elements (in proper index enumeration order, as given by e.g. `range'. `array' allows you to give the elements in arbitrary order, but then you have to pair up each element with its corresponding index, and it's also possible to repeat an index (in which case, iirc, it will just pick the last association pair)) |
| 2024-05-16 18:48:46 +0200 | <Guest13> | "where fibs = L.tabulate (0,n) (\n -> case n of 0 -> 0; 1 -> 1; n -> fibs ! (n - 1) + fibs ! (n - 2))" is crazy |
| 2024-05-16 18:48:58 +0200 | <ski> | it's just a recursivelt defined array |
| 2024-05-16 18:49:03 +0200 | <Guest13> | yeah I like it |
| 2024-05-16 18:49:25 +0200 | <ski> | it automatically gives you top-down dynamic programming, through lazy caching of the array elements |
| 2024-05-16 18:49:40 +0200 | <Guest13> | I can never get top down vs bottom up lol |
| 2024-05-16 18:49:52 +0200 | <Guest13> | I know one goes from leaves other from root but idk |
| 2024-05-16 18:50:16 +0200 | <ski> | bottom-up means that you start at the "base cases" of the recursion, building your way upwards. for fibonacci, this would be starting at `0' and `1' |
| 2024-05-16 18:50:43 +0200 | <Guest13> | but when you call it you start at the top? |
| 2024-05-16 18:50:51 +0200 | <Guest13> | and then work your way down to the bottom |
| 2024-05-16 18:50:55 +0200 | <Guest13> | and then back up to the top |
| 2024-05-16 18:51:01 +0200 | <ski> | it requires knowing which results will depend on which other results, so that you can make sure to initialize the latter results before the former ones need them |
| 2024-05-16 18:51:26 +0200 | <ski> | top-down means that you start at the top desired result, and then let demand determine which sub-results are actually demanded |
| 2024-05-16 18:51:54 +0200 | <Guest13> | ok so fib (n-1) + fib (n-2) is top down |
| 2024-05-16 18:51:59 +0200 | <ski> | (and those are then cached, so that if they're needed in a sibling branch of the call-tree, they won't be recomputed, but just looked up) |
| 2024-05-16 18:52:51 +0200 | <Guest13> | what is an example of bottom up, I know bottom up parsing where you look at "leaves" of the grammar and then say this must be this production rule and so on |
| 2024-05-16 18:52:58 +0200 | <Guest13> | but not other cases |
| 2024-05-16 18:53:48 +0200 | <ski> | yea. if you do `fib n = fibLoop 0 1 n where fibLoop a b 0 = a; fibLoop a !b n = fibLoop b (a + b) (n-1)', then that's bottom-up (but keeping just the last two results around, since for fibonacci we know we don't need any previous ones any longer) |
| 2024-05-16 18:54:39 +0200 | <Guest13> | ah I see |
| 2024-05-16 18:54:47 +0200 | <Guest13> | bottom up is usually better surely |
| 2024-05-16 18:54:53 +0200 | <Guest13> | if you can do it |
| 2024-05-16 18:56:01 +0200 | neiluj | (~neiluj@193.203.71.162) (Ping timeout: 256 seconds) |
| 2024-05-16 18:57:21 +0200 | <Guest13> | is it convention to put the changing values in the recursive call before or after the static ones? |
| 2024-05-16 18:57:26 +0200 | <ski> | > let memoFib n | n >= 0 = fib n where ((!) . L.tabulate (0,n) -> fib) = \case 0 -> 0; 1 -> 1; n -> fib (n-1) + fib (n-2) in memoFib 12 |
| 2024-05-16 18:57:28 +0200 | <lambdabot> | 144 |
| 2024-05-16 18:57:30 +0200 | <ski> | ^ a cute way to, instead of inlining the function `fib' into the array `fibs', inlining the array `fibs' into the function `fib', using `ViewPatterns' to pass the function `\case ...' through `L.tabulate (0,n)' (giving back an array), and then also through `(!)' (indexing the array, giving back a function), before naming that function `fib' .. while `\case ...' already uses that `fib', recursively |
| 2024-05-16 18:58:18 +0200 | <ski> | @let memoArray :: Ix i => (i,i) -> (i -> e) -> (i -> e); memoArray ix f = (L.tabulate ix f !) |
| 2024-05-16 18:58:19 +0200 | <lambdabot> | Defined. |
| 2024-05-16 18:58:35 +0200 | <ski> | > let memoFib n | n >= 0 = fib n where (memoArray (0,n) -> fib) = \case 0 -> 0; 1 -> 1; n -> fib (n-1) + fib (n-2) in memoFib 12 -- same thing, just slightly clearer |
| 2024-05-16 18:58:37 +0200 | <lambdabot> | 144 |
| 2024-05-16 19:00:39 +0200 | <Guest13> | not sure I understand this one |
| 2024-05-16 19:00:42 +0200 | <ski> | Guest13 : "bottom up is usually better surely","if you can do it" -- depends. if you know which results will be needed, beforehand, i'll probably be a little more efficient, i suppose. but if there may be large swathes of subresults that may not actually be needed, then it's hard to avoid computing them anyway with bottom-up, so in that case you may be doing quite a bit more work than for top-down |
| 2024-05-16 19:01:13 +0200 | <Guest13> | ((!) . tabulate (0,n) -> fib) = \case 0 -> 0; 1 -> 1; n -> fib (n-1) + fib (n-2) I don't understand |
| 2024-05-16 19:01:23 +0200 | <ski> | Guest13 : well, basically we just splice a memoization/caching lookup inbetween each recursive call |
| 2024-05-16 19:01:50 +0200 | <ski> | `(<expr> -> <pat>)' is a, so-called, view pattern |
| 2024-05-16 19:01:50 +0200 | <Guest13> | I don't understand the assignment |
| 2024-05-16 19:02:12 +0200 | <Guest13> | we are assigning a function to the left |
| 2024-05-16 19:02:24 +0200 | <ski> | my use of the view pattern above is rather unusual .. normally view patterns are used in function (formal) parameter patterns |
| 2024-05-16 19:02:31 +0200 | <ski> | e.g. |
| 2024-05-16 19:02:52 +0200 | <ski> | > let last (reverse -> x:_) = x in last [2,3,5,7] |
| 2024-05-16 19:02:54 +0200 | <lambdabot> | 7 |
| 2024-05-16 19:03:31 +0200 | <ski> | this will call `reverse' on the input `[2,3,5,7]', before trying to match it with the pattern `x:_'. so we actually match the list `[7,5,3,2]' with the pattern `x:_', so `x' becomes `7' |
| 2024-05-16 19:03:56 +0200 | <ski> | that example makes sense to you ? |
| 2024-05-16 19:04:17 +0200 | <Guest13> | I understand what it is doing |
| 2024-05-16 19:04:22 +0200 | <ski> | oh |
| 2024-05-16 19:04:25 +0200 | <Guest13> | but not how the syntax reflects that |
| 2024-05-16 19:04:25 +0200 | <ski> | in general |
| 2024-05-16 19:04:36 +0200 | <ski> | foo (f -> y) = ..y.. |
| 2024-05-16 19:04:41 +0200 | <Guest13> | yeah |
| 2024-05-16 19:04:49 +0200 | <ski> | can be refactored/rewritten as |
| 2024-05-16 19:04:56 +0200 | <ski> | foo x = ..y.. |
| 2024-05-16 19:04:58 +0200 | <ski> | where |
| 2024-05-16 19:05:01 +0200 | <ski> | y = f x |
| 2024-05-16 19:05:55 +0200 | <ski> | (.. except that if `y' is a complex pattern, rather than a simple variable, then failure to match that pattern will cause the whole defining equation `foo (f -> y) = ...' to fail (trying the next defining equation instead), while with the `where'-version above, this doesn't happen) |
| 2024-05-16 19:06:19 +0200 | <ski> | or, more generally, we can say that |
| 2024-05-16 19:06:23 +0200 | <ski> | (f -> y) = x |
| 2024-05-16 19:06:28 +0200 | <ski> | amounts to the same thing as |
| 2024-05-16 19:06:32 +0200 | <ski> | y = f x |
| 2024-05-16 19:07:01 +0200 | <Guest13> | I see how applying f to both sides does that |
| 2024-05-16 19:07:02 +0200 | <ski> | (input `x', matched against the view-pattern `(f -> y)', will call `f' on the input `x', and match the result of that to the pattern `y') |
| 2024-05-16 19:07:11 +0200 | <ski> | so, in my example |
| 2024-05-16 19:07:20 +0200 | <ski> | (memoArray (0,n) -> fib) = \case 0 -> 0; 1 -> 1; n -> fib (n-1) + fib (n-2) |
| 2024-05-16 19:07:26 +0200 | <ski> | this is actually the same thing as |
| 2024-05-16 19:07:36 +0200 | <ski> | fib = memoArray (0,n) (\case 0 -> 0; 1 -> 1; n -> fib (n-1) + fib (n-2)) |
| 2024-05-16 19:07:59 +0200 | <Guest13> | is there a reason to phrase it like that? |
| 2024-05-16 19:08:04 +0200 | <ski> | cuteness |
| 2024-05-16 19:08:08 +0200 | <Guest13> | lol |
| 2024-05-16 19:08:31 +0200 | <Guest13> | I understood the below one immediately but the top was super confusing lol |
| 2024-05-16 19:08:38 +0200 | <Guest13> | I think I get it now though |
| 2024-05-16 19:08:58 +0200 | <Guest13> | you are saying that to get x in (f -> x) = y you need to call f on y |
| 2024-05-16 19:09:17 +0200 | <ski> | well, we're also avoiding wrapping the whole `\case ...' in brackets. so when we break that over multiple lines in the source file, we don't need a closing bracket at the end, that may look a bit unclear which opening bracket it is matching, multiple lines up |
| 2024-05-16 19:09:35 +0200 | <ski> | it would perhaps be even more fun, if we could write |
| 2024-05-16 19:09:48 +0200 | <ski> | (memoArray (0,n) -> fib) 0 = 0 |
| 2024-05-16 19:09:51 +0200 | <ski> | (memoArray (0,n) -> fib) 1 = 1 |
| 2024-05-16 19:09:55 +0200 | <ski> | (memoArray (0,n) -> fib) n = fib (n-1) + fib (n-2) |
| 2024-05-16 19:10:24 +0200 | <Guest13> | what does memoArray do again? |
| 2024-05-16 19:10:25 +0200 | <ski> | .. but my unintended usage of view patterns, above, doesn't support this style of defining `fib' |
| 2024-05-16 19:10:45 +0200 | <Guest13> | ! . tabulate |
| 2024-05-16 19:10:47 +0200 | <ski> | (and .. it might be unclear whether there'd be only a single call to `memoArray' here, or three separate calls) |
| 2024-05-16 19:11:19 +0200 | <ski> | `tabulate (0,n)' converts the function to an array that lists the results of the function, for each input in the range `(0,n)' |
| 2024-05-16 19:11:30 +0200 | <ski> | `(!)' converts back from that array, to the function |
| 2024-05-16 19:11:42 +0200 | <Guest13> | ok ok |
| 2024-05-16 19:12:03 +0200 | <ski> | so, `(!) . tabulate (0,n)' allocates a single array, and makes a new function that, when called, will indirect through this array before calling the original function |
| 2024-05-16 19:12:26 +0200 | ft | (~ft@p508db8fc.dip0.t-ipconnect.de) |
| 2024-05-16 19:12:28 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-05-16 19:12:43 +0200 | <ski> | btw .. note that we should not use |
| 2024-05-16 19:13:07 +0200 | <ski> | fib n = memoArray (0,n) fib (n-1) + memoArray (0,n) fib (n-2) |
| 2024-05-16 19:13:08 +0200 | <ski> | or |
| 2024-05-16 19:13:18 +0200 | <ski> | fib n = fib' (n-1) + fib' (n-2) |
| 2024-05-16 19:13:20 +0200 | <ski> | where |
| 2024-05-16 19:13:32 +0200 | <ski> | fib' = memoArray (0,n) fib |
| 2024-05-16 19:13:35 +0200 | <Guest13> | because these are two different arrays |
| 2024-05-16 19:13:50 +0200 | <ski> | since this would call `memoArray' once for each recursive call, allocating a new array on each recursive call |
| 2024-05-16 19:13:58 +0200 | <Guest13> | ok I see |
| 2024-05-16 19:14:01 +0200 | <ski> | we only want to allocate an array on the initial/top call |
| 2024-05-16 19:14:15 +0200 | <Guest13> | so defining it as f -> x = y is good |
| 2024-05-16 19:14:40 +0200 | <ski> | well .. it does look a bit neat |
| 2024-05-16 19:14:56 +0200 | <ski> | of course, there's nothing wrong with naming the intermediate array cache, as well |
| 2024-05-16 19:14:58 +0200 | patrl | (~patrl@user/patrl) (Remote host closed the connection) |
| 2024-05-16 19:16:01 +0200 | <Guest13> | I gotta go cook dinner, but I will let you know how the problem goes |
| 2024-05-16 19:16:11 +0200 | <Guest13> | I think I understand it fairly well know |
| 2024-05-16 19:16:12 +0200 | <Guest13> | now |
| 2024-05-16 19:16:41 +0200 | <ski> | but i suppose one reason i played around with view patterns here (or rather, a more complcated function, involving a two-dimensional array, for matching a pattern string inside a text string), was to try to keep the memoized code version as close as possible to the original, non-memoized code |
| 2024-05-16 19:19:54 +0200 | <Guest13> | so you can reuse the non memoized code? |
| 2024-05-16 19:20:06 +0200 | <Guest13> | or separate the logic |
| 2024-05-16 19:20:08 +0200 | <ski> | no, not really |
| 2024-05-16 19:20:26 +0200 | <Guest13> | so it is clear where the memoization happens and where the recursion happens |
| 2024-05-16 19:20:28 +0200 | <ski> | but i localize the differences to a minimal numer of places |
| 2024-05-16 19:20:49 +0200 | <ski> | well .. that too. but it's not that unclear for the more elaborated versions, either |
| 2024-05-16 19:21:23 +0200 | <ski> | it's more to clearly seee that you haven't accidentally introduced some bug change in the memoized version |
| 2024-05-16 19:22:02 +0200 | <ski> | and also to easily be able to ignore the memoization when reading (when thinking about what it does, without concern for the memoization optimiztion) |
| 2024-05-16 19:22:59 +0200 | <Guest13> | (y) thank you for the help! ill see if I can let you know how my solution goes, and maybe send it to this channel at some point |
| 2024-05-16 19:23:00 +0200 | <ski> | because i keep the recursive calls `fib (n-1) + fib (n-2)', rather than replacing them with array lookups `fibs ! (n-1) + fib ! (n-2)' |
| 2024-05-16 19:23:23 +0200 | <Guest13> | its much cleaner like that |
| 2024-05-16 19:23:32 +0200 | <ski> | well .. |
| 2024-05-16 19:23:42 +0200 | <ski> | .. you should use whichever version is clearer to you |
| 2024-05-16 19:24:11 +0200 | <ski> | if you think the view pattern version is too clever, or obscure, then you probably shouldn't use it |
| 2024-05-16 19:24:47 +0200 | billchenchina | (~billchenc@103.152.35.21) (Ping timeout: 256 seconds) |
| 2024-05-16 19:43:19 +0200 | Guest13 | (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) (Ping timeout: 250 seconds) |
| 2024-05-16 19:44:48 +0200 | halloy9814 | (~halloy981@103.144.93.164) |
| 2024-05-16 19:45:09 +0200 | halloy9814 | suvid |
| 2024-05-16 19:45:15 +0200 | <suvid> | hi |
| 2024-05-16 19:46:28 +0200 | suvid | (~halloy981@103.144.93.164) (Remote host closed the connection) |
| 2024-05-16 19:50:05 +0200 | ph88 | (~ph88@2a02:8109:9e26:c800:801e:36ad:9367:33b9) |
| 2024-05-16 19:51:46 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b940:892b:2549:5c20:9c9b) |
| 2024-05-16 19:54:40 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-05-16 20:00:18 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-05-16 20:02:59 +0200 | polyphem | (~rod@p4fc2c1da.dip0.t-ipconnect.de) |
| 2024-05-16 20:06:40 +0200 | suvid | (~suvid@103.144.93.164) |
| 2024-05-16 20:07:22 +0200 | <suvid> | hi |
| 2024-05-16 20:08:05 +0200 | xnyhps | (~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288) (Ping timeout: 240 seconds) |
| 2024-05-16 20:08:19 +0200 | xnyhps | (~xnyhps@2a02:2770:3:0:216:3eff:fe67:3288) |
| 2024-05-16 20:10:21 +0200 | random-jellyfish | (~developer@user/random-jellyfish) (Ping timeout: 255 seconds) |
| 2024-05-16 20:11:42 +0200 | suvid | (~suvid@103.144.93.164) (Remote host closed the connection) |
| 2024-05-16 20:14:30 +0200 | y04nn | (~username@2a03:1b20:8:f011::e10d) |
| 2024-05-16 20:24:31 +0200 | wootehfoot | (~wootehfoo@user/wootehfoot) |
| 2024-05-16 20:38:55 +0200 | jjnkn | (~jjnkn@46.150.73.222.kyiv.volia.net) (Remote host closed the connection) |
| 2024-05-16 20:50:06 +0200 | philopsos | (~caecilius@user/philopsos) |
| 2024-05-16 20:50:34 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-05-16 20:54:41 +0200 | danse-nr3 | (~danse-nr3@151.47.136.223) |
| 2024-05-16 20:55:36 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-05-16 20:56:38 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 256 seconds) |