Newest at the top
| 2025-04-20 22:07:06 +0200 | <haskellbridge> | <hellwolf> maybe you give an example, and let me give it a try and learn? |
| 2025-04-20 22:06:46 +0200 | haritz | (~hrtz@user/haritz) (Ping timeout: 265 seconds) |
| 2025-04-20 22:05:55 +0200 | <haskellbridge> | <hellwolf> why not? it's just lambda with linear arrows. You would need to take care of dup/ignore data to produce valid diagrams; the type system forces you anyways. |
| 2025-04-20 22:03:55 +0200 | <haskellbridge> | <hellwolf> I am curious. I don't know the answer. |
| 2025-04-20 22:03:53 +0200 | <monochrom> | Or maybe I assumed it didn't matter. The question I would ask: Can I obtain compositional reasoning from linear temporal logic? |
| 2025-04-20 22:02:29 +0200 | <monochrom> | Maybe I did. |
| 2025-04-20 22:02:03 +0200 | <haskellbridge> | <hellwolf> Do you assume laziness cannot be obtained from linear temporal logic? |
| 2025-04-20 22:01:59 +0200 | <monochrom> | Sure! Now "take n (repeat ())" takes Theta(n)-time. |
| 2025-04-20 22:01:35 +0200 | <mauke> | why do I need a statement about repeat ()? |
| 2025-04-20 22:01:26 +0200 | <lambdabot> | [] |
| 2025-04-20 22:01:25 +0200 | <mauke> | > take 0 undefined |
| 2025-04-20 22:00:30 +0200 | <monochrom> | (I did, it's my PhD thesis: https://www.cs.utoronto.ca/~trebla/albert-thesis-ut.pdf ) |
| 2025-04-20 21:59:17 +0200 | <monochrom> | How do you prove that in Haskell "take 0 (repeat ())" is O(1)-time, without a whole-program analysis of the the "take 0 (repeat ())"? Can you just prove one statement about "take 0", and one statement about "repeat ()", and combine them to deduce O(1)-time? |
| 2025-04-20 21:57:52 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-04-20 21:57:36 +0200 | <monochrom> | People like eager languages because running times are compositional. The running time of "take 0 . repeat" is factorable to (time of take 0) + (time of repeat) = infinity. |
| 2025-04-20 21:54:46 +0200 | <haskellbridge> | <hellwolf> At least you didn't say it's false. I feel relieved :D |
| 2025-04-20 21:54:41 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-20 21:53:33 +0200 | <monochrom> | That is tautological. |
| 2025-04-20 21:53:03 +0200 | <haskellbridge> | In some cases, when timeless equations are of advantage, denotational semantics is really great; but the moment you want to deal with performance, or worse, side effects, inevitably you need the help from the "timely" logic. |
| 2025-04-20 21:53:03 +0200 | <haskellbridge> | <hellwolf> I am still conceiving this idea. And I am puching above my weight: |
| 2025-04-20 21:51:02 +0200 | <haskellbridge> | <hellwolf> it's just boxes and wires with very rigorous rules. |
| 2025-04-20 21:50:58 +0200 | <monochrom> | Compositional reasoning means if I want to prove "foo . bar" correct for example, I can break it down into proving a statement about foo, a statement about bar, and a combination of them to obtain overall correctness. |
| 2025-04-20 21:50:48 +0200 | <haskellbridge> | linear-logic and symmetric monoidal category can represent operations in quite simple diagrams. |
| 2025-04-20 21:50:48 +0200 | <haskellbridge> | <hellwolf> You sure? |
| 2025-04-20 21:50:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-20 21:50:37 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-20 21:48:53 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-20 21:48:51 +0200 | <monochrom> | OK here is why my preference, but I can't speak for others. It is easier to do compositional reasoning in denotational semantics than in operational semantics. |
| 2025-04-20 21:48:35 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-20 21:43:51 +0200 | <monochrom> | Then don't. |
| 2025-04-20 21:42:51 +0200 | <monochrom> | (not serious answer) Even physics is now trying to get rid of time from really fundamental theories >:) |
| 2025-04-20 21:42:32 +0200 | <haskellbridge> | <hellwolf> Somehow when it involves "sequence" and timeliness, it becomes dirty. I cannot justify it anymore. |
| 2025-04-20 21:41:34 +0200 | ljdarj1 | ljdarj |
| 2025-04-20 21:41:34 +0200 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds) |
| 2025-04-20 21:41:33 +0200 | <haskellbridge> | <hellwolf> This is my linear-time temporal logic take on the meaning of "par", "pseq phi psi": $\neg \psi_{whnf}\ \mathcal{U}\ \phi_{whnf}$ This is mathematics, too, you know, why this is less "simple and elegant". |
| 2025-04-20 21:40:56 +0200 | <monochrom> | I won't defend "low level is direct, high level abstract is clean", although I am mathematically inclined and I feel that way. But then I am happy to get low level, unless when I'm too lazy to. |
| 2025-04-20 21:40:28 +0200 | <int-e> | sounds subjective to me, so there is no good answer |
| 2025-04-20 21:40:22 +0200 | <haskellbridge> | <hellwolf> almost a pure aesthetic preference. |
| 2025-04-20 21:40:03 +0200 | <haskellbridge> | <hellwolf> all the answer I got from denotational conalists are usually about "simple and elegance" |
| 2025-04-20 21:39:07 +0200 | <haskellbridge> | <hellwolf> What makes encoding timeliness in computation as logic less "clean" than timeless denotational meanings? I used to be a "conalist", too. But now I am questioning and want to understand more. |
| 2025-04-20 21:38:18 +0200 | ljdarj1 | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-04-20 21:38:11 +0200 | inca | (~inca@h213.233.30.71.dynamic.ip.windstream.net) |
| 2025-04-20 21:37:46 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds) |
| 2025-04-20 21:35:58 +0200 | <monochrom> | Or even downright evil, spawn two threads to evaluate x and y concurrently, and wait for both. Just to try bringing down your computer. |
| 2025-04-20 21:35:02 +0200 | <monochrom> | For example, suppose a sick compiler decides that "seq x y" means evaluate y first, then evaluate x, then return the result of y. Then it satisfies the strictness requirement but totally defeats John Hughes's contribution. |
| 2025-04-20 21:33:48 +0200 | <monochrom> | John Hughes said, in an interview, that his contribution was adding one thing to fix the problem like foldl using up too much space because pointlessly lazy. That must be seq. And yet, for the purpose of saving space, you must talk dirty about evaluation order and not hide behind clean denotational strictness "oh order is not guaranteed". |
| 2025-04-20 21:32:31 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-20 21:31:50 +0200 | euleritian | (~euleritia@dynamic-176-006-141-238.176.6.pool.telefonica.de) |
| 2025-04-20 21:31:09 +0200 | <haskellbridge> | <hellwolf> "strict evaluation quirk" I am making stuff up for fun. |
| 2025-04-20 21:30:47 +0200 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |