Newest at the top
| 2024-12-22 17:45:51 +0100 | <ski> | albet70 : sounds like coroutines |
| 2024-12-22 17:45:37 +0100 | <haskellbridge> | <thirdofmay18081814goya> woah thank you very much for the extensive comments! I'm studying these |
| 2024-12-22 17:45:19 +0100 | toch | (toch@user/toch) toch |
| 2024-12-22 17:44:38 +0100 | <ski> | (or, if we want to restrict to single conclusions, just : if `[] Gamma , A |- <> B', then `[] Gamma , <> A |- <> B') |
| 2024-12-22 17:44:37 +0100 | toch | (toch@user/toch) (Quit: WeeChat 4.5.0) |
| 2024-12-22 17:42:45 +0100 | <ski> | and, symmetrically, we can have a rule that if `[] Gamma , A |- <> Delta', then `[] Gamma , <> A |- <> Delta' |
| 2024-12-22 17:40:35 +0100 | <ski> | left it means "and" roughly)) |
| 2024-12-22 17:40:29 +0100 | <ski> | more generally, one can have a rule that if `[] Gamma |- A' (where `Gamma' is a collection of hypotheses considered conjunctively, and `[] Gamma' means `[]' applied to each one of them, individually), then `[] Gamma |- [] A' (or even : if `[] Gamma |- A , <> Delta', then `[] Gamma |- [] A , <> Delta', where `Delta' is a collection taken disjunctively (`,' on the right of `|-' means "or" roughly, while to the |
| 2024-12-22 17:40:18 +0100 | tnt2 | tnt1 |
| 2024-12-22 17:40:17 +0100 | tnt1 | (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds) |
| 2024-12-22 17:39:48 +0100 | tnt2 | (~Thunderbi@user/tnt1) tnt1 |
| 2024-12-22 17:38:36 +0100 | gmg | (~user@user/gehmehgeh) (Ping timeout: 264 seconds) |
| 2024-12-22 17:38:15 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-12-22 17:37:34 +0100 | <ski> | necessarily, `A' still holds, so `B' is also still holds), and then we can derive `[] A |- [] B' (when `A' holds even necessarily, `B' will then also hold necessarily). first step is comonadic unit (`extract'). second step is comonadic "preservation" (`(<<=)', `(=>>)') |
| 2024-12-22 17:37:28 +0100 | <ski> | thirdofmay18081814goya : if `[]' represents "necessity" of some kind (alethic ("necessary"), temporal ("always","henceforth/hereafter","hitherto/heretofore"), epistemic ("is known by me"), doxastic ("is believed by me", deontic ("obligatory"), provability ("is provable in the formal system"), ..), then if we assume `A |- B' holds, then we can derive `[] A |- B' (under the stronger condition of `A' holding |
| 2024-12-22 17:33:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 17:32:15 +0100 | <ski> | (`return'). second step is monadic extension (`(=<<)', `(>>=)'/"bind") |
| 2024-12-22 17:31:23 +0100 | <ski> | we can derive `A |- <> B' (under the condition of `A', `B' holds, so `B' is possible), and then we can derive `<> A |- <> B' (should `A' hold only possibly, `B' will then still hold possibly). first step is monadic unit |
| 2024-12-22 17:31:17 +0100 | <ski> | thirdofmay18081814goya : if `<>' represents "possibility" of some kind (alethic ("possible"), temporal ("sometimes","eventually/later","earlier/before"), epistemic ("is consistent with my knowledge / might hold for all i know"), doxastic ("is consistent with my belief", deontic ("permissible"), provability ("is consistent with derivability in the formal system"), ..), then if we assume `A |- B' holds, then |
| 2024-12-22 17:25:19 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-12-22 17:25:07 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 252 seconds) |
| 2024-12-22 17:22:54 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-12-22 17:20:50 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) alecs |
| 2024-12-22 17:19:24 +0100 | roosterphant | (~roosterph@185.21.217.76) |
| 2024-12-22 17:19:12 +0100 | swistak | (~swistak@185.21.216.141) |
| 2024-12-22 17:19:01 +0100 | roosterphant_ | (~roosterph@185.21.217.76) (Remote host closed the connection) |
| 2024-12-22 17:18:55 +0100 | swistak | (~swistak@185.21.216.141) (Quit: bye bye) |
| 2024-12-22 17:18:35 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 17:07:45 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-12-22 17:07:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> ski: I see! ty |
| 2024-12-22 17:04:26 +0100 | <albet70> | what that is called? |
| 2024-12-22 17:03:23 +0100 | <albet70> | like it capture k1 inside f, then call g with k1, then capture g's rest as k2, it jumps to k1 with k2 |
| 2024-12-22 17:03:14 +0100 | <int-e> | . o O ( deadlocks are bad, let's starve instead ) |
| 2024-12-22 17:03:12 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-12-22 17:02:54 +0100 | <geekosaur> | otherwise you risk deadlocks |
| 2024-12-22 17:02:25 +0100 | <geekosaur> | anyway, AIUI one shared var in entire program is atomicModifyIORef, one shared between two given threads is MVar, anything more requires something more complex and STM is preferred these days |
| 2024-12-22 17:02:09 +0100 | <albet70> | I learned scheme a few years ago, I saw a article about call/cc to do coroutine, it can jump between two functions with variable, but I can't find that article now |
| 2024-12-22 17:01:21 +0100 | <ski> | thirdofmay18081814goya : "possible"-type modalities would be the ones which could be monadic, while "neccesary"-type ones could be comonadic |
| 2024-12-22 17:01:15 +0100 | <int-e> | MutVar# != MVar# (MutVar# is STRef/IORef) |
| 2024-12-22 17:00:26 +0100 | <geekosaur> | but it's a very low level thing |
| 2024-12-22 17:00:08 +0100 | <geekosaur> | well, not primitive, MutVar# is the primitive |
| 2024-12-22 16:59:54 +0100 | <geekosaur> | it's a primitive synchronization variable |
| 2024-12-22 16:59:03 +0100 | <albet70> | what mvar is based on? |
| 2024-12-22 16:53:03 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-12-22 16:52:13 +0100 | <probie> | If it's just a single variable, `MVar`s might be sufficient |
| 2024-12-22 16:51:42 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-12-22 16:51:32 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 265 seconds) |
| 2024-12-22 16:47:25 +0100 | Digit | (~user@user/digit) Digit |
| 2024-12-22 16:47:13 +0100 | <geekosaur> | STM is the usual method |
| 2024-12-22 16:45:09 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |