Logs: liberachat/#haskell
| 2025-12-26 15:18:33 | <[exa]> | thanks :) |
| 2025-12-26 15:19:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 15:19:32 | <ncf> | (well, i think there's only one (lawful) monad instance you can write) |
| 2025-12-26 15:20:07 | <Franciman> | they mention this phenomenon in the mailing list that is referred to in the stackoverflow thread |
| 2025-12-26 15:21:54 | <Franciman> | hi ncf ! |
| 2025-12-26 15:23:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-26 15:28:23 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 2025-12-26 15:31:28 | <[exa]> | yeah, it's ... unpleasantly rigorous |
| 2025-12-26 15:34:24 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 2025-12-26 15:35:09 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 15:40:10 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-12-26 15:50:55 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 15:55:59 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-12-26 16:00:32 | × | karenw quits (~karenw@user/karenw) (Quit: Deep into that darkness peering...) |
| 2025-12-26 16:03:58 | × | Axman6 quits (~Axman6@user/axman6) (Remote host closed the connection) |
| 2025-12-26 16:04:33 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 16:09:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-26 16:20:22 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 16:24:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-26 16:32:10 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Ping timeout: 255 seconds) |
| 2025-12-26 16:36:09 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 16:37:44 | → | ZLima12_ joins (~zlima12@user/meow/ZLima12) |
| 2025-12-26 16:37:59 | × | ZLima12 quits (~zlima12@user/meow/ZLima12) (Ping timeout: 260 seconds) |
| 2025-12-26 16:40:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2025-12-26 16:51:40 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 16:56:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2025-12-26 16:56:39 | Digitteknohippie | is now known as Digit |
| 2025-12-26 17:05:34 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 17:10:20 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-12-26 17:11:43 | <haskellbridge> | <Liamzee> umm, been thinking, doesn't unsafeInterleaveIO violate referential transparency? I guess that's implied by the name! |
| 2025-12-26 17:12:42 | <geekosaur> | yes |
| 2025-12-26 17:12:54 | <haskellbridge> | <Liamzee> but, implicitly, i can have a pure function trigger an effect on its own simply by evaluating a value that causes unsafeInterleaveIO to throw effects |
| 2025-12-26 17:13:11 | <geekosaur> | yep, that's exactly the point of it |
| 2025-12-26 17:13:17 | → | sroso joins (~sroso@user/SrOso) |
| 2025-12-26 17:13:23 | <geekosaur> | and why it's `unsafe` |
| 2025-12-26 17:14:04 | <haskellbridge> | <Liamzee> i just never thought about it in the sense of having pure functions evaluate through unsafeInterleaveIO |
| 2025-12-26 17:14:14 | <haskellbridge> | <Liamzee> I thought of it more like, actions doing so |
| 2025-12-26 17:15:31 | <ncf> | ? |
| 2025-12-26 17:16:25 | × | synchromesh quits (~john@2406:5a00:2412:2c00:68ff:586d:59bf:bb1) (Read error: Connection reset by peer) |
| 2025-12-26 17:16:33 | → | marinelli joins (~weechat@gateway/tor-sasl/marinelli) |
| 2025-12-26 17:16:43 | <ncf> | oh never mind, i misread |
| 2025-12-26 17:17:52 | → | synchromesh joins (~john@2406:5a00:2412:2c00:68ff:586d:59bf:bb1) |
| 2025-12-26 17:20:03 | <c_wraith> | At least there's still an IO in the type at the end to tell you there are effects going on. |
| 2025-12-26 17:20:42 | <c_wraith> | Compare that to unsafeInterleaveST, which leaves no traces behind.... |
| 2025-12-26 17:21:12 | <ski> | Liamzee : there is an argument that observed differences in behaviour as to if and when the I/O occurs, is due to the nondeterminacy of the `IO' in the result type of `unsafeInterleaveIO', similarly to how `forkIO' (concurrency) introduce nondeterminacy with how threads will be scheduled wrt each other. iow, `unsafeInterleaveIO' would guarantee that the I/O might or might not happen (but obviously must've |
| 2025-12-26 17:21:18 | <ski> | happened before forcing the returned value, if that happens) |
| 2025-12-26 17:21:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 17:24:01 | <ski> | iow, the "have a pure function trigger an effect on its own simply by evaluating a value that causes unsafeInterleaveIO to throw effects" would be a particular implementation choice, for efficiency, but the compiler would be allowed to schedule the I/O to happen earlier (and so earlier than other I/O actions not sequenced wrt this one), if it could show that the result value would eventually get forced |
| 2025-12-26 17:25:20 | <ski> | otoh, this argument does not work for `unsafeInterleaveST', there's no concurrency in `ST s' |
| 2025-12-26 17:26:32 | <ncf> | 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 17:27:09 | <ncf> | ah, not quite, it's using the input RealWorld instead of creating one out of thin air |
| 2025-12-26 17:27:44 | <ski> | you'd not be surprised by an I/O action in an invocation of `forkIO' happening at different times, on different runs, so you should also not be surprised by the I/O with `unsafeInterleaveIO' being hard to predict when it happens |
| 2025-12-26 17:27:45 | <haskellbridge> | <Liamzee> TBH I'm still looking at FFI and I'm thinking about using unsafeInterleaveIO with a mutex to allow streaming of FFI read-in-place |
| 2025-12-26 17:27:47 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 2025-12-26 17:27:54 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-12-26 17:28:21 | <haskellbridge> | <Liamzee> but w/e this is fancy, I'll be happy just to get RecordBatch from arrow-rs being converted to a dataframe without segfaulting |
| 2025-12-26 17:28:28 | <haskellbridge> | <Liamzee> via a copy |
| 2025-12-26 17:30:42 | <ncf> | so an equivalent formulation of unsafeInterleaveIO should be choice :: IO (IO a → a) |
| 2025-12-26 17:31:21 | <ncf> | well, not equivalent, more primitive |
| 2025-12-26 17:31:41 | <ncf> | given choice, you can implement unsafeInterleaveIO ma = choice <*> ma |
| 2025-12-26 17:32:07 | <ncf> | (i call it choice because it's a form of choice if you replace IO with a propositional truncation modality, but this is a bad name) |
| 2025-12-26 17:32:47 | <ski> | you mean `choice <*> pure ma' ? |
| 2025-12-26 17:32:59 | <ncf> | yeah |
| 2025-12-26 17:33:20 | <ski> | (aka `($ ma) <$> choice') |
| 2025-12-26 17:34:03 | <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 17:34:06 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/pUZqcmzrNFjqpSRguxhgPvfI/iqhSMNoSnW4 (3 lines) |
| 2025-12-26 17:34:31 | <ncf> | in terms of the state monad, choice s = (\ k -> fst (k s), s) |
| 2025-12-26 17:34:36 | <ski> | type reminds me a little of `loeb :: Functor f => f (f a -> a) -> f a' |
| 2025-12-26 17:34:37 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2025-12-26 17:35:04 | <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 17:35:36 | <ski> | mm |
| 2025-12-26 17:36:10 | <ncf> | it comes up in https://lmcs.episciences.org/3217/pdf theorem 7.7 |
| 2025-12-26 17:36:40 | <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 17:37:19 | <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 17:37:19 | <ncf> | it also comes up here https://proofassistants.stackexchange.com/a/932 as the "irrelevance axiom" |
| 2025-12-26 17:37:38 | <ncf> | yeah that's the point |
| 2025-12-26 17:37:51 | <haskellbridge> | <Liamzee> Also: |
| 2025-12-26 17:37:53 | <haskellbridge> | <Liamzee> https://hackage-content.haskell.org/package/ghc-internal-9.1401.0/docs/src/GHC.Internal.IO.Unsafe.html#unsafeInterleaveIO |
| 2025-12-26 17:39:29 | → | merijn joins (~merijn@62.45.136.136) |
| 2025-12-26 17:43:55 | × | merijn quits (~merijn@62.45.136.136) (Ping timeout: 240 seconds) |
| 2025-12-26 17:46:53 | ← | L29Ah parts (~L29Ah@wikipedia/L29Ah) () |
| 2025-12-26 17:48:04 | × | tabemann quits (~tabemann@12.215.215.61) (Quit: Leaving) |
| 2025-12-26 17:55:10 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 17:59:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-26 18:06:34 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 18:11:23 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2025-12-26 18:15:02 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 2025-12-26 18:15:19 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Remote host closed the connection) |
| 2025-12-26 18:22:23 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 18:27:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-12-26 18:38:10 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 18:42:48 | → | rainbyte_ joins (~rainbyte@186.22.19.214) |
| 2025-12-26 18:42:50 | × | rainbyte quits (~rainbyte@186.22.19.214) (Read error: Connection reset by peer) |
| 2025-12-26 18:42:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-12-26 18:43:01 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-26 18:53:37 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2025-12-26 18:57:11 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2025-12-26 18:58:07 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-26 19:04:07 | <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:09:55 | <ncf> | mere christmas |
All times are in UTC.