Home liberachat/#haskell: Logs Calendar

Logs on 2024-12-22 (liberachat/#haskell)

00:01:58 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
00:04:28 <Leary> % :t \xs i -> either Just (const Nothing) . flip runStateT 0 $ for_ xs \x -> do{ j <- get; put (j + 1); when (j == i) (throwError x) }
00:04:28 <yahb2> \xs i -> either Just (const Nothing) . flip runStateT 0 $ for_ xs \x -> do{ j <- get; put (j + 1); when (j == i) (throwError x) } ; :: (Eq a, Num a, Foldable t) => t e -> a -> Maybe e
00:04:41 × cptaffe quits (~cptaffe@user/cptaffe) (Ping timeout: 265 seconds)
00:05:03 sprotte24 joins (~sprotte24@p200300d16f1a2c0064c6ee858fd5dcfe.dip0.t-ipconnect.de)
00:05:09 MyNetAz joins (~MyNetAz@user/MyNetAz)
00:05:16 × E2Combinator quits (~E2Combina@190.180.45.137) (Quit: Client closed)
00:05:23 <Leary> EvanR: `Foldable` already has indexing.
00:06:47 cptaffe joins (~cptaffe@user/cptaffe)
00:10:12 × housemate quits (~housemate@ppp203-122-213-191.static.internode.on.net) (Quit: Nothing to see here. I wasn't there. I take IRC seriously.)
00:10:22 E2Combinator joins (~E2Combina@190.180.45.137)
00:13:20 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
00:17:27 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
00:17:47 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
00:23:12 <monochrom> Wait, do you mean one can just do toList and index into that list?!
00:23:36 <monochrom> Not very efficient but I guess it counts.
00:24:00 <monochrom> Then again Napier functors can have inefficient indexing too.
00:28:42 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
00:33:08 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
00:34:04 housemate joins (~housemate@ppp203-122-213-191.static.internode.on.net)
00:42:31 × CrunchyFlakes quits (~CrunchyFl@31.19.233.78) (Read error: Connection reset by peer)
00:44:05 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
00:44:46 CrunchyFlakes joins (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de)
00:45:45 <E2Combinator> Hi. I have some serious issues tryong to define a wrapper effect in fused-effects, anyone can help with that?
00:46:33 <E2Combinator> I have defined the effect as such:
00:46:33 <E2Combinator> https://paste.tomsmeding.com/4J7pz5eI
00:46:33 <E2Combinator> And it typechecks and all
00:47:05 <E2Combinator> I have defined an operation as such:
00:47:07 <E2Combinator> resolveMovementStep :: Has UpdateTracking sig m => WilMaze InMovement -> m (WilMaze InMovement)
00:47:12 <E2Combinator> And it typechecks and all
00:47:36 <E2Combinator> But the moment I try to run resolveMovementStep with an effect carrier stack, I get the following:
00:47:48 <E2Combinator> run $ runUpdateTracking $ resolveMovementStep m
00:48:28 <E2Combinator> https://paste.tomsmeding.com/pXrMkP7e
00:48:40 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
00:49:09 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
00:49:09 <E2Combinator> It complains partially about a missing effect signature, but even if I add the Has (Writer Any) constraint, it still fails
00:50:07 <E2Combinator> Nvm, I saw the issue. Extraneous constraint in the Algebra instance
00:55:45 × MyNetAz quits (~MyNetAz@user/MyNetAz) (Remote host closed the connection)
00:59:46 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:02:46 MyNetAz joins (~MyNetAz@user/MyNetAz)
01:04:52 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
01:15:05 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:15:27 ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com)
01:17:27 × sprotte24 quits (~sprotte24@p200300d16f1a2c0064c6ee858fd5dcfe.dip0.t-ipconnect.de) (Quit: Leaving)
01:20:05 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
01:21:17 <orangeflu> Bowuigi, you here?
01:27:00 <haskellbridge> <Bowuigi> Yes, also Matrix stores messages when I'm offline
01:30:47 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:35:17 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 244 seconds)
01:37:21 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
01:38:08 <orangeflu> ok, so weird thing
01:38:14 <orangeflu> been coding some more on that branch today
01:38:38 <orangeflu> decided, what the hell, haven't done a cabal test in a few hours, let me make sure i didn't fuck anything up in the meanwhile
01:38:49 <orangeflu> that few gigs we were talking about yesterday
01:38:54 <orangeflu> disappeared completely
01:39:06 <orangeflu> if i run test.asm, it doesn't do that anymore
01:39:10 <orangeflu> not sure when it stopped
01:39:14 × housemate quits (~housemate@ppp203-122-213-191.static.internode.on.net) (Quit: Nothing to see here. I wasn't there. I take IRC seriously.)
01:39:41 <orangeflu> i tried to go back to yesterday's commits but no luck, it simply isn't there
01:40:10 <orangeflu> so i'ma just decide its a compiler weirdness and hope it never comes back, but it is weird indeed
01:41:07 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:42:08 <haskellbridge> <thirdofmay18081814goya> hm, how owuld FRP model something like viewer state? e.g., the current page the user is on in a website
01:42:08 <orangeflu> you know what, i might retry some profiling right now since it seems that the compiler decided to behave
01:42:15 <haskellbridge> <thirdofmay18081814goya> * would
01:43:30 sprotte24 joins (~sprotte24@p200300d16f1a2c0064c6ee858fd5dcfe.dip0.t-ipconnect.de)
01:43:54 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
01:45:24 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
01:45:39 × sprotte24 quits (~sprotte24@p200300d16f1a2c0064c6ee858fd5dcfe.dip0.t-ipconnect.de) (Client Quit)
01:46:39 × acidjnk_new quits (~acidjnk@p200300d6e7283f52b5be3bacf47f1ed3.dip0.t-ipconnect.de) (Ping timeout: 245 seconds)
01:50:27 × mhatta quits (~mhatta@www21123ui.sakura.ne.jp) (Quit: ZNC 1.9.1+deb2+b1 - https://znc.in)
01:51:05 <haskellbridge> <thirdofmay18081814goya> oh this would be represented as a constant stream that changes contents as the user changes pages, right?
01:51:19 <haskellbridge> <thirdofmay18081814goya> uh not "constant" stream, but continuous stream
01:52:01 mhatta joins (~mhatta@www21123ui.sakura.ne.jp)
01:52:01 <haskellbridge> <thirdofmay18081814goya> e.g. a stream whose content is the unique ID of the current page
01:52:03 <haskellbridge> <thirdofmay18081814goya> right?
01:56:25 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
01:59:51 weary-traveler joins (~user@user/user363627)
02:00:54 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
02:11:46 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
02:11:54 <haskellbridge> <Bowuigi> orangeflu odd stuff, but I'm glad it got solved
02:16:24 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
02:18:00 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds)
02:22:45 housemate joins (~housemate@125.63.162.34)
02:30:37 E2Combinator parts (~E2Combina@190.180.45.137) ()
02:33:04 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
02:33:33 × housemate quits (~housemate@125.63.162.34) (Ping timeout: 265 seconds)
02:37:03 <orangeflu> Bowuigi: I don't like that i don't know where it came from, and i still can't make profiling work
02:37:54 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
02:38:13 <haskellbridge> <Bowuigi> Did you update or change any settings?
02:39:01 <orangeflu> i disabled test coverage
02:39:27 <orangeflu> waaaait
02:39:37 <orangeflu> it compiled with profiling
02:39:43 <orangeflu> stand-by for results
02:42:36 <orangeflu> nvm
02:47:14 <orangeflu> idk why it doesn't work. I try to build it wiht -prof, cabal complains i shouldn't do that. not like it matters, it gives an error anyway. Then i do cabal build --enable-profiling and then when i run it, no prog file is generated
02:47:28 <orangeflu> How this whole process is supposed to work is hideously explained
02:48:26 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
02:50:30 <orangeflu> ok, i ended up doing it
02:50:42 <orangeflu> you want the results? not sure how to interpret them
02:51:51 <haskellbridge> <Bowuigi> To be honest no idea how to profile either, but if it is a text file just drop it in https://paste.tomsmeding.com
02:52:40 <haskellbridge> <Bowuigi> In particular, allocation spikes is what you are looking for
02:52:59 <haskellbridge> <thirdofmay18081814goya> in FRP, do we suppose there exists a stream between the user's ability-to-click and buttons?
02:53:00 <orangeflu> https://paste.tomsmeding.com/b9owLIrr
02:53:41 <geekosaur> generally you need to compile with profiling (cabal will do this with --enable-profiling) and then run with profiling enabled (which is an RTS option: https://downloads.haskell.org/ghc/9.10.1/docs/users_guide/runtime_control.html#rts-profiling)
02:53:51 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
02:53:58 <orangeflu> am i reading it correctly when it says it allocated 914 megabytes?
02:54:07 <orangeflu> total alloc = 914,690,800 bytes (excludes profiling overheads)
02:55:08 <orangeflu> geekosaur: yeah, what i did is i added profiling: True in cabal.project.local, and these arguments to ghc-options: -fprof-auto "-with-rtsopts=-N -p -s -h -i0.1"
02:55:12 <orangeflu> and it seems to work now
02:57:50 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
02:57:58 <geekosaur> also note that "total alloc" includes ephemeral allocations which never leave the nursery and can generally be ignored because they're very fast to both allocate and reclaim
02:58:24 <haskellbridge> <Bowuigi> thirdofmay18081814goya re:current-page yes, a value that may change as time moves is represented like that
02:58:55 <haskellbridge> <Bowuigi> orangeflu the tables on the allocation report show how much time and allocation is used on every function
02:58:59 <orangeflu> geekosaur: still seems like a lot, for what the programs does
03:00:48 <haskellbridge> <Bowuigi> thirdofmay18081814goya you might want to check the source for reactive-banana or some other FRP UI library, I don't know enough about that, sorry
03:01:45 <orangeflu> so what should i take away from this report? that the ST instruction takes a lot of time, since it's in a program where it's used a lot?
03:02:01 <haskellbridge> <thirdofmay18081814goya> hm I see ty
03:02:34 <haskellbridge> <Bowuigi> st might have a space leak, 961MB for bubble sort is too much lol
03:03:42 <orangeflu> yeah, but ST is used a lot in that program
03:04:07 <orangeflu> and if haskell allocates and deallocates those EmulatorState everytime i modify the arrays inside
03:04:14 <orangeflu> it would make sense to consume that much
03:04:20 <orangeflu> right?
03:04:24 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:04:47 <orangeflu> cause the ST instruction stores something in the memory, which is a 2000 bytes array
03:05:04 × op_4 quits (~tslil@user/op-4/x-9116473) (Remote host closed the connection)
03:05:06 <haskellbridge> <Bowuigi> Oh could you move to MVector?
03:05:13 <orangeflu> I could
03:05:18 <orangeflu> already made plans to
03:05:29 housemate joins (~housemate@ppp203-122-213-191.static.internode.on.net)
03:05:34 op_4 joins (~tslil@user/op-4/x-9116473)
03:05:52 <orangeflu> i have an idea though. My emulator has configurable SRAM sizes. Let's see if the total allocation decreases if i give it less total SRAM
03:05:53 <haskellbridge> <Bowuigi> Because GHC tries to make stuff mutable on lower layers, but it can't if large parts are modified (as in the case of Array)
03:06:14 × housemate quits (~housemate@ppp203-122-213-191.static.internode.on.net) (Max SendQ exceeded)
03:07:11 housemate joins (~housemate@ppp203-122-213-191.static.internode.on.net)
03:07:15 × housemate quits (~housemate@ppp203-122-213-191.static.internode.on.net) (Remote host closed the connection)
03:07:29 <orangeflu> memory allocation drops to 511 mb if i give it 500 bytes of SRAM instead
03:08:11 <geekosaur> Array does carding but the cards are fairly large
03:08:22 <haskellbridge> <Bowuigi> The tree below indicates the local (with respect to the siblings of the tree and children) time and allocation usage
03:08:26 <geekosaur> 128 elements last I heard?
03:08:58 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
03:09:33 <orangeflu> if i use another assembly file, like one that doesn't write to memory at all, total allocation is 1-2 mb, and changing the memory size doesn't make that much of a difference
03:10:09 <orangeflu> geekosaur: carding?
03:10:32 <geekosaur> instead of GCing the entire array, it's divided into cards and individual cards are GCd
03:11:43 <geekosaur> but f you touch elements in a lot of cards, it's slightly less performant than GCing the whole array; it works best if only nearby elements are modified
03:12:02 <orangeflu> but why GC the array in the first place is what i don't understand. Like, i assume the compiler is smart enough to see that i always take the array, modify it and return the copy. does that not imply that it should make it mutable behind the scenes?
03:12:33 <haskellbridge> <Bowuigi> Not exactly, the compiler likely can't assume that
03:12:35 <geekosaur> if you're not modifying it, why was MVector the alternative?
03:13:09 <orangeflu> i am "modifying it", by making a copy of it with the element i want modified changed, and i return that instead
03:13:17 <haskellbridge> <Bowuigi> It was being modified, orangeflu refers to copy/mutate semantics, not explicit cloning
03:13:32 <orangeflu> yeah
03:14:04 <haskellbridge> <Bowuigi> So MVector would help here, as it has better fusion and is supposed to be mutable
03:14:44 <orangeflu> let me see if i can make a quick experiment to see how it would work
03:15:08 <orangeflu> but it may prove to be difficult because i would need to modify every function for every instruction, may take a while
03:15:40 <haskellbridge> <Bowuigi> It is likely rebuilding the emulator state and array, but the only way to know for certain is to read the Core. That is way too far from a begginer topic
03:15:41 <orangeflu> and i never worked with monads in this way before
03:15:59 <orangeflu> is the Core in haskell?
03:18:08 <haskellbridge> <Bowuigi> With "Core" I mean GHC Core, one of the intermediate representations of Haskell code used in GHC, specifically, the one that seems to have the most influence in the compilation result while being functional
03:19:33 <haskellbridge> <Bowuigi> Practice with MVector outside of the emulator (and possibly with the strict state monad, the recommendation that was made yesterday) before implementing it, to understand it better
03:19:44 <geekosaur> Core is kinda a simplified Haskell, but with annotations for things like strictness of parameters which guide optimization
03:19:46 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:22:35 <orangeflu> By strict state monad, what do you mean?
03:24:36 <orangeflu> ST?
03:26:32 <geekosaur> https://downloads.haskell.org/ghc/latest/docs/libraries/mtl-2.3.1-a17d/Control-Monad-State-Strict.html
03:26:40 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
03:27:07 housemate joins (~housemate@ppp203-122-213-191.static.internode.on.net)
03:27:18 <geekosaur> ST is not "state" in the same sense, it is an execution context with private state in the form of STRefs and STArrays
03:30:08 <orangeflu> i wish i knew what you were trying to say
03:30:51 <orangeflu> when i was trying to understand monads, i thought "after i get this, everything else will be easy, this is the hardest thing ever"
03:30:52 <geekosaur> the concept behind ST is a bit difficult to understand, yes
03:30:55 <orangeflu> apparently not
03:32:29 × housemate quits (~housemate@ppp203-122-213-191.static.internode.on.net) (Quit: Nothing to see here. I wasn't there. I take IRC seriously.)
03:33:08 <geekosaur> when we talk about threads, we normally talk about CPU threads. ST is a difference concept, a state thread. instead of representing a separate CPU execution environment, it's a separate local state environment. in Haskell this means you have access to mutable data within the thread that can't be accessed outside of it
03:35:33 <geekosaur> the best explanation is probably one in the paper linked at the top of the Control.Monad.ST documentation
03:36:00 <geekosaur> also, trust me, you haven't by far exhausted the complexities of Haskell
03:37:49 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:37:50 <geekosaur> rank-N types (which you're on the border of with ST), STM (software transactional memory), type level programming, … the list goes on
03:38:29 <orangeflu> you might as well be speaking dutch
03:41:16 <geekosaur> that was kinda the point 🙂
03:42:20 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
03:43:25 <orangeflu> i am already stuck with this vector
03:43:43 × td_ quits (~td@i53870903.versanet.de) (Ping timeout: 244 seconds)
03:45:03 alecs joins (~alecs@61.pool85-58-154.dynamic.orange.es)
03:45:39 td_ joins (~td@i5387092A.versanet.de)
03:49:24 × alecs quits (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 244 seconds)
03:49:42 <orangeflu> i can't even create an mvector, it doesn't let me
03:53:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
03:55:13 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:57:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
03:59:12 <orangeflu> how do i unwrap from ST?
03:59:37 <c_wraith> :t runST
03:59:38 <lambdabot> (forall s. ST s a) -> a
04:00:15 <orangeflu> i thought so too but it doesnt work
04:00:40 <c_wraith> it does if you aren't trying to leak things that you're not supposed to
04:00:48 <orangeflu> Couldn't match type: M.MVector s Int with: IO a0
04:00:58 <orangeflu> leak?
04:01:14 <c_wraith> ST is designed to prevent mutable values from leaking into pure code.
04:01:27 <c_wraith> but if you're getting an error about IO, you're doing something else wrong.
04:01:47 <orangeflu> probably because i am running this in main
04:04:22 L29Ah parts (~L29Ah@wikipedia/L29Ah) ()
04:08:34 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:09:12 <orangeflu> i think i made it work somehow
04:09:48 <orangeflu> but i had to make like 3 functions just to set a value and return it, and i lost the vector
04:11:32 × dostoevsky quits (~dostoevsk@user/dostoevsky) (Quit: Leaving)
04:13:07 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
04:13:30 <haskellbridge> <thirdofmay18081814goya> hm
04:13:36 <haskellbridge> <thirdofmay18081814goya> what's the right way to think of switches in FRP?
04:13:54 <haskellbridge> <thirdofmay18081814goya> e.g. if a switch has two possible targets, do we think of it as a function from one signal to two signals?
04:13:56 <monochrom> A stream of booleans?
04:14:22 <monochrom> If the two signals are mutually exclusive then it is just one signal of two states.
04:14:56 <monochrom> or 3 states if they are {0, 1, neither}
04:15:34 <haskellbridge> <thirdofmay18081814goya> hm, I'm not sure I understand. don't we think of a switch as changing the target signal?
04:16:00 <haskellbridge> <thirdofmay18081814goya> like network switches
04:16:17 <monochrom> A long time ago, Shannon already turned switches into logic gates, so still just booleans.
04:17:16 <haskellbridge> <thirdofmay18081814goya> we're talking about e.g. Yampa switches here right?
04:18:26 <monochrom> Are they really non-isomorphic to relays?
04:18:56 <haskellbridge> <thirdofmay18081814goya> I don't know, here's the type "switch :: SF i (o, Event e) -> (e -> SF i o) -> SF i o"
04:19:00 <orangeflu> c_wraith: so, if i understand correctly, everywhere i need to modify the mvector, it needs to return ST s (MVector s Int). Just to read it, i need to be in at least ST s Int. Then how do I reconcile that with getting user input and stuff. I have a bunch of other monads i need to think about in my REPL, that need to take input from the user and so on. But if i escape this ST by running through runST, i
04:19:06 <orangeflu> lose the vector, right?
04:23:56 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:24:27 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds)
04:27:06 × aforemny quits (~aforemny@2001:9e8:6cf6:8000:f088:f772:a53:8f63) (Ping timeout: 246 seconds)
04:27:45 aforemny joins (~aforemny@89.244.199.39)
04:28:35 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
04:30:13 <c_wraith> orangeflu: The point of ST is that you encapsulate *all* the mutation in a single call to runST. You return an immutable value.
04:32:43 <haskellbridge> <Bowuigi> orangeflu you have to create the MVector in IO, not in ST
04:33:08 <haskellbridge> <Bowuigi> So you allocate the memory in main as usual, but instead of creating an array you create an MVector
04:33:21 <c_wraith> Bowuigi: eh? If you want to mutate it in ST, you need to allocate it in ST.
04:36:00 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:36:01 <haskellbridge> <Bowuigi> The idea was to have an MVector on IO, not on ST
04:36:02 <orangeflu> how do i return an immutable value?
04:36:30 <haskellbridge> <Bowuigi> What
04:36:43 <c_wraith> Eh, I started answering questions starting from "what's the eliminator for ST"
04:37:37 <c_wraith> If you're using IO mutable vectors, ignore everything about ST.
04:37:37 <orangeflu> c_wraith said "you return an immutable value". So i go in ST or IO, mutate it however i wish based on what the instruction needs to do, then when i remove it from IO, it becomes immutable?
04:39:41 <haskellbridge> <Bowuigi> c_wraith Some context, orangeflu is writing an emulator. This emulator has a fixed memory, which used to be in an Array. This caused space leaks, so I and [exa] suggested using an MVector because it provides benefits on this use case
04:40:24 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
04:41:13 <haskellbridge> <Bowuigi> orangeflu the idea is to run the modifications on IO only (ST also works but it's not what we want here), that's what the "PrimMonad" stuff means
04:41:18 <c_wraith> That's a kind of bad way to avoid space leaks. It's better to write code that uses space invariants properly. But it has enough other benefits that it's still worth doing.
04:41:47 <c_wraith> (It's likely to not avoid space leaks)
04:43:35 <haskellbridge> <Bowuigi> The Array here was used as if it was a mutable one (it was the original idea, but the name Array was somewhat misleading since it isn't a C array)
04:45:26 housemate joins (~housemate@124.187.109.206)
04:49:10 xff0x joins (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp)
04:50:33 <orangeflu> well, the idea is to transition to mvectors, but i thought it would be easier. I am also using InputT IO (EmulatorState) in my REPL because i am using haskeline, so not sure how that is going to affect things with mvector. Also, there is also the functionality for reading a file and then ditching the IO after that, before executing
04:50:50 <orangeflu> Does that mean now I will need to have IO everywhere?
04:51:18 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
04:51:38 <haskellbridge> <Bowuigi> c_wraith you might be able to help more with this, the codebase is in https://github.com/Flu/avr-emulator and the profiling results are in https://paste.tomsmeding.com/b9owLIrr
04:51:38 <orangeflu> This seems more trouble than its worth considering I don't even understand how to use, let alone modify all my pure functions into using it atop of my InputT IO stuff
04:52:25 <haskellbridge> <Bowuigi> With MVector you need something like IO everywhere yes. Haskell optimization is not for begginners
04:52:31 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
04:52:47 <haskellbridge> <Bowuigi> Just like optimization in other languages ofc
04:53:42 <haskellbridge> <Bowuigi> There might be a more obvious refactor that we missed tho
04:54:35 <orangeflu> i'm sure i did a horrible job of writing this and there are a bunch of stuff that make no sense or could be optimized heavily
04:55:02 <orangeflu> thing is, this is both a learning project and something that i want to be useful
04:55:39 × xff0x quits (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 265 seconds)
04:56:01 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
04:56:06 <haskellbridge> <Bowuigi> MVector is a somewhat extreme solution, mutable stuff is fairly common in heavily optimized programs/libraries like smalltt or flatparse (there are a lot more examples but I know those two more in depth than anything else)
04:56:33 rvalue joins (~rvalue@user/rvalue)
04:57:03 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
04:58:10 <haskellbridge> <Bowuigi> Hmmm moving to a strict state monad to handle your emulator state could also help. It attacks space leaks more directly and is a smaller change
04:58:10 × housemate quits (~housemate@124.187.109.206) (Quit: Nothing to see here. I wasn't there. I take IRC seriously.)
05:00:55 <orangeflu> i know what a state monad is, i think. like, if i have a function, that takes a container and returns a modified container and a result, i can chain them together with do notation. that's what i understand anyway. But how is that different from what i'm doing now? except for the fact that i don't chain them in a do block (which wouldn't be useful anyway, cause i don't execute instructions that way
05:01:02 <orangeflu> anyway)
05:02:43 <haskellbridge> <Bowuigi> Passing state around in a strict way, along with nice syntax sugar is what this is supposed to do
05:03:41 housemate joins (~housemate@124.187.109.206)
05:03:41 <orangeflu> when you say 'strict', do you mean not lazily?
05:04:16 <haskellbridge> <Bowuigi> Yes, but not eagerly either
05:05:18 <orangeflu> c_wraith: what do you think about the project?
05:05:18 × califax quits (~califax@user/califx) (Remote host closed the connection)
05:05:18 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection)
05:05:35 califax joins (~califax@user/califx)
05:05:41 ChaiTRex joins (~ChaiTRex@user/chaitrex)
05:05:55 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
05:06:35 <haskellbridge> <Bowuigi> "Eager" is "fully evaluate", "Strict" is "evaluate only what I'm directly responsible for" and "Lazy" is "evaluate only what I will pattern match on, as I pattern match on it". Or at least that seems to be the general consensus
05:07:30 <orangeflu> and why is the laziness causing me space leaks while strictness wouldn't?
05:07:52 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
05:08:37 <haskellbridge> <Bowuigi> Space leaks are caused by duplication of code, code is duplicated wherever variables are duplicated in lazy evaluation
05:09:37 <haskellbridge> <Bowuigi> Strict evaluation would evaluate the value once and possibly duplicate other computations inside that value
05:10:10 × Guest78 quits (~Guest78@37.228.252.73) (Ping timeout: 240 seconds)
05:10:45 Guest78 joins (~Guest78@213.233.155.134)
05:10:45 <monochrom> Ugh no, strictness is a denotational notion, not an operational (evaluation) notion. A strict function means f bottom = bottom.
05:11:46 <haskellbridge> <Bowuigi> So what do you call the operational notion?
05:12:02 <monochrom> denotational means you only talk about whether you get an answer and what answer if yes, it deliberately avoids how the computer manages to do it.
05:12:09 <monochrom> eager and lazy
05:12:19 <haskellbridge> <Bowuigi> That's why I prefer working with total languages lol
05:12:34 <haskellbridge> <Bowuigi> Oh there we go
05:12:44 × chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
05:13:16 chexum joins (~quassel@gateway/tor-sasl/chexum)
05:13:16 <monochrom> there is also speculative evaluation, it can result in non-strict while being even more eager than eager.
05:13:46 <monochrom> So even the "eager : lazy :: strict : non-strict" "correspondence" is easily broken.
05:14:59 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
05:15:40 <haskellbridge> <Bowuigi> So the duplication is operational right?
05:16:58 <monochrom> Yes absolutely. If you want to predict how much time and how much space are spent, they emphatically require knowing the evaluation strategy, i.e., operational.
05:17:32 <monochrom> Denotational semantics strives to (even prides in) avoid talking about them.
05:17:42 × poscat quits (~poscat@user/poscat) (Read error: Connection reset by peer)
05:17:53 poscat0x04 joins (~poscat@user/poscat)
05:21:38 <haskellbridge> <Bowuigi> I see, yeah Haskell can be hard to understand sometimes lol
05:23:54 <monochrom> Having said that, if you say you are only using GHC, then you know it almost sticks to "use lazy for non-strict, use eager for strict". But there are occasional deviations when the code optimizer thinks it's more efficient to do it some other way.
05:25:14 × ryanbooker quits (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
05:25:54 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
05:30:30 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
05:33:05 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds)
05:39:28 tnt1 joins (~Thunderbi@user/tnt1)
05:41:18 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
05:44:30 × CrunchyFlakes quits (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
05:46:10 alecs joins (~alecs@61.pool85-58-154.dynamic.orange.es)
05:46:21 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
05:47:00 CrunchyFlakes joins (~CrunchyFl@31.19.233.78)
05:50:45 × alecs quits (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 265 seconds)
05:56:40 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:00:22 housemate_ joins (~housemate@124.187.109.206)
06:01:23 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
06:01:56 tnt2 joins (~Thunderbi@user/tnt1)
06:02:50 × housemate quits (~housemate@124.187.109.206) (Ping timeout: 265 seconds)
06:03:21 × housemate_ quits (~housemate@124.187.109.206) (Remote host closed the connection)
06:03:30 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds)
06:03:30 tnt2 is now known as tnt1
06:12:03 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:14:22 tnt2 joins (~Thunderbi@user/tnt1)
06:15:24 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 265 seconds)
06:15:24 tnt2 is now known as tnt1
06:16:39 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
06:27:25 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:27:55 agent314 joins (~quassel@149.40.50.111)
06:31:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
06:37:00 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:41:38 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
06:43:06 hiredman joins (~hiredman@frontier1.downey.family)
06:43:51 youthlic joins (~Thunderbi@user/youthlic)
06:44:54 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
06:50:40 × Guest78 quits (~Guest78@213.233.155.134) (Ping timeout: 240 seconds)
06:52:23 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
06:54:34 gorignak joins (~gorignak@user/gorignak)
07:00:59 jaava joins (~nick@syn-076-035-209-158.res.spectrum.com)
07:01:05 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
07:01:59 <jaava> hi discovered haskell through xmonad but now i'm curious about using it for other things
07:02:48 <jaava> is haskell good for physics simulations where one would probably lean towards c++, fortran or python depending on the use case?
07:09:12 takuan joins (~takuan@178-116-218-225.access.telenet.be)
07:12:15 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:16:49 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
07:20:55 × flukiluke quits (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Remote host closed the connection)
07:22:11 flukiluke joins (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962)
07:23:05 ephilalethes joins (~noumenon@202.186.203.84)
07:28:08 <iqubic> Looks like Hoogle is down right now due to an SSL handshake failure.
07:28:37 <iqubic> Oh, refreshing seems to have fixed it.
07:29:54 <iqubic> Actually, it seems a bit inconsistent right now.
07:31:17 <jaava> I didn't know hoogle was a thing
07:31:30 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
07:31:32 <iqubic> hoogle is great
07:31:37 <iqubic> @whereis hoogle
07:31:37 <lambdabot> Maybe you meant: where+ where
07:31:44 <iqubic> @where hoogle
07:31:44 <lambdabot> https://hoogle.haskell.org
07:32:02 <jaava> nice thanks
07:32:22 <iqubic> If you have a question of "do any functions exist that match a given type signature?" that's a really useful tool.
07:32:30 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:32:42 <jaava> there's so much software for haskell I can't believe no one ever talks about it. at least in my world
07:36:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
07:36:56 N0ping joins (~N0ping@31-208-56-179.cust.bredband2.com)
07:38:05 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:39:39 × jaava quits (~nick@syn-076-035-209-158.res.spectrum.com) (Quit: Lost terminal)
07:41:34 jaava joins (~nick@syn-076-035-209-158.res.spectrum.com)
07:42:25 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
07:47:51 × monochrom quits (trebla@216.138.220.146) (Read error: Connection reset by peer)
07:48:01 monochrm joins (trebla@216.138.220.146)
07:48:25 monochrm is now known as monochrom
07:51:24 xff0x joins (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp)
07:53:23 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
07:53:25 × ubert quits (~Thunderbi@p200300ecdf117cbda8ce35cba2c9a19e.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
07:57:55 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
08:00:03 × caconym quits (~caconym@user/caconym) (Quit: bye)
08:00:08 × tt12310978324354 quits (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Quit: The Lounge - https://thelounge.chat)
08:00:40 caconym joins (~caconym@user/caconym)
08:01:26 target_i joins (~target_i@user/target-i/x-6023099)
08:02:10 × N0ping quits (~N0ping@31-208-56-179.cust.bredband2.com) (Ping timeout: 240 seconds)
08:03:53 tt12310978324354 joins (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee)
08:05:23 housemate joins (~housemate@124.187.109.206)
08:06:49 × housemate quits (~housemate@124.187.109.206) (Remote host closed the connection)
08:09:41 housemate joins (~housemate@124.187.109.206)
08:13:44 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
08:16:08 × img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
08:17:28 img joins (~img@user/img)
08:18:29 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
08:21:14 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
08:28:57 <hellwolf> which one do you use the most.
08:29:08 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
08:30:23 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:33:34 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
08:39:02 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
08:44:38 × xff0x quits (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 244 seconds)
08:45:48 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
08:46:16 × jaava quits (~nick@syn-076-035-209-158.res.spectrum.com) (Quit: Lost terminal)
08:48:17 jaava joins (~nick@syn-076-035-209-158.res.spectrum.com)
08:49:50 × jaava quits (~nick@syn-076-035-209-158.res.spectrum.com) (Client Quit)
08:51:50 acidjnk_new joins (~acidjnk@p200300d6e7283f49b5be3bacf47f1ed3.dip0.t-ipconnect.de)
08:57:03 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
08:57:44 jaava joins (~nick@syn-076-035-209-158.res.spectrum.com)
09:03:45 × jaava quits (~nick@syn-076-035-209-158.res.spectrum.com) (Quit: Lost terminal)
09:03:57 Guest78 joins (~Guest78@64.43.50.117)
09:04:34 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
09:15:25 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
09:19:49 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
09:22:30 × yuuta quits (~YuutaW@2404:f4c0:f9c3:502::100:17b7) (Ping timeout: 246 seconds)
09:22:55 L29Ah joins (~L29Ah@wikipedia/L29Ah)
09:26:06 YuutaW joins (~YuutaW@2404:f4c0:f9c3:502::100:17b7)
09:30:48 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
09:36:18 × housemate quits (~housemate@124.187.109.206) (Quit: Nothing to see here. I wasn't there. I take IRC seriously.)
09:36:36 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
09:40:06 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
09:41:32 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
09:41:36 tnt2 joins (~Thunderbi@user/tnt1)
09:42:17 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds)
09:42:17 tnt2 is now known as tnt1
09:44:22 × ephilalethes quits (~noumenon@202.186.203.84) (Quit: Leaving)
09:44:50 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
09:54:01 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
09:57:07 sawilagar joins (~sawilagar@user/sawilagar)
09:58:18 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
10:00:57 × econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
10:02:32 __monty__ joins (~toonn@user/toonn)
10:06:03 ljdarj joins (~Thunderbi@user/ljdarj)
10:09:23 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
10:11:46 l_k joins (~student@46.61.242.35)
10:13:41 × student quits (~student@85.172.111.189) (Ping timeout: 265 seconds)
10:14:09 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
10:17:32 xff0x joins (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp)
10:19:03 Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
10:23:59 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
10:24:46 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
10:29:18 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
10:35:55 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
10:38:25 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en)
10:40:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
10:41:29 sprotte24 joins (~sprotte24@p200300d16f236f0034c2c833107a461e.dip0.t-ipconnect.de)
10:47:33 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
10:57:57 Lain_ joins (~Lain@102.211.6.62)
10:58:11 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
10:58:54 × driib318 quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat)
10:59:17 × Lain_ quits (~Lain@102.211.6.62) (Remote host closed the connection)
11:00:12 Piedro joins (~Piedro@213.226.141.133)
11:00:14 driib318 joins (~driib@vmi931078.contaboserver.net)
11:01:58 × Square quits (~Square@user/square) (Ping timeout: 252 seconds)
11:02:49 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
11:04:24 × driib318 quits (~driib@vmi931078.contaboserver.net) (Client Quit)
11:05:14 alexherbo2 joins (~alexherbo@2a02-8440-350e-cece-a50d-b49e-108d-0242.rev.sfr.net)
11:06:14 ljdarj joins (~Thunderbi@user/ljdarj)
11:06:21 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
11:08:51 driib318 joins (~driib@vmi931078.contaboserver.net)
11:10:42 × sawilagar quits (~sawilagar@user/sawilagar) (Ping timeout: 276 seconds)
11:13:33 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
11:15:13 CiaoSen joins (~Jura@2a05:5800:2da:8900:ca4b:d6ff:fec1:99da)
11:17:52 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
11:20:48 homo_ joins (~homo@37-33-152-6.bb.dnainternet.fi)
11:21:07 × homo_ quits (~homo@37-33-152-6.bb.dnainternet.fi) (Changing host)
11:21:07 homo_ joins (~homo@user/homo)
11:23:33 × CiaoSen quits (~Jura@2a05:5800:2da:8900:ca4b:d6ff:fec1:99da) (Ping timeout: 248 seconds)
11:24:42 × homo quits (~homo@user/homo) (Ping timeout: 252 seconds)
11:26:08 homo_ is now known as homo
11:27:07 homo_ joins (~homo@37-33-136-207.bb.dnainternet.fi)
11:28:54 × homo_ quits (~homo@37-33-136-207.bb.dnainternet.fi) (Changing host)
11:28:54 homo_ joins (~homo@user/homo)
11:28:55 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
11:30:15 × homo quits (~homo@user/homo) (Ping timeout: 246 seconds)
11:30:21 homo_ is now known as homo
11:30:40 × Piedro quits (~Piedro@213.226.141.133) (Ping timeout: 240 seconds)
11:32:27 housemate joins (~housemate@124.187.109.206)
11:33:24 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
11:39:33 gmg joins (~user@user/gehmehgeh)
11:41:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
11:45:53 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
11:47:50 × housemate quits (~housemate@124.187.109.206) (Quit: Nothing to see here. I wasn't there. I take IRC seriously.)
11:51:19 sawilagar joins (~sawilagar@user/sawilagar)
11:51:39 pavonia joins (~user@user/siracusa)
11:54:23 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
11:56:31 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
12:01:00 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
12:03:04 × youthlic quits (~Thunderbi@user/youthlic) (Quit: youthlic)
12:04:06 × mrmr155334346318 quits (~mrmr@user/mrmr) (Quit: Bye, See ya later!)
12:04:22 × Guest78 quits (~Guest78@64.43.50.117) (Quit: Client closed)
12:11:54 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
12:16:27 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
12:17:23 × alexherbo2 quits (~alexherbo@2a02-8440-350e-cece-a50d-b49e-108d-0242.rev.sfr.net) (Remote host closed the connection)
12:27:16 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
12:27:44 wootehfoot joins (~wootehfoo@user/wootehfoot)
12:31:56 lxsameer joins (~lxsameer@Serene/lxsameer)
12:32:02 × son0p quits (~ff@186.121.98.118) (Ping timeout: 272 seconds)
12:34:00 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
12:35:29 mrmr155334346318 joins (~mrmr@user/mrmr)
12:42:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
12:46:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
12:47:14 alexherbo2 joins (~alexherbo@2a02-8440-350e-cece-fc33-ab37-4fc7-9825.rev.sfr.net)
12:49:49 × ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj)
12:50:14 ljdarj joins (~Thunderbi@user/ljdarj)
12:57:32 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
13:02:26 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
13:04:26 × agent314 quits (~quassel@149.40.50.111) (Ping timeout: 252 seconds)
13:08:40 califax_ joins (~califax@user/califx)
13:08:58 × califax quits (~califax@user/califx) (Remote host closed the connection)
13:09:54 califax_ is now known as califax
13:11:46 × kronicmage quits (~kronicmag@neotame.csclub.uwaterloo.ca) (Ping timeout: 252 seconds)
13:12:54 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
13:15:36 tnt2 joins (~Thunderbi@user/tnt1)
13:15:40 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds)
13:15:40 tnt2 is now known as tnt1
13:18:06 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
13:25:36 michalz joins (~michalz@185.246.207.203)
13:28:16 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
13:30:40 son0p joins (~ff@186.121.98.118)
13:33:06 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
13:38:45 × ft quits (~ft@p508db070.dip0.t-ipconnect.de) (Quit: leaving)
13:38:57 ft joins (~ft@p508db070.dip0.t-ipconnect.de)
13:40:34 × ft quits (~ft@p508db070.dip0.t-ipconnect.de) (Client Quit)
13:40:45 ft joins (~ft@p508db070.dip0.t-ipconnect.de)
13:43:09 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
13:47:42 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
13:50:41 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
13:52:57 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
13:58:33 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
14:05:25 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
14:08:11 × alexherbo2 quits (~alexherbo@2a02-8440-350e-cece-fc33-ab37-4fc7-9825.rev.sfr.net) (Remote host closed the connection)
14:11:55 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en)
14:13:20 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds)
14:15:05 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 244 seconds)
14:16:36 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
14:21:37 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
14:22:32 zenmov joins (~zenmov@user/zenmov)
14:26:57 × Digit quits (~user@user/digit) (Ping timeout: 265 seconds)
14:27:55 Smiles joins (uid551636@id-551636.lymington.irccloud.com)
14:31:57 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
14:35:21 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 252 seconds)
14:36:28 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
14:42:39 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
14:43:16 manwithluck joins (~manwithlu@194.177.28.164)
14:45:30 ljdarj joins (~Thunderbi@user/ljdarj)
14:47:12 × xff0x quits (~xff0x@p3704193-ipxg12201sapodori.hokkaido.ocn.ne.jp) (Ping timeout: 252 seconds)
14:48:22 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
14:51:08 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
14:59:18 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
15:03:25 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
15:04:10 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
15:06:02 lxsameer joins (~lxsameer@Serene/lxsameer)
15:07:42 JuanDaugherty joins (~juan@user/JuanDaugherty)
15:14:40 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
15:18:40 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Ping timeout: 265 seconds)
15:19:09 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
15:30:04 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
15:31:38 <haskellbridge> <thirdofmay18081814goya> I recall reading somewhere that modal types are given by monads
15:31:49 <haskellbridge> <thirdofmay18081814goya> can Haskell monads simulate modal types?
15:32:17 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 244 seconds)
15:33:26 JuanDaugherty joins (~juan@user/JuanDaugherty)
15:34:57 <ncf> do you mean anything precise by that
15:35:04 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
15:36:08 <haskellbridge> <thirdofmay18081814goya> well this could be a way to make that precise: a monad-encoding of a modal type is inhabited iff it's corresponding modal type is inhabited
15:38:00 <albet70> hello everyone
15:39:21 ljdarj joins (~Thunderbi@user/ljdarj)
15:40:29 <albet70> how to share or passing one variable between two async function? like there are async function f and g, jump between f and g with one variable so that f and g can both modify
15:45:09 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
15:47:13 <geekosaur> STM is the usual method
15:47:25 Digit joins (~user@user/digit)
15:51:32 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 265 seconds)
15:51:42 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
15:52:13 <probie> If it's just a single variable, `MVar`s might be sufficient
15:53:03 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
15:59:03 <albet70> what mvar is based on?
15:59:54 <geekosaur> it's a primitive synchronization variable
16:00:08 <geekosaur> well, not primitive, MutVar# is the primitive
16:00:26 <geekosaur> but it's a very low level thing
16:01:15 <int-e> MutVar# != MVar# (MutVar# is STRef/IORef)
16:01:21 <ski> thirdofmay18081814goya : "possible"-type modalities would be the ones which could be monadic, while "neccesary"-type ones could be comonadic
16:02:09 <albet70> I learned scheme a few years ago, I saw a article about call/cc to do coroutine, it can jump between two functions with variable, but I can't find that article now
16:02:25 <geekosaur> anyway, AIUI one shared var in entire program is atomicModifyIORef, one shared between two given threads is MVar, anything more requires something more complex and STM is preferred these days
16:02:54 <geekosaur> otherwise you risk deadlocks
16:03:12 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
16:03:14 <int-e> . o O ( deadlocks are bad, let's starve instead )
16:03:23 <albet70> like it capture k1 inside f, then call g with k1, then capture g's rest as k2, it jumps to k1 with k2
16:04:26 <albet70> what that is called?
16:07:11 <haskellbridge> <thirdofmay18081814goya> ski: I see! ty
16:07:45 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
16:18:35 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
16:18:55 × swistak quits (~swistak@185.21.216.141) (Quit: bye bye)
16:19:01 × roosterphant_ quits (~roosterph@185.21.217.76) (Remote host closed the connection)
16:19:12 swistak joins (~swistak@185.21.216.141)
16:19:24 roosterphant joins (~roosterph@185.21.217.76)
16:20:50 alecs joins (~alecs@61.pool85-58-154.dynamic.orange.es)
16:22:54 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
16:25:07 × alecs quits (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 252 seconds)
16:25:19 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
16:31:17 <ski> thirdofmay18081814goya : if `<>' represents "possibility" of some kind (alethic ("possible"), temporal ("sometimes","eventually/later","earlier/before"), epistemic ("is consistent with my knowledge / might hold for all i know"), doxastic ("is consistent with my belief", deontic ("permissible"), provability ("is consistent with derivability in the formal system"), ..), then if we assume `A |- B' holds, then
16:31:23 <ski> we can derive `A |- <> B' (under the condition of `A', `B' holds, so `B' is possible), and then we can derive `<> A |- <> B' (should `A' hold only possibly, `B' will then still hold possibly). first step is monadic unit
16:32:15 <ski> (`return'). second step is monadic extension (`(=<<)', `(>>=)'/"bind")
16:33:57 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
16:37:28 <ski> thirdofmay18081814goya : if `[]' represents "necessity" of some kind (alethic ("necessary"), temporal ("always","henceforth/hereafter","hitherto/heretofore"), epistemic ("is known by me"), doxastic ("is believed by me", deontic ("obligatory"), provability ("is provable in the formal system"), ..), then if we assume `A |- B' holds, then we can derive `[] A |- B' (under the stronger condition of `A' holding
16:37:34 <ski> necessarily, `A' still holds, so `B' is also still holds), and then we can derive `[] A |- [] B' (when `A' holds even necessarily, `B' will then also hold necessarily). first step is comonadic unit (`extract'). second step is comonadic "preservation" (`(<<=)', `(=>>)')
16:38:15 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
16:38:36 × gmg quits (~user@user/gehmehgeh) (Ping timeout: 264 seconds)
16:39:48 tnt2 joins (~Thunderbi@user/tnt1)
16:40:17 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds)
16:40:18 tnt2 is now known as tnt1
16:40:29 <ski> more generally, one can have a rule that if `[] Gamma |- A' (where `Gamma' is a collection of hypotheses considered conjunctively, and `[] Gamma' means `[]' applied to each one of them, individually), then `[] Gamma |- [] A' (or even : if `[] Gamma |- A , <> Delta', then `[] Gamma |- [] A , <> Delta', where `Delta' is a collection taken disjunctively (`,' on the right of `|-' means "or" roughly, while to the
16:40:35 <ski> left it means "and" roughly))
16:42:45 <ski> and, symmetrically, we can have a rule that if `[] Gamma , A |- <> Delta', then `[] Gamma , <> A |- <> Delta'
16:44:37 × toch quits (toch@user/toch) (Quit: WeeChat 4.5.0)
16:44:38 <ski> (or, if we want to restrict to single conclusions, just : if `[] Gamma , A |- <> B', then `[] Gamma , <> A |- <> B')
16:45:19 toch joins (toch@user/toch)
16:45:37 <haskellbridge> <thirdofmay18081814goya> woah thank you very much for the extensive comments! I'm studying these
16:45:51 <ski> albet70 : sounds like coroutines
16:46:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
16:49:34 <albet70> ski , but that coroutine passing variable between two functions
16:50:25 <albet70> or say passing function inside context into another function
16:50:38 econo_ joins (uid147250@id-147250.tinside.irccloud.com)
16:50:48 <albet70> how to archive that with async?
16:51:04 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
16:53:36 <ski> thirdofmay18081814goya : from what i've seen, it's more common for formalize modal logics in axiomatic / Hilbert-style (with possible axioms like `[] A |- A',`[] A |- [] [] A',`A |- [] <> A',`[] A |- <> A',`<> A |- [] <> A ',&c. depending on the particular modal logic in question that we're formalizing), rather than in a natural deduction, or in a sequent calculus (what i sketched above) style
16:55:00 tnt2 joins (~Thunderbi@user/tnt1)
16:55:03 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds)
16:55:03 tnt2 is now known as tnt1
16:56:19 <ski> albet70 : dunno whether it'd be reasonable with `async'. passing data (and not just the frozen control point) as "baton" back and forth between coroutines requires them to know about each other, or at least about the interface of the other(s), so would seem to assume synchronous communication
16:57:02 × Smiles quits (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity)
16:58:28 <ski> albet70 : btw, i literally did the "like it capture k1 inside f, then call g with k1, then capture g's rest as k2, it jumps to k1 with k2" thing, in Haskell, to do coroutines, to be able to jump back and forth between two parallel (and a priori independent) traversals of two data structures, combining their data "pointwise"/"coordinatewise"/"in lockstep"
16:59:50 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
17:00:21 rvalue joins (~rvalue@user/rvalue)
17:00:33 tnt2 joins (~Thunderbi@user/tnt1)
17:01:32 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
17:01:40 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds)
17:01:40 tnt2 is now known as tnt1
17:06:15 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
17:07:02 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
17:07:33 × toch quits (toch@user/toch) (Ping timeout: 248 seconds)
17:09:28 sinbad joins (~sinbad@user/sinbad)
17:09:39 toch joins (toch@user/toch)
17:10:54 gmg joins (~user@user/gehmehgeh)
17:11:33 <sinbad> How can I parse an empty line ("/n/n") between non-empty lines using readP?
17:13:33 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds)
17:22:46 <c_wraith> Usually you approach it from the other direction
17:23:23 <c_wraith> match the newlines in the stuff you care about. throw a (char '\n') parser between them.
17:23:50 <c_wraith> Note that you need to be using backslashes (\) for escape codes, not forward slashes (/)
17:24:48 <sinbad> c_wraith: yes I should have used \
17:25:11 <probie> Assuming you already know the last line wasn't empty, perhaps something like `count 2 (char "\n") >> look >>= \case { ('\n':_) -> pfail; _ -> pure () }`
17:26:22 <c_wraith> Here's my day 19 aoc parser. It literally matches (string "\n\n") at one point. https://github.com/chowells79/aoc/blob/main/2024/Day19.hs#L21-L31
17:27:49 × zenmov quits (~zenmov@user/zenmov) (Ping timeout: 272 seconds)
17:29:13 <c_wraith> And my day 17 parser: https://github.com/chowells79/aoc/blob/main/2024/Day17.hs#L33-L48 . It matches a series of lines including the terminal \n, then matches one more \n before the next section.
17:29:20 <c_wraith> Those are the two main ways
17:29:21 <albet70> ski , how you did it?
17:29:24 <enikar> sinbad: use (string "\n\n")
17:29:35 <enikar> it's what I use
17:30:05 <albet70> I found that 'yield' in python can do that
17:30:41 <enikar> ah! yield in python is awesome
17:31:23 × son0p quits (~ff@186.121.98.118) (Remote host closed the connection)
17:32:16 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
17:32:56 <monochrom> You can make your own yield in Haskell: https://www.vex.net/~trebla/haskell/cont.xhtml#yield
17:34:45 <albet70> call/cc in scheme can capture the outside/rest code of call/cc, I don't think Cont or callCC in haskell can do that
17:35:24 <albet70> callCC only capture what is inside callCC
17:35:27 son0p joins (~ff@186.121.98.118)
17:36:21 <enikar> there are arguments against call/cc.
17:36:54 × __monty__ quits (~toonn@user/toonn) (Ping timeout: 265 seconds)
17:38:00 <ski> albet70 : the challenge was to implement `zipWith' (or `zip', if you prefer), only traversing either input list (and only once), with a single call to `foldr' for each, not inspecting the lists in any way apart from that
17:38:11 <sinbad> c_wraith: thank you
17:38:34 <enikar> albet70: https://okmij.org/ftp/continuations/against-callcc.html
17:38:44 <ski> `callCC' is delimited by the `runCont'/`runContT', yes
17:39:12 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
17:41:42 <ski> (albet70 : and no recursive computation needed/permitted, apart from the one inside `foldr')
17:41:51 <albet70> enikar , but call/cc still in r4rs?
17:42:33 <albet70> ski , what's the delimited continuation
17:44:36 <probie> ski: That sounds like a fun challenge. I think I'll have a go
17:45:24 <ski> evalCont ca = ca `runCont` id -- `id' here is the initial ("empty") delimited/composable continuation
17:46:19 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:47:11 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
17:47:41 <enikar> albet70: yes, r4rs is quite old.
17:48:21 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
17:49:12 <ski> probie : i first solved it (out of curiosity), around 2007-04-10 (and made a smaller edit for elegance and generality, in 2011-06-14)
17:51:12 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: JuanDaugherty)
17:52:04 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds)
17:57:27 <albet70> can I say callCC is delimited continuation and call/cc is full contit?
17:58:45 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 246 seconds)
18:00:13 Guest78 joins (~Guest78@2a02:8084:1:6500::db)
18:02:57 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
18:09:12 <monochrom> callCC is global because there is no reset to scope it.
18:09:28 tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
18:09:43 <monochrom> Of course you get to say "but only within runCont" but it is not like you really have multiple levels of runCont.
18:10:06 <monochrom> Whereas with shift-reset you really always have multiple levels.
18:11:02 <monochrom> As Oleg points out, call/cc is not very nice. shift-reset is better. Even the Haskell Cont library provides shift-reset.
18:11:45 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds)
18:11:47 <albet70> is that redis distributed lock very like MVar?
18:12:55 <monochrom> And Python's yield corresponds to shift-reset rather than call/cc. https://www.cs.indiana.edu/~sabry/papers/yield.pdf
18:13:30 <albet70> monochrom , callCC can capture the rest code which is after it?
18:15:10 housemate joins (~housemate@125.63.162.34)
18:18:02 <monochrom> Although, when you instead look for extending Curry-Howard to classical logic, call/cc is Pierce's law and is exactly the one single thing you need to complete classical logic.
18:18:23 <monochrom> s/look for/look to/ # English is hard, I hate prepositions
18:19:35 Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
18:20:13 × housemate quits (~housemate@125.63.162.34) (Remote host closed the connection)
18:20:53 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 265 seconds)
18:20:56 Lord_of_Life_ is now known as Lord_of_Life
18:21:19 haver joins (~Enviosity@2.219.56.221)
18:22:04 <albet70> monochrom , Pierce's law is related to Yoneda embedding?
18:22:10 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
18:22:16 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
18:23:07 sinbad parts (~sinbad@user/sinbad) ()
18:24:10 × Enviosity_ quits (~Enviosity@2.219.56.221) (Ping timeout: 252 seconds)
18:27:10 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
18:29:30 <ski> resetCont :: Cont o o -> Cont p o
18:29:34 <ski> resetCont = return . evalCont
18:32:09 <monochrom> If you do use call/cc aka Pierce's law to extend Curry-Howard, then excluded middle executes like this story: https://www.cs.cmu.edu/~cmartens/if/dem.html#4.8 >:)
18:32:18 lxsameer joins (~lxsameer@Serene/lxsameer)
18:34:31 <monochrom> I heard of it last month on the haskell-cafe mailing list: https://mail.haskell.org/pipermail/haskell-cafe/2024-November/136916.html
18:36:41 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
18:37:32 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
18:38:45 <ncf> btw, is anyone aware of an elementary proof that pierce's law / call/cc is undefinable in system f or something? maybe using parametricity?
18:40:18 <ski> you can draw `call/cc', with a box in the style of "To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction" by David C. Keenan in 1996-08-27 - 2014-04-01 at <https://web.archive.org/web/20231128103508/https://dkeenan.com/Lambda/>, only that you'll need a line *exiting* a box abnormally (crossing the border), as opposed to *entering* (using a variable, inside a lambda,
18:40:24 <ski> where it was bound outside the lambda)
18:41:39 <ski> (`K'/"Kestrel" (`\x. \y. x') there is an example of the latter)
18:42:12 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
18:44:31 tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
18:44:38 <ncf> @free ((a -> b) -> a) -> a
18:44:38 <lambdabot> Try `free <ident>` or `free <ident> :: <type>`
18:44:45 <ncf> @free callCC :: ((a -> b) -> a) -> a
18:44:45 <lambdabot> (forall p q. g . p = q . f => f (h p) = k q) => f (callCC h) = callCC k
18:49:39 <monochrom> ncf: Interesting question! Thanks. Maybe excluded-middle is easier. So someone promises me ∀a. a + not a. By parametricity (very high-level-ly), it cannot say "I give you Left or Right depending on your a", it has to either "I give you Left regardless of a" or "I give you Right regardless of a". But always-Left breaks (a = false), always-Right also breaks (a = true).
18:50:25 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 248 seconds)
18:51:53 <ncf> yeah, it's easy to see for LEM (and you can always argue that call/cc implies LEM), but i wonder if there's a more direct story
18:52:55 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
18:53:21 <monochrom> That may be harder to understand when you finish it. :)
18:53:23 <ncf> for Martin-Löf type theory it's easy to prove that the type of pierce's law is not inhabited in the family model (presheaves over ∙ → ∙): https://gist.github.com/ncfavier/6ca209ab691f640a8d08e9f67bd041e1
18:54:06 <ncf> i'm not familiar enough with the semantics of system f to know if something similar can be done there
18:56:18 <monochrom> But hey I'm going to put it on the exam! (OK, I just mean: Suppose e :: ∀a. Either [a] (Maybe a). Prove: (always e = Left ...) or (always e = Right ...).)
18:59:40 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
19:04:17 <haskellbridge> <thirdofmay18081814goya> hm, in an FRP setting, suppose I want to model the signal function that takes two input signals: the first is the device's screen specs, and the second is an IO event representing a click, and the output is a coordinate of the click
19:04:30 <haskellbridge> <thirdofmay18081814goya> what should be the type of the IO event?
19:04:47 <haskellbridge> <thirdofmay18081814goya> hm, in an FRP setting, suppose I want to model the signal function that takes two input signals: the first is the device's screen specs, and the second is an IO event representing a click, and the output is the coordinates of the click
19:05:23 <geekosaur> (careful with those edits)
19:05:38 <haskellbridge> <thirdofmay18081814goya> uh right yes my bad
19:06:49 <monochrom> I'm OK with those edits. :)
19:07:06 <haskellbridge> <thirdofmay18081814goya> so the function has:
19:07:06 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/OhYpqzWlQxOOEZERbielBCRQ/4iEIbaNtSto (4 lines)
19:08:37 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Quit: ash3en)
19:09:05 ash3en joins (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207)
19:10:29 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
19:12:04 × ash3en quits (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Client Quit)
19:12:12 sinbad joins (~sinbad@user/sinbad)
19:14:03 ski . o O ( `(forall a. Either (f a) (g a)) -> Either (forall a. f a) (forall a. g a)' )
19:15:58 <haskellbridge> <thirdofmay18081814goya> hm... right that makes sense, I will be thinking about this formulation, thank you!
19:17:02 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
19:17:03 <ski> (afaik, you can't internalize this, in System F)
19:20:39 × sefidel quits (~sefidel@user/sefidel) (Remote host closed the connection)
19:20:55 <monochrom> Yeah, System F doesn't know that itself is parametric. :)
19:23:25 JuanDaugherty joins (~juan@user/JuanDaugherty)
19:23:33 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Remote host closed the connection)
19:24:12 sefidel joins (~sefidel@user/sefidel)
19:28:15 sinbad parts (~sinbad@user/sinbad) ()
19:28:32 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
19:29:15 zenmov joins (~zenmov@user/zenmov)
19:31:51 sk1lton joins (~sk1lton@user/sk1lton)
19:31:59 <sk1lton> https://pastejustit.com/3zb8ipyqbv
19:32:09 <sk1lton> Edna Skilton, a plump and flamboyant woman with areolas and nipples tattooed on her flabby, bulgy, and voluptuous elbows, was sitting in the stands at the North Charleston Coliseum, watching the South Carolina Stingrays play hockey. She was wearing a bright yellow tank top that hugged her ample bosom and a pair of neon green leggings that accentuated her curves. Her hair was styled in a bouffant that towered high above her head, and she wore a pair of
19:32:09 <sk1lton> oversized sunglasses that covered most of her face.
19:32:15 ChanServ sets mode +o monochrom
19:32:19 monochrom sets mode +b *!*@user/sk1lton
19:32:19 sk1lton is kicked by monochrom (sk1lton)
19:32:47 ski . o O ( "Internalizing Parametricity" (Ph. D. thesis) by Guilhem Moulin in 2016 at <https://publications.lib.chalmers.se/records/fulltext/235758/235758.pdf> )
19:32:54 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds)
19:35:20 housemate joins (~housemate@60.231.48.87)
19:35:59 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
19:36:58 machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
19:43:09 × housemate quits (~housemate@60.231.48.87) (Ping timeout: 260 seconds)
19:43:54 × son0p quits (~ff@186.121.98.118) (Quit: Leaving)
19:43:55 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
19:48:44 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
19:56:33 × manwithluck quits (~manwithlu@194.177.28.164) (Ping timeout: 248 seconds)
19:59:19 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:00:05 × caconym quits (~caconym@user/caconym) (Quit: bye)
20:00:44 caconym joins (~caconym@user/caconym)
20:04:19 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
20:04:19 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 264 seconds)
20:09:50 × gorignak quits (~gorignak@user/gorignak) (Read error: Connection reset by peer)
20:11:03 gorignak joins (~gorignak@user/gorignak)
20:12:24 Sgeo joins (~Sgeo@user/sgeo)
20:14:42 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:19:25 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
20:30:04 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:30:22 monochrom sets mode -o monochrom
20:32:57 × zenmov quits (~zenmov@user/zenmov) (Ping timeout: 276 seconds)
20:34:46 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds)
20:44:00 Jeanne-Kamikaze joins (~Jeanne-Ka@static-198-54-134-102.cust.tzulo.com)
20:45:27 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
20:50:20 × michalz quits (~michalz@185.246.207.203) (Remote host closed the connection)
20:52:01 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
21:03:31 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
21:08:42 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
21:13:03 × Spawns_Carpeting quits (~mobile@user/spawns-carpeting/x-6969421) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
21:13:55 zenmov joins (~zenmov@user/zenmov)
21:14:36 Spawns_Carpeting joins (~mobile@user/spawns-carpeting/x-6969421)
21:18:19 <haskellbridge> <thirdofmay18081814goya> hm, in FRP, what is the relationship between the signal function "PointlessButton :: Signal (Maybe ()) -> ?" and the rendering function "Render :: ? -> Signal (Nat, Nat) -> RGB"?
21:18:53 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
21:19:26 × CrunchyFlakes quits (~CrunchyFl@31.19.233.78) (Read error: Connection reset by peer)
21:19:46 <haskellbridge> <thirdofmay18081814goya> "type RGB = (Nat, Nat, Nat)"
21:20:21 <geekosaur> mm, wouldn't it be determined by whatever you want that button to do?
21:20:29 <haskellbridge> <thirdofmay18081814goya> so the render function takes the whole FRP circuit and produces a function "(Nat, Nat) -> RGB" that renders an image by specifying RGB value at each pixel
21:21:00 <haskellbridge> <thirdofmay18081814goya> geekosaur: suppose "PointlessButton" does nothing, and has only two possible renderings, a clicked form and a nonclicked form
21:21:49 CrunchyFlakes joins (~CrunchyFl@ip1f13e94e.dynamic.kabel-deutschland.de)
21:22:18 <haskellbridge> <thirdofmay18081814goya> we can think of them as two inhabitants of "(Nat, Nat) -> Maybe RGB" where the places the button is not rendered returns "None"
21:23:27 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
21:26:44 Square joins (~Square@user/square)
21:27:42 <haskellbridge> <thirdofmay18081814goya> what I'm wondering more precisely: what passes these two inhabitants to "Render", and what is passed to "Render" so that it knows which of these is the current one?
21:32:36 <haskellbridge> <thirdofmay18081814goya> one possibility is that "Render" receives "type AllPossibleComponentRenderings = [(Nat, Nat) -> Maybe RGB]" and some sort of array that tells it, at each sampling, which of these to compose together with "type Background = (Nat, Nat) -> RGB" to produce "type RenderingResult = (Nat, Nat) -> RGB"
21:33:12 Everything joins (~Everythin@195.138.86.118)
21:33:45 __monty__ joins (~toonn@user/toonn)
21:34:15 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
21:34:36 <haskellbridge> <thirdofmay18081814goya> but I'm having a hard time figuring out the "array that tells it which of these to compose with "Background"" part
21:34:42 × Jeanne-Kamikaze quits (~Jeanne-Ka@static-198-54-134-102.cust.tzulo.com) (Remote host closed the connection)
21:34:57 <haskellbridge> <thirdofmay18081814goya> or a binary vector
21:38:54 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds)
21:49:38 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
21:54:16 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
21:58:40 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 252 seconds)
21:59:04 tnt1 joins (~Thunderbi@user/tnt1)
22:03:04 tnt2 joins (~Thunderbi@user/tnt1)
22:03:33 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 248 seconds)
22:03:34 tnt2 is now known as tnt1
22:05:01 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:09:48 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds)
22:11:46 × target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving)
22:20:22 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:23:57 × zenmov quits (~zenmov@user/zenmov) (Ping timeout: 252 seconds)
22:27:16 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
22:36:38 tnt2 joins (~Thunderbi@user/tnt1)
22:37:06 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 276 seconds)
22:37:06 tnt2 is now known as tnt1
22:44:05 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
22:44:47 × szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
22:46:56 tnt2 joins (~Thunderbi@user/tnt1)
22:47:30 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 276 seconds)
22:47:30 tnt2 is now known as tnt1
22:48:21 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds)
22:51:52 × Square quits (~Square@user/square) (Remote host closed the connection)
22:53:03 Square2 joins (~Square4@user/square)
22:59:27 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
23:02:56 × Everything quits (~Everythin@195.138.86.118) (Quit: leaving)
23:02:57 tnt2 joins (~Thunderbi@user/tnt1)
23:03:56 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
23:04:18 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 246 seconds)
23:04:18 tnt2 is now known as tnt1
23:11:34 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
23:12:20 tnt2 joins (~Thunderbi@user/tnt1)
23:12:21 × xal quits (~xal@mx1.xal.systems) (Quit: bye)
23:12:56 × tnt1 quits (~Thunderbi@user/tnt1) (Ping timeout: 244 seconds)
23:12:56 tnt2 is now known as tnt1
23:13:11 xal joins (~xal@mx1.xal.systems)
23:13:54 weary-traveler joins (~user@user/user363627)
23:14:51 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
23:19:56 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds)
23:24:31 × yaroot quits (~yaroot@2400:4052:ac0:d901:1cf4:2aff:fe51:c04c) (Read error: Connection reset by peer)
23:24:45 yaroot joins (~yaroot@p3031163-ipngn4701souka.saitama.ocn.ne.jp)
23:25:18 peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:30:14 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
23:32:31 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
23:35:06 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds)
23:36:33 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
23:45:55 merijn joins (~merijn@128-137-045-062.dynamic.caiway.nl)
23:50:31 × merijn quits (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 264 seconds)
23:50:49 zenmov joins (~zenmov@user/zenmov)

All times are in UTC on 2024-12-22.