Newest at the top
| 2025-03-24 23:13:51 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-24 23:05:41 +0100 | kh0d | (~kh0d@212.200.65.82) (Ping timeout: 248 seconds) |
| 2025-03-24 23:03:20 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2025-03-24 23:03:08 +0100 | Sgeo | (~Sgeo@user/sgeo) Sgeo |
| 2025-03-24 23:01:00 +0100 | kh0d | (~kh0d@212.200.65.82) kh0d |
| 2025-03-24 22:58:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-24 22:56:48 +0100 | target_i | (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 2025-03-24 22:54:37 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-03-24 22:54:16 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-03-24 22:52:47 +0100 | <EvanR> | answer: no |
| 2025-03-24 22:46:28 +0100 | takuan | (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection) |
| 2025-03-24 22:45:49 +0100 | JuanDaugherty | (~juan@user/JuanDaugherty) JuanDaugherty |
| 2025-03-24 22:45:11 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2025-03-24 22:45:09 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 244 seconds) |
| 2025-03-24 22:43:10 +0100 | <EvanR> | can you somehow prove the opposite law |
| 2025-03-24 22:42:39 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2025-03-24 22:42:12 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2025-03-24 22:41:09 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-24 22:39:46 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-03-24 22:37:44 +0100 | <tomsmeding> | I'm saying that the behaviour of 'check' pins down the semantics of 'Stack' (modulo initial/empty stack), not that every invocation of 'check' says something meaningful |
| 2025-03-24 22:37:35 +0100 | michalz | (~michalz@185.246.207.221) (Remote host closed the connection) |
| 2025-03-24 22:36:57 +0100 | <EvanR> | as long as the [Maybe a] isn't infinite |
| 2025-03-24 22:36:37 +0100 | <tomsmeding> | but neither does the output order :p |
| 2025-03-24 22:36:19 +0100 | <tomsmeding> | which, like, doesn't matter for my claim |
| 2025-03-24 22:36:08 +0100 | <tomsmeding> | then you process the list of instructions in reverse |
| 2025-03-24 22:35:53 +0100 | <EvanR> | is just using foldr instead of foldl' enough |
| 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 |