Newest at the top
| 2025-03-24 22:35:29 +0100 | <EvanR> | I was going to write a similar piece of code to convert a stack into a list but forwards |
| 2025-03-24 22:34:45 +0100 | <tomsmeding> | yes |
| 2025-03-24 22:34:40 +0100 | <EvanR> | the initial stack is where you can do root exploits |
| 2025-03-24 22:34:27 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-03-24 22:33:26 +0100 | <tomsmeding> | point being that as long as there are enough Justs before Nothings to make sure you never "pop into" the initial stack s, you can determine the output of 'check' purely from your law |
| 2025-03-24 22:33:00 +0100 | <tomsmeding> | list of instructions, essentially |
| 2025-03-24 22:32:52 +0100 | <tomsmeding> | Just is a push, Nothing is a pop |
| 2025-03-24 22:32:46 +0100 | <EvanR> | what is this [Maybe a] |
| 2025-03-24 22:32:01 +0100 | <tomsmeding> | yes, the output is reversed, and no I don't care |
| 2025-03-24 22:31:47 +0100 | petrichor | (~znc-user@user/petrichor) petrichor |
| 2025-03-24 22:31:26 +0100 | <tomsmeding> | claim: the behaviour of 'check' pins down the entire semantics of Stack: check :: Stack a -> [Maybe a] -> [a]; checks s = snd . foldl' (\(s', out) -> maybe (let (y,s'') = pop s' in (s'',y:out)) (flip push s')) (s, []) |
| 2025-03-24 22:31:13 +0100 | yangby | (~secret@115.205.72.232) yangby |
| 2025-03-24 22:29:43 +0100 | cipherrot | (~znc-user@user/petrichor) (Read error: Connection reset by peer) |
| 2025-03-24 22:28:39 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-03-24 22:25:42 +0100 | <EvanR> | semantically |
| 2025-03-24 22:25:31 +0100 | <EvanR> | push 9 (push 8 (...)) |
| 2025-03-24 22:25:22 +0100 | <EvanR> | becomes |
| 2025-03-24 22:25:21 +0100 | <EvanR> | push 9 (pop! (push 7 (push 8 (...)))) |
| 2025-03-24 22:24:57 +0100 | <EvanR> | define pop! = snd . pop |
| 2025-03-24 22:23:59 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-24 22:21:45 +0100 | <EvanR> | push 9 (push 8 (...)) |
| 2025-03-24 22:21:30 +0100 | <EvanR> | let (x, xs) = pop (push 7 (push 8 (...)) in push 9 xs |
| 2025-03-24 22:19:49 +0100 | petrichor | (~znc-user@user/petrichor) (Ping timeout: 248 seconds) |
| 2025-03-24 22:18:51 +0100 | <EvanR> | and you're left with the final state of the stack |
| 2025-03-24 22:18:41 +0100 | <EvanR> | somehow |
| 2025-03-24 22:18:36 +0100 | <EvanR> | a push next to a pop cancels |
| 2025-03-24 22:18:29 +0100 | <EvanR> | inventing notation to make that sequence of calls easy to see |
| 2025-03-24 22:17:21 +0100 | infohazards | (~user@user/fmira) fmira |
| 2025-03-24 22:17:20 +0100 | <tomsmeding> | so for semantics, you only need to look at all such sequences |
| 2025-03-24 22:17:15 +0100 | cipherrot | (~znc-user@user/petrichor) petrichor |
| 2025-03-24 22:17:03 +0100 | <tomsmeding> | EvanR: important observation, which was implicit in my first reply, is that push and pop each take and return exactly one stack, so any "history" of a stack is a linear sequence of pushes and pops |
| 2025-03-24 22:16:44 +0100 | kh0d | (~kh0d@212.200.65.82) (Ping timeout: 244 seconds) |
| 2025-03-24 22:15:18 +0100 | <EvanR> | push x xs = x : x : xs, ok, this fails the law |
| 2025-03-24 22:13:56 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds) |
| 2025-03-24 22:13:08 +0100 | <EvanR> | I'll ignore the empty stack for now xD |
| 2025-03-24 22:12:57 +0100 | <sprout> | EvanR: if you don't have a 'stack_empty?' predicate you'll probably need to keep track of it yourself somehow |
| 2025-03-24 22:12:36 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-03-24 22:12:00 +0100 | <tomsmeding> | Athas: 7x slower than baseline is indeed slow, but if it's 'ad' that achieves that, I'd call that a win |
| 2025-03-24 22:12:00 +0100 | <sprout> | EvanR: but how would you keep track? |
| 2025-03-24 22:11:53 +0100 | kh0d | (~kh0d@212.200.65.82) kh0d |
| 2025-03-24 22:11:46 +0100 | <sprout> | EvanR: assuming that you're only interested in popping what you once pushed |
| 2025-03-24 22:11:39 +0100 | <EvanR> | I'll ignore the empty stack for now |
| 2025-03-24 22:11:33 +0100 | <Athas> | tomsmeding: yes, 'ad'. And maybe more like 7x. |
| 2025-03-24 22:11:24 +0100 | <sprout> | EvanR: I don't think you need the infinite stack |
| 2025-03-24 22:11:24 +0100 | <Rembane> | 5x slower than C++ is very fast imho |
| 2025-03-24 22:11:19 +0100 | <tomsmeding> | Athas: only 5x? And that's with 'ad'? |
| 2025-03-24 22:10:35 +0100 | <EvanR> | because looking bad might indicate something is actually bad and needs improvement |
| 2025-03-24 22:10:09 +0100 | <Athas> | Although on the largest workloads it's only about 5x slower than C++. |
| 2025-03-24 22:10:05 +0100 | <EvanR> | unless it's haskell |
| 2025-03-24 22:09:51 +0100 | acidjnk | (~acidjnk@p200300d6e71c4f84f984511b1aacfb73.dip0.t-ipconnect.de) acidjnk |