Newest at the top
| 2025-12-26 21:08:33 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-26 21:05:08 +0100 | marinelli | (~weechat@gateway/tor-sasl/marinelli) marinelli |
| 2025-12-26 21:04:49 +0100 | marinelli | (~weechat@gateway/tor-sasl/marinelli) (Remote host closed the connection) |
| 2025-12-26 21:02:31 +0100 | ThePenguin | (~ThePengui@cust-95-80-28-221.csbnet.se) ThePenguin |
| 2025-12-26 21:00:38 +0100 | ThePenguin | (~ThePengui@cust-95-80-28-221.csbnet.se) (Remote host closed the connection) |
| 2025-12-26 20:44:47 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-12-26 20:42:31 +0100 | karenw | (~karenw@user/karenw) karenw |
| 2025-12-26 20:35:36 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2025-12-26 20:34:55 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds) |
| 2025-12-26 20:34:18 +0100 | Lord_of_Life_ | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2025-12-26 20:22:01 +0100 | omidmash | (~omidmash@user/omidmash) omidmash |
| 2025-12-26 20:10:40 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2025-12-26 20:09:55 +0100 | <ncf> | mere christmas |
| 2025-12-26 20:04:07 +0100 | <monochrom> | About the paper. I saw "Merely Inhabited" and misread as "Merrily Inhabited". Must be the seaon holidays. Merry Inhabited Holidays! |
| 2025-12-26 19:58:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-26 19:57:11 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-12-26 19:53:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-26 19:43:01 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-26 19:42:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-12-26 19:42:50 +0100 | rainbyte | (~rainbyte@186.22.19.214) (Read error: Connection reset by peer) |
| 2025-12-26 19:42:48 +0100 | rainbyte_ | (~rainbyte@186.22.19.214) rainbyte |
| 2025-12-26 19:38:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-26 19:27:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-12-26 19:22:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-26 19:15:19 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Remote host closed the connection) |
| 2025-12-26 19:15:02 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2025-12-26 19:11:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-26 19:06:34 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-26 18:59:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-26 18:55:10 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-26 18:48:04 +0100 | tabemann | (~tabemann@12.215.215.61) (Quit: Leaving) |
| 2025-12-26 18:46:53 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2025-12-26 18:43:55 +0100 | merijn | (~merijn@62.45.136.136) (Ping timeout: 240 seconds) |
| 2025-12-26 18:39:29 +0100 | merijn | (~merijn@62.45.136.136) merijn |
| 2025-12-26 18:37:53 +0100 | <haskellbridge> | <Liamzee> https://hackage-content.haskell.org/package/ghc-internal-9.1401.0/docs/src/GHC.Internal.IO.Unsafe.… |
| 2025-12-26 18:37:51 +0100 | <haskellbridge> | <Liamzee> Also: |
| 2025-12-26 18:37:38 +0100 | <ncf> | yeah that's the point |
| 2025-12-26 18:37:19 +0100 | <ncf> | it also comes up here https://proofassistants.stackexchange.com/a/932 as the "irrelevance axiom" |
| 2025-12-26 18:37:19 +0100 | <ski> | "How does it matter that it's still using the original RealWorld?" -- mm, i guess it means the action can't be scheduled to happen before the invocation of `unsafeInterleaveIO' happens |
| 2025-12-26 18:36:40 +0100 | <ncf> | if you replace IO with propositional truncation, then the assumption of choice as above is equivalent to the "world's smallest axiom of choice" (choice over propositions) |
| 2025-12-26 18:36:10 +0100 | <ncf> | it comes up in https://lmcs.episciences.org/3217/pdf theorem 7.7 |
| 2025-12-26 18:35:36 +0100 | <ski> | mm |
| 2025-12-26 18:35:04 +0100 | <ncf> | yeah, it has the form of the premise. i don't think it's really related though, since we're not interested in taking fixed points |
| 2025-12-26 18:34:37 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2025-12-26 18:34:36 +0100 | <ski> | type reminds me a little of `loeb :: Functor f => f (f a -> a) -> f a' |
| 2025-12-26 18:34:31 +0100 | <ncf> | in terms of the state monad, choice s = (\ k -> fst (k s), s) |
| 2025-12-26 18:34:06 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/pUZqcmzrNFjqpSRguxhgPvfI/iqhSMNoSnW4 (3 lines) |
| 2025-12-26 18:34:03 +0100 | <haskellbridge> | <Liamzee> now that i think about it: is it true that unsafeInterleaveIO ma = pure (unsafePerformIO ma) ? it sure seems like that's what the implementation is doing |
| 2025-12-26 18:33:20 +0100 | <ski> | (aka `($ ma) <$> choice') |
| 2025-12-26 18:32:59 +0100 | <ncf> | yeah |