Home liberachat/#haskell: Logs Calendar

Logs on 2024-05-21 (liberachat/#haskell)

00:28:57 × ystael quits (~ystael@user/ystael) (Ping timeout: 268 seconds)
00:34:25 × it_ quits (~quassel@v2202212189510211193.supersrv.de) (Quit: ,o>)
00:34:50 → it_ joins (~quassel@v2202212189510211193.supersrv.de)
00:35:17 × szkl quits (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity)
00:35:35 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
00:49:44 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
00:50:59 × demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 264 seconds)
00:57:05 → hsw joins (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net)
01:05:08 × xdminsy quits (~xdminsy@117.147.70.240) (Ping timeout: 260 seconds)
01:06:10 → xdminsy joins (~xdminsy@117.147.70.240)
01:11:48 → sayola joins (~sayola@ip-109-42-242-108.web.vodafone.de)
01:13:41 × sayola1 quits (~sayola@ip-109-42-241-204.web.vodafone.de) (Ping timeout: 240 seconds)
01:15:16 × xdminsy quits (~xdminsy@117.147.70.240) (Read error: Connection reset by peer)
01:16:04 → xdminsy joins (~xdminsy@117.147.70.240)
01:20:39 × xdminsy quits (~xdminsy@117.147.70.240) (Read error: Connection reset by peer)
01:21:46 → xdminsy joins (~xdminsy@117.147.70.240)
01:26:51 × xff0x quits (~xff0x@2405:6580:b080:900:b527:98ae:f93a:e494) (Ping timeout: 255 seconds)
01:28:40 × xdminsy quits (~xdminsy@117.147.70.240) (Read error: Connection reset by peer)
01:29:01 → xdminsy joins (~xdminsy@117.147.70.240)
02:00:01 × fliife quits (~fliife@user/fliife) (Quit: ZNC 1.8.2+deb2build5 - https://znc.in)
02:00:48 → fliife joins (~fliife@user/fliife)
02:00:53 × otto_s quits (~user@p5de2fafb.dip0.t-ipconnect.de) (Ping timeout: 240 seconds)
02:02:56 → otto_s joins (~user@p5de2f060.dip0.t-ipconnect.de)
02:05:59 × td_ quits (~td@i53870921.versanet.de) (Ping timeout: 264 seconds)
02:07:44 → td_ joins (~td@i5387090E.versanet.de)
02:14:05 × agent314 quits (~quassel@184.75.215.3) (Ping timeout: 240 seconds)
02:14:11 → xff0x joins (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
02:15:07 → agent314 joins (~quassel@104.129.57.116)
02:15:35 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 264 seconds)
02:40:45 → demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net)
02:41:23 × justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6)
02:41:37 → justsomeguy joins (~justsomeg@user/justsomeguy)
02:44:59 × demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 252 seconds)
02:50:46 → joeyadams joins (~joeyadams@2603:6010:5100:2ed:64b6:9e88:7ce7:a120)
03:06:52 × Midjak quits (~MarciZ@82.66.147.146) (Quit: This computer has gone to sleep)
03:11:23 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds)
03:17:17 × yin quits (~yin@user/zero) (Ping timeout: 240 seconds)
03:28:11 × aforemny_ quits (~aforemny@i59F516F9.versanet.de) (Ping timeout: 264 seconds)
03:28:38 → aforemny joins (~aforemny@2001:9e8:6cca:4800:37b5:fb76:9e3f:6a26)
03:42:48 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:49:24 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
03:52:55 × justsomeguy quits (~justsomeg@user/justsomeguy) (Quit: WeeChat 3.6)
03:56:02 → demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net)
04:00:35 × demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 264 seconds)
04:26:23 × agent314 quits (~quassel@104.129.57.116) (Ping timeout: 264 seconds)
04:26:36 → agent314 joins (~quassel@162.219.176.19)
04:34:50 → michalz joins (~michalz@185.246.207.203)
04:35:05 × michalz quits (~michalz@185.246.207.203) (Client Quit)
04:37:54 → michalz joins (~michalz@185.246.207.221)
04:46:50 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
05:17:01 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
05:18:08 → zetef joins (~quassel@5.2.182.99)
05:20:52 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
05:27:43 → y04nn joins (~username@2a03:1b20:8:f011::e10d)
05:30:07 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
05:30:42 → vladl joins (~vladl@24.35.90.183)
05:37:18 × johnw_ quits (~johnw@69.62.242.138) (Quit: ZNC - http://znc.in)
05:38:50 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
05:40:59 → demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net)
05:41:29 <vladl> What patterns are present in a recursion scheme that requires synchronization? For example, recursively interpolating subpixels in an image, where the interpolation step requires the parent pixel neighborhood? The subpixels get folded back into the original resolution, so this is almost a hylomorphism, except the coalgebra gets "split" over the synchronization step. This seems like a common pattern but I
05:41:35 <vladl> can't really find much on it, which could definitely be a skill issue. I read "Fantastic Morphisms and where to find them" but none of these really fit the bill. There's a problem on tree nexuses in Richard Bird's Pearls of Functional Algorithm design that I went through that, again, seemed very close to what I wanted but I couldn't make the pieces fit.
05:45:55 × demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 268 seconds)
05:50:40 <probie> I don't quite understand what you mean by "synchronization" here
05:53:11 geekosaur is thinking this sounds more like a comonad
05:53:39 <vladl> At a given resolution j, before interpolating the subpixels at resolution j+1, the neighboring (sub)pixels at resolution j have to have been computed. So we need to sync layer-by-layer. Synchronization like a fence or a barrier.
05:54:55 → johnw joins (~johnw@69.62.242.138)
05:57:35 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
05:57:40 <vladl> Yes I think I see a comonad in there too, but its also split. Like, lets suppose a 1D array of pixels p with neighborhoods w, so something like [w p]. We have a (w p -> p), but in order to extend and get a (w p) out, we have to step all the way out of the [] in order to propagate neighbor values. So we can go [p] -> [w p], but that [] prevents me from making it a proper comonad.
05:58:13 <probie> I don't see what requires you to synchronize layer-by-layer. A subpixel merely requires its neighbours at the previous resolution to have been computed, not the entire previous layer
05:59:11 <vladl> That's true but I'm relaxing my focus to the layer scale in hopes of making it easier for me to reason about
06:00:39 <vladl> Also because my particular use case ultimately does need to synchonize layer-by-layer for other reasons (memory allocation strategy) so I may as well
06:01:56 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
06:10:56 → demon-cat joins (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net)
06:13:25 → internatetional joins (~nate@182.2.51.214)
06:13:53 × internatetional quits (~nate@182.2.51.214) (Max SendQ exceeded)
06:14:11 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
06:15:35 × demon-cat quits (~demon-cat@dund-15-b2-v4wan-169642-cust1347.vm6.cable.virginm.net) (Ping timeout: 264 seconds)
06:18:56 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
06:20:24 <vladl> Actually, scratch that - we don't have a (w p -> p), we have a (w p -> f p), where f is the coalgebra functor (what contains the subpixels). So the comonad situation is even messier.
06:21:35 <vladl> Its like... taking an anamorphism and a comonad and trying to thread them through one another somehow.
06:21:38 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
06:22:50 <vladl> Or, hopefully, I am just overcomplicating things and there is some more elegant formalism for this out there
06:34:48 ski isn't too clear on the concrete example with subpixel interpolation
06:36:01 <ski> you're building a quadtree of the pixels, or something ?
06:37:09 <vladl> You guessed right. If it matters, the pixels are actually fluid density distributions and the interpolation is meant to refine the grid cells until they're fine enough for the fluid to advect across in one time step.
06:37:39 <ski> hm, or maybe considering a rectangle of pixels, and then a rectangle of all windows around each pixel, and then a rectangle of all windows around those, &c. (so this is a DAG, not a tree) ?
06:38:49 <vladl> Well it is a tree in the sense that every parent cell is exactly decomposed into its child cells, like they overlap. But in terms of data dependencies, it is a DAG.
06:38:50 <ski> (windows of a particular fixed size, in terms of the elements of the layer below, say)
06:39:32 ski doesn't know the term "advect"
06:40:06 <vladl> It just means the movement of materials. So basically it is the fluid traversing space.
06:40:09 <ski> does two adjacent parent cells share child cells ?
06:40:59 <vladl> No, no child cells are shared. So imagine each pixel gets broken up into 4 child pixels, but the values of the child pixels gets interpolated from the parent pixels and its adjacent neighbors (for a first-order interpolation scheme)
06:41:58 <vladl> Er, cells, sorry, I should stop mixing terminology
06:42:05 <ski> hm, interpolated from parent cell, and parentsibling cells ? or also from cousin cells ?
06:42:21 → sayola1 joins (~sayola@ip-109-42-241-195.web.vodafone.de)
06:42:34 <vladl> Only from parent sibling cells. So a cell at resolution j only depends on cell values at resolutoin j-1
06:43:28 × sayola quits (~sayola@ip-109-42-242-108.web.vodafone.de) (Ping timeout: 260 seconds)
06:43:41 <ski> mhm
06:44:00 <ski> so how does information flow ? only from root towards leaves ?
06:44:07 <ski> hmm
06:44:08 × sayola1 quits (~sayola@ip-109-42-241-195.web.vodafone.de) (Read error: Connection reset by peer)
06:44:29 <ski> well, to sibling children as well, yea
06:44:50 <vladl> Both ways, but not at the same time. We unfold all the way, then do some transformations, and then fold it back up to the original resolution.
06:45:49 <ski> mhm, so first stage is basically from root toward leaves (but including from siblings to children). and then later from leaves to root again ?
06:46:36 <vladl> so a 1D example, say you have [x0, x1, x2, x3, x4...] and you want to expand x2 into [y0, y1], then y0 = f 0 [x1, x2, x3] and y1 = f 1 [x1, x2, x3] for some interpolation function f
06:46:40 <vladl> yes
06:46:51 → sayola joins (~sayola@ip-109-42-241-195.web.vodafone.de)
06:48:51 <ski> hm, i see
06:49:03 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
06:49:25 <ski> (or `[y0,y1] = g [x1,x2,x3]')
06:49:38 <vladl> yes, that's more accurate
06:50:06 <ski> so this would be `w p -> f p'
06:50:16 <vladl> yes, exactly
06:53:07 → acidjnk_new joins (~acidjnk@p200300d6e714dc192d105e993ca958d7.dip0.t-ipconnect.de)
06:53:21 <ski> still not following what you mean by the synchronization
06:55:09 <vladl> so, suppose we have [[y0, y1], [y2, y3], ...] from the expansion and we flattened it down to [y0, y1, y2, y3,...]. So we want to expand y1 into [z0,z1] but we need [y0, y1, y2] to do this. but x2 only computes y0 and y1, so we need x3 to have been expanded into y2 and y3 before we can compute z0,z1
06:56:25 <vladl> so z's have to wait until all of the y's in their interpolation domain are done
06:57:09 <vladl> which means x2 and x3 have to both finish their expansions before either y1 or y2 can be expanded
06:58:24 <ski> "but x2 only computes y0 and y1, so we need x3" -- hm, shouldn't `x2' and `x3' be `x0' and `x1' ?
06:59:05 <ski> (hm, or maybe you don't have cropped windows/neighbourhoods at the edges. that would make it `x1' and `x2' though, i think)
06:59:36 <vladl> we don't expand x0, because it doesn't have a complete interpolation domain
06:59:58 <ski> mm, right
07:03:54 <vladl> And then i just try to simplify it for myself and consider dependencies at the scale of an entire layer at a time, instead of worrying about the implicit DAG in the window-wise dependencies
07:04:48 <ski> hmm .. so i guess you only need siblings,cousins,&c. ("same generation") up to a common ancestor `n' levels up, where `n' would depend on the width of `w' and the branching factor of `f'
07:05:29 <ski> (only thinking of fairly "regular" `w' and `f' here (e.g. probably linear), rather than say more arbitrary ones)
07:05:35 → cfricke joins (~cfricke@user/cfricke)
07:06:07 <ski> at least, for your example above, `n' would seem to be `2'
07:06:08 <vladl> yes, but note the common ancestor could be pretty far up, if the cell's position is near a power-of-two.
07:06:18 <ski> hmm
07:06:30 <ski> oh right. i was misthinking here
07:08:02 <ski> the flattening, to generate `w', is complicating stuff
07:09:09 <ski> "consider dependencies at the scale of an entire layer at a time" -- i suppose you mean generating a layer completely, before increasing the resolution. is this what you meant by "synchronization" ?
07:09:32 <vladl> yes. the flattening complicates things significantly, and yes that is what i mean by synchronization
07:13:58 <ski> given `t p', you can get to `t (w p)', and then to `t (f p)'. then that becomes `t p' with one level deeper
07:16:09 <vladl> yes. t needs to be able to absorb f (and remember it so it can form it later) so it seems like a tree with layer-wise views
07:19:35 <ski> i guess, something like `data TreeD f :: Nat -> * -> * where Leaf :: TreeD f Zero p; Branch :: f (TreeD f n p) -> TreeD f (Succ n) p' or `data TreeB f p = Conquer p | Divide (TreeB f (f p))'
07:20:22 <ski> (where `TreeB f p' amounts to `exists n :: Nat. TreeD f n p')
07:20:58 <ski> the interesting part, of course, is how to do the `t p -> t (w p)' part
07:24:52 <vladl> Yeah, something like that
07:25:41 <ski> .. i'm wondering if you could carry siblings with you, as you go down, so that you don't have to traverse arbitarily high up again to retrieve them
07:26:24 <vladl> So the way I do it in my specific case, is that, during the unfolding, each cell carries with it an object called a "topology" that you can basically think of as a list of pointers to the neighbors
07:26:49 <vladl> So when a cell gets expanded, it actually computes this right away, so it knows from the moment of birth where its neighbors are, so to speak
07:27:14 <ski> hm, so instead of `t p >-> t (w p) >-> t (f p)', could one do `t (w p) >-> t (w (f p)) >-> t (f (w p))' ?
07:28:09 <vladl> i don't think so, because the new cell only knows where its neighbors are, not what their values are
07:29:22 <ski> mhm
07:30:52 <vladl> so in my case, in a sense i have to pair the topology with the entire parent layer (since the offsets are with respect to the layer) in order to compute the child cells
07:31:50 → chele joins (~chele@user/chele)
07:32:31 → ubert joins (~Thunderbi@p200300ecdf1a44e6bddfe2bf28cca96e.dip0.t-ipconnect.de)
07:33:10 <vladl> that's another reason I go layer-by-layer, I can access neighbors in O(1) and I only have to store 2 layers at a time
07:33:21 <vladl> instead of O(log n) and storing the entire tree
07:34:13 <ski> yup, just like dynamic programming with fixed memory/history
07:34:53 → kuribas joins (~user@ptr-17d51encis8jg2ccf48.18120a2.ip6.access.telenet.be)
07:36:00 <vladl> yeah, and I was considering the dynamorphism as a model but its that lateral dependency that trips me up.
07:36:59 <ski> (hm, this all is making me think of "structure syntax" now .. although that's tangential to what you're pondering)
07:38:39 <vladl> you mean like how ListF a b is a functor over its recursive structure, that kind of thing?
07:39:54 <ski> well .. it's an idea i've been pondeing, on and off. basically, given a structure/collection with elements, i want to name the structure (the layer(s)) itself, separately from the elements
07:41:39 × ubert quits (~Thunderbi@p200300ecdf1a44e6bddfe2bf28cca96e.dip0.t-ipconnect.de) (Quit: ubert)
07:42:45 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
07:42:49 <ski> e.g. with `concat :: [[a]] -> [a]' and `sum :: [Integer] -> Integer' we have a law `sum . map sum = sum . concat'. i was to express this as `sum (| l0 ; sum (| l1 ; n |) |) = sum (| concat (| l0,l1 |) ; n |)'. here `l0' is the name of the outer list structure, and `l1' is the name of each inner list structure (it's plural), and `n' is the name of each element (it's doubly plural)
07:43:06 <ski> s/i was to/i want to/
07:48:51 <vladl> i think i'm following. i read `sum(| a ; b |)` as sum of b's ranging over a, so this expression shows how different views of the structure relate to one another, which tells you about the structure as a whole
07:49:30 <vladl> s/expression/equation
07:51:37 <vladl> i'm guessing you might be able to derive equivalent-but-different traversals if you had some syntax like that?
07:51:58 <ski> (and then i want to be able to say things like `[] -> Maybe', which would be a right kan extension. `([] -> Maybe) a' amounting to `forall b. (a -> [b]) -> Maybe b'. and `(exists n. t n) a', i think (?), amounting to `exists n. t n a' (and similarly for `forall'))
07:52:49 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
07:53:11 <ski> `sum (| a ; b |)' sums all the `b's inside the `a' structure. `concat (| l0,l1 |)' concatenates ("flattens") the `l0' and `l1' structures (the latter being contained inside the former). note that there are no elements mentioned here (hence no `;', just `,')
07:54:12 <vladl> we don't think of l1 as elements of l0?
07:54:25 <ski> basically, it's an attempt to make a calculus where you can name individual structures, or layers, *without* including the contents/elements in that name. *separating* structure from contents
07:54:44 <ski> concat :: [] . [] -> []
07:55:07 → danse-nr3 joins (~danse-nr3@151.35.171.208)
07:55:13 <ski> this is why it is `concat (| l0,l1 |)', the `.' (composition) means that you call `concat' with two layers (`l0' and `l1' here)
07:55:24 <ski> (and the result is also a list layer)
07:56:15 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
07:56:16 <ski> so, polymorphic operations don't need to mention the elements of the type parameters. but `sum' involves both the structure and the elements, so it still needs to mention both
07:56:55 <vladl> i see now
07:57:32 <ski> (`sum' is like a monoid action, `[]' acting on `Integer'. the law involving `concat' and `sum' above is similar to e.g. `(x * y) * v = x * (y * v)' law for scalars `x',`y' and vector `v')
08:00:13 <ski> part of the point here is to avoid having to spell out annoying `fmap's, to manipulate the correct layer of a structure
08:01:49 <ski> like, which is more readable, `join . fmap join = join . join', or `join (| m0,join (| m1,m2 |) |) = join (| join (| m0,m1 |),m2 |)' ?
08:02:49 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
08:02:57 <ski> i should also say that this isn't just meant for expressing laws, but also for defining things. it's just that i'm drawing inspiration from some laws
08:05:55 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
08:07:17 × son0p quits (~ff@186.121.14.247) (Ping timeout: 240 seconds)
08:08:02 → Square2 joins (~Square4@user/square)
08:08:22 <vladl> so instead of using fmap which says "just give me the function, i know how to map it over me" the structure syntax shows explicitly where the function gets applied, in terms of the part-to-whole relationship (the nature of which is abstracted over by the syntax) of the structure and its substructures?
08:08:24 × danse-nr3 quits (~danse-nr3@151.35.171.208) (Ping timeout: 260 seconds)
08:08:34 → gmg joins (~user@user/gehmehgeh)
08:08:59 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 268 seconds)
08:09:19 → Nixkernal joins (~Nixkernal@240.17.194.178.dynamic.wline.res.cust.swisscom.ch)
08:10:04 <vladl> so you end up defining the law by naming the substructures in the operations, without reference to the elements if they're not relevant to the calculation
08:11:12 <ski> yea .. it's basically a pointful syntax, but for function kinds (so having expressions `e', where `e :: f', where `f :: * -> *', say), rather than for concrete kinds (plain expressions `e' where `e :: t' and `t :: *')
08:11:51 <ski> (well, preferably it'd work for `f :: k0 -> k1' ..)
08:12:12 <ski> yes
08:12:26 <ski> or defining the operation
08:16:27 → danse-nr3 joins (~danse-nr3@151.35.171.208)
08:17:35 → __monty__ joins (~toonn@user/toonn)
08:22:22 <ski> something like
08:22:29 <ski> data List :: * -> *
08:22:39 <ski> where
08:22:58 <ski> Nil :: ( ) -> List
08:23:17 <ski> Cons :: (Identity,List) -> List
08:23:28 <ski> and then you can do
08:23:45 <ski> append :: (List,List) -> List
08:24:02 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
08:24:33 <ski> append (Nil ( ),l1) = l1
08:24:52 <ski> append (Cons ((||),l0),l1) = Cons ((||),append (l0,l1))
08:24:54 <ski> and
08:25:00 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
08:25:08 <ski> concat :: List . List -> List
08:26:03 <ski> concat (| Nil ( ),l1 |) = Nil ( )
08:26:22 <ski> concat (| Cons ((||),l0),l1 |) = append (l1,concat (| l0,l1 |))
08:27:32 <ski> (note that `f . g -> h' here curries as `f -> g -> h' (and `Identity -> h' as `h'). `(f,g) -> h' does not curry (and nor does `() -> h'))
08:28:29 <ski> the `(||)' in the `Cons' case of `append' basically indicates the place of the element (the "hole", since elements are not explicitly mentioned in these operations)
08:28:57 × danse-nr3 quits (~danse-nr3@151.35.171.208) (Ping timeout: 255 seconds)
08:29:48 → danse-nr3 joins (~danse-nr3@151.35.171.208)
08:30:34 <ski> note that, in the `Cons' case of `concat', because `l1' is plural, in the first argument of `append' (whose domain is a (lifted) product, not a composition), `l1' refers to the first list (which is pointed out by the `(||)', in the pattern). wihle in the second argument of `append', `l1' refers to all the other lists, living under the `l0' list structure
08:32:46 <vladl> ah yes that makes sense now
08:33:04 × ft quits (~ft@p508db8fc.dip0.t-ipconnect.de) (Quit: leaving)
08:33:23 <ski> .. it's a bit weird and unusual to think in these terms
08:33:26 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
08:34:22 <ski> and i'm not too sure how more generally useful it would be .. but it seems like an interesting idea to explore, regardless, to see how far one can push it, how much it can make sense, and perhaps how much can be incorporated in such a system
08:36:59 <ski> the type system for this requires keeping track of an *ordered* context/environment of variable typings ..
08:37:59 <ski> .. which i guess is another reason i've semi-recently been interested in grokking ordered logic (also for its own sake, e.g. for use as a logic programming language, or a logical framework)
08:42:30 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection)
08:43:13 → sord937 joins (~sord937@gateway/tor-sasl/sord937)
08:46:06 × ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds)
08:47:04 → ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:6584:33d2:35a2:fd74)
08:48:06 → ChaiTRex joins (~ChaiTRex@user/chaitrex)
08:49:59 → lxsameer joins (~lxsameer@Serene/lxsameer)
08:54:08 × danse-nr3 quits (~danse-nr3@151.35.171.208) (Ping timeout: 260 seconds)
08:57:59 → danse-nr3 joins (~danse-nr3@151.35.171.208)
09:04:07 <tomsmeding> why is Ord a superclass of Real?
09:04:45 <ncf> the reals are ordered aren't they
09:05:02 <tomsmeding> you have a point
09:05:04 <ncf> well i guess not decidably so
09:05:20 × danse-nr3 quits (~danse-nr3@151.35.171.208) (Ping timeout: 260 seconds)
09:05:32 <tomsmeding> I guess my actual X question is: why are all the numeric classes specifically for single scalars
09:05:41 <tomsmeding> there's no sensible way to make arrays an instance of the numeric hierarchy
09:06:11 <tomsmeding> if you squint on fromInteger you can maybe make Num work, but that's as far as you get
09:06:14 → danse-nr3 joins (~danse-nr3@151.35.171.208)
09:07:46 <ski> it's a mess
09:21:29 <mauke> the numeric classes lift straightforwardly into Applicative
09:21:38 <mauke> so [a] works fine :-)
09:22:29 × Flow quits (~none@gentoo/developer/flow) (Ping timeout: 240 seconds)
09:22:38 <int-e> > liftA2 (+) [1,2] [10,20]
09:22:39 <lambdabot> [11,21,12,22]
09:22:51 <int-e> is that what you want though :)
09:24:27 <mauke> WYGIWYG
09:24:45 <int-e> I'll give you that it is /a/ (non-commutative) ring.
09:27:53 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
09:30:12 <tomsmeding> the numeric classes lift straightforwardly into applicative?
09:30:22 <tomsmeding> > liftA toInteger [1,2]
09:30:24 <lambdabot> [1,2]
09:30:42 <tomsmeding> okay that typechecks as-is but it's not a valid definition of toInteger :p
09:31:00 <tomsmeding> goes wrong at Num(fromInteger) already
09:31:25 <tomsmeding> and everything breaks down once you get to Real, RealFrac and RealFloat
09:31:47 <tomsmeding> (decldeFloat :: a -> (Integer, Int) ?)
09:31:53 <ski> fromInteger = pure . fromInteger
09:31:53 <tomsmeding> *decodeFloat
09:32:25 <tomsmeding> ski: okay I concede that one, but what about toInteger :p
09:32:50 <tomsmeding> though that's a very questionable definition for fromInteger on arrays
09:34:10 <ski> replication is sensible for pointwise operations
09:34:31 <tomsmeding> it is
09:34:34 <tomsmeding> those are the easy ones
09:34:43 → noumenon joins (~noumenon@113.51-175-156.customer.lyse.net)
09:38:16 → Flow joins (~none@gentoo/developer/flow)
09:42:43 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
09:57:06 × danse-nr3 quits (~danse-nr3@151.35.171.208) (Remote host closed the connection)
09:57:26 × rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer)
09:57:58 → rvalue joins (~rvalue@user/rvalue)
09:58:26 → danse-nr3 joins (~danse-nr3@151.35.171.208)
10:00:49 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
10:01:19 × danse-nr3 quits (~danse-nr3@151.35.171.208) (Read error: Connection reset by peer)
10:02:59 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
10:03:26 → sawilagar joins (~sawilagar@user/sawilagar)
10:03:43 → euleritian joins (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de)
10:04:13 × euleritian quits (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
10:04:38 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
10:04:51 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
10:05:21 → Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
10:09:23 × xff0x quits (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds)
10:11:03 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
10:11:37 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
10:12:38 → danse-nr3 joins (~danse-nr3@151.35.171.208)
10:23:16 × aryah quits (~aryah@141-138-38-218.dsl.iskon.hr) (Read error: Connection reset by peer)
10:25:03 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 255 seconds)
10:28:27 → son0p joins (~ff@181.32.157.144)
10:39:55 × joeyadams quits (~joeyadams@2603:6010:5100:2ed:64b6:9e88:7ce7:a120) (Quit: Leaving)
10:40:36 × ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:6584:33d2:35a2:fd74) (Remote host closed the connection)
10:40:49 → ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:f77c:428b:229c:4616)
10:47:47 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
10:53:59 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
10:54:24 → euleritian joins (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de)
10:54:33 → yin joins (~yin@user/zero)
10:56:53 × danse-nr3 quits (~danse-nr3@151.35.171.208) (Ping timeout: 240 seconds)
11:01:58 × cfricke quits (~cfricke@user/cfricke) (Ping timeout: 255 seconds)
11:04:06 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
11:07:42 × noumenon quits (~noumenon@113.51-175-156.customer.lyse.net) (Read error: Connection reset by peer)
11:08:17 → lortabac joins (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
11:13:42 → xff0x joins (~xff0x@2405:6580:b080:900:6e2f:a302:dfa:99b5)
11:16:18 → CiaoSen joins (~Jura@2a05:5800:2b2:8e00:e6b9:7aff:fe80:3d03)
11:19:29 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
11:19:56 → cfricke joins (~cfricke@user/cfricke)
11:20:34 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
11:27:29 → joeyadams joins (~joeyadams@2603:6010:5100:2ed:eb4a:233c:d82d:5868)
11:29:49 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
11:30:55 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
11:35:57 → Lycurgus joins (~georg@user/Lycurgus)
11:42:49 × euleritian quits (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
11:43:17 → euleritian joins (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de)
11:46:33 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
11:49:45 × jcarpenter2 quits (~lol@2603:3016:1e01:b940:892b:2549:5c20:9c9b) (Ping timeout: 268 seconds)
11:55:40 × cfricke quits (~cfricke@user/cfricke) (Ping timeout: 256 seconds)
11:56:27 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Quit: WeeChat 4.1.2)
11:57:10 × joeyadams quits (~joeyadams@2603:6010:5100:2ed:eb4a:233c:d82d:5868) (Quit: Leaving)
11:57:49 × p3n quits (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (Quit: ZNC 1.8.2 - https://znc.in)
11:58:15 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
12:00:26 → p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1)
12:02:59 × yin quits (~yin@user/zero) (Ping timeout: 264 seconds)
12:04:08 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
12:08:55 × euleritian quits (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
12:09:12 → euleritian joins (~euleritia@77.22.252.56)
12:09:32 → yin joins (~yin@user/zero)
12:13:48 × euleritian quits (~euleritia@77.22.252.56) (Ping timeout: 268 seconds)
12:14:02 → euleritian joins (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de)
12:22:56 → cfricke joins (~cfricke@user/cfricke)
12:23:12 × euleritian quits (~euleritia@dynamic-176-006-198-126.176.6.pool.telefonica.de) (Ping timeout: 260 seconds)
12:24:29 → euleritian joins (~euleritia@dynamic-176-001-018-229.176.1.pool.telefonica.de)
12:28:43 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
12:35:48 × haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb2 - https://znc.in)
12:39:32 × cfricke quits (~cfricke@user/cfricke) (Ping timeout: 260 seconds)
12:41:33 × lortabac quits (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.1)
12:51:00 → haritz joins (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220)
12:51:00 × haritz quits (~hrtz@2a02:8010:65b5:0:6009:6384:e3cb:2220) (Changing host)
12:51:00 → haritz joins (~hrtz@user/haritz)
12:52:33 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
12:54:14 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
12:55:53 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
13:08:20 → cfricke joins (~cfricke@user/cfricke)
13:22:22 → ystael joins (~ystael@user/ystael)
13:33:05 × acidjnk_new quits (~acidjnk@p200300d6e714dc192d105e993ca958d7.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
13:34:34 weechat is now known as dminuoso
13:34:51 × Maxdamantus quits (~Maxdamant@user/maxdamantus) (Ping timeout: 260 seconds)
13:35:31 → Maxdamantus joins (~Maxdamant@user/maxdamantus)
13:36:35 × euleritian quits (~euleritia@dynamic-176-001-018-229.176.1.pool.telefonica.de) (Ping timeout: 264 seconds)
13:37:03 → euleritian joins (~euleritia@dynamic-176-006-196-082.176.6.pool.telefonica.de)
13:43:08 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
13:56:29 × zetef quits (~quassel@5.2.182.99) (Remote host closed the connection)
14:01:19 × haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb2 - https://znc.in)
14:01:50 → haritz joins (~hrtz@82-69-11-11.dsl.in-addr.zen.co.uk)
14:03:40 × haritz quits (~hrtz@82-69-11-11.dsl.in-addr.zen.co.uk) (Changing host)
14:03:40 → haritz joins (~hrtz@user/haritz)
14:04:15 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Quit: Lost terminal)
14:13:00 × cfricke quits (~cfricke@user/cfricke) (Quit: WeeChat 4.2.2)
14:14:29 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 240 seconds)
14:21:39 → danse-nr3 joins (~danse-nr3@151.35.136.250)
14:27:34 × TheCoffeMaker quits (~TheCoffeM@user/thecoffemaker) (Quit: So long and thanks for all the fish)
14:27:55 → TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
14:30:12 × haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in)
14:32:38 → haritz joins (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737)
14:32:41 × haritz quits (~hrtz@2a02:8010:65b5:0:5d9a:9bab:ee5e:b737) (Changing host)
14:32:41 → haritz joins (~hrtz@user/haritz)
14:34:24 → bontaq joins (~user@ool-45779c03.dyn.optonline.net)
14:42:37 × sayola quits (~sayola@ip-109-42-241-195.web.vodafone.de) (Read error: Connection reset by peer)
14:42:45 → sayola joins (~sayola@ip-109-42-243-149.web.vodafone.de)
14:50:52 → aryah joins (~aryah@141-138-38-218.dsl.iskon.hr)
14:53:47 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
14:58:47 × agent314 quits (~quassel@162.219.176.19) (Ping timeout: 264 seconds)
15:09:07 → d34df00d joins (~d34df00d@2600:1702:4f1b:7c10::43)
15:09:18 × mei quits (~mei@user/mei) (Remote host closed the connection)
15:11:44 → mei joins (~mei@user/mei)
15:15:09 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
15:15:35 → acidjnk_new joins (~acidjnk@p200300d6e714dc192d105e993ca958d7.dip0.t-ipconnect.de)
15:33:36 → ocra8 joins (ocra8@user/ocra8)
15:34:24 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds)
15:34:56 × ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:f77c:428b:229c:4616) (Remote host closed the connection)
15:35:16 → ubert joins (~Thunderbi@2a02:8109:ab8a:5a00:8905:bde4:99bc:a84f)
15:40:18 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
15:45:21 × sawilagar quits (~sawilagar@user/sawilagar) (Quit: Leaving)
15:52:36 → Midjak joins (~MarciZ@82.66.147.146)
15:54:51 × euleritian quits (~euleritia@dynamic-176-006-196-082.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
15:55:10 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
15:56:56 × machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 260 seconds)
16:03:16 × infinity0 quits (~infinity0@pwned.gg) (Remote host closed the connection)
16:05:23 → infinity0 joins (~infinity0@pwned.gg)
16:08:08 → y04nn joins (~username@2a03:1b20:8:f011::e10d)
16:08:10 → titibandit joins (~user@user/titibandit)
16:11:17 × CiaoSen quits (~Jura@2a05:5800:2b2:8e00:e6b9:7aff:fe80:3d03) (Ping timeout: 240 seconds)
16:16:47 × danse-nr3 quits (~danse-nr3@151.35.136.250) (Ping timeout: 264 seconds)
16:17:48 → danse-nr3 joins (~danse-nr3@151.43.113.96)
16:23:59 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
16:24:13 → euleritian joins (~euleritia@dynamic-176-006-196-082.176.6.pool.telefonica.de)
16:27:32 <c_wraith> abs and signum are the weird ones...
16:29:02 <int-e> just use abs x | x == 0 = 0 | otherwise = 1; signum x = x
16:29:39 <c_wraith> Like, the meaning of signum is utterly baffling for non-scalar numbers. You can make sure (x == abs x * signum x) is true, but why you'd ever use expect signum to mean anything for a non-scalar is an interesting question
16:32:32 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
16:35:40 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds)
16:36:47 <dolio> Generalizing to magnitude and direction doesn't seem that weird.
16:37:25 <dolio> Not sure about, like, matricies, though
16:39:17 × noctux quits (~noctux@user/noctux) (Ping timeout: 272 seconds)
16:39:19 × euleritian quits (~euleritia@dynamic-176-006-196-082.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
16:39:38 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
16:40:16 → noctux joins (~noctux@user/noctux)
16:43:26 <d34df00d> Got a fairly ill-posed question here, but anyway. I'm looking at the disassembly of ghc to see how certain constructs get optimized, and there's a lot of boilerplate apparently related to laziness even if I do -XStrict (which makes sense, since the arguments aren't necessarily strict at the invocation site).
16:43:31 <EvanR> matrices have a positive negative or zero determinant
16:43:51 <d34df00d> Is there any decent way to get rid of that boilerplate (or at least clearly separate it out)?
16:44:02 → manwithluck joins (manwithluc@gateway/vpn/protonvpn/manwithluck)
16:44:38 <lxsameer> hey folks, I'm looking for some reading material on how the haskell compiler is designed and its internal architecture. Any suggestion?
16:46:03 <kuribas> d34df00d: haskell assembly doesn't look like imperative assembly
16:46:52 <mauke> https://www.stephendiehl.com/posts/ghc_01.html ?
16:46:56 <kuribas> For example, all functions are called using continuation passing style.
16:47:33 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
16:48:18 <mauke> you could try writing code that passes unboxed values around explicitly
16:48:18 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
16:48:26 <mauke> not sure how helpful/workable that would be
16:49:07 <lxsameer> mauke: cheers
16:49:32 <kuribas> d34df00d: https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/generated-code
16:52:59 → Guest62 joins (~Guest54@1.240.117.251)
16:54:11 × ubert quits (~Thunderbi@2a02:8109:ab8a:5a00:8905:bde4:99bc:a84f) (Remote host closed the connection)
16:54:34 × yin quits (~yin@user/zero) (Quit: Lost terminal)
16:54:45 <lxsameer> thank you
16:56:07 × lxsameer quits (~lxsameer@Serene/lxsameer) (Quit: WeeChat 4.2.1)
16:58:17 <mauke> @let willHalt :: IO a -> IO Bool; willHalt = (True <$)
16:58:18 <lambdabot> Defined.
16:58:29 <mauke> > willHalt (pure ())
16:58:30 <lambdabot> <IO Bool>
16:59:37 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
17:00:23 <c_wraith> now.. willHaltUnsafely a = True <$ unsafeInterleaveIO a
17:01:57 × danse-nr3 quits (~danse-nr3@151.43.113.96) (Ping timeout: 255 seconds)
17:02:02 <EvanR> :t fix willHalt
17:02:04 <lambdabot> IO Bool
17:04:01 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
17:04:16 × mei quits (~mei@user/mei) (Remote host closed the connection)
17:05:06 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Ping timeout: 255 seconds)
17:05:21 <mauke> proof of correctness: 'willHalt x' will return True for all actions x that halt
17:05:31 <mauke> 'willHalt x' will never return True for any action x that doesn't halt
17:06:42 → mei joins (~mei@user/mei)
17:07:04 <EvanR> classically valid
17:08:01 <ncf> that's the statement not the proof
17:09:25 <EvanR> argument of correctness, ethos pathos logos
17:09:39 <mauke> I use an old technique called "proof by assertion"
17:10:09 <ncf> proof by intimidation
17:11:29 <systemfault> I bench press more so I'm right?
17:11:37 × chele quits (~chele@user/chele) (Remote host closed the connection)
17:12:15 <Rembane> Proof by flex!
17:12:20 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
17:12:53 × dtman34 quits (~dtman34@c-75-72-163-222.hsd1.mn.comcast.net) (Ping timeout: 240 seconds)
17:12:55 → euleritian joins (~euleritia@dynamic-176-006-196-082.176.6.pool.telefonica.de)
17:15:32 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
17:17:10 <EvanR> too real
17:18:15 × Guest62 quits (~Guest54@1.240.117.251) (Quit: Client closed)
17:18:39 × FragByte quits (~christian@user/fragbyte) (Quit: Quit)
17:19:46 × euleritian quits (~euleritia@dynamic-176-006-196-082.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
17:20:03 → euleritian joins (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
17:20:23 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
17:20:35 → FragByte joins (~christian@user/fragbyte)
17:20:41 → danse-nr3 joins (~danse-nr3@151.43.113.96)
17:23:38 <d34df00d> kuribas: I'm curious then how one might compare some common haskell constructs (think even pattern matching) to what happens in other, more imperative languages.
17:26:37 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
17:26:54 × ocra8 quits (ocra8@user/ocra8) (Quit: WeeChat 4.2.2)
17:27:09 <EvanR> the core language has a simplified version of pattern matching which can be implemented like the switch statement in C
17:27:39 <EvanR> the translation of haskell into core language is where the magic happens
17:31:30 <EvanR> looking at core output can give clues to the success of optimizing
17:32:06 × rdcdr quits (~rdcdr@user/rdcdr) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in)
17:32:18 <EvanR> or lack of success
17:32:47 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds)
17:33:42 → rdcdr joins (~rdcdr@user/rdcdr)
17:40:57 → jstolarek joins (~jstolarek@staticline-31-183-174-191.toya.net.pl)
17:43:21 → Guest86 joins (~Guest41@186.82.99.37)
17:43:48 ← Guest86 parts (~Guest41@186.82.99.37) ()
17:47:31 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
17:51:56 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds)
17:53:43 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
17:53:54 → lxsameer joins (~lxsameer@Serene/lxsameer)
17:54:26 <lxsameer> hey folks, what lib do you recommend for using sqlite? Supporting db migrations is a plus
18:01:38 <monochrom> I no longer distinguish continuation passing from call stack.
18:02:36 <EvanR> care to explain how they are the same
18:02:49 <dolio> The stack is the continuation.
18:02:54 <monochrom> If you see a "push <code address>", it can be narrated as "push return address", but it can just as well be narrated as "push address of continuation". Same difference.
18:03:50 → dtman34 joins (~dtman34@2601:447:d001:ed50:ebe5:b36d:357b:8a39)
18:03:53 <monochrom> And in the latter case, furthermore, "push" is narrated as "pass a parameter".
18:05:01 <EvanR> this calls for a closed cartesian comics on this subject
18:06:08 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
18:07:52 <monochrom> ghc-generated code looks different from gcc-generated code because of better reasons than this. Evaluation order. Heap system. Closures. How they decide to use registers.
18:11:01 → Guest86 joins (~Guest86@186.82.99.37)
18:11:16 <mauke> lxsameer: I like direct-sqlite. no built-in support for migrations, but pretty trivial to add IMHO. depends on what you expect from a migration feature
18:11:29 <monochrom> The fact that Haskell FFI works best if Haskell code leave OS-sanctioned stack alone (so C code can use it unconfused) so ghc-generated code uses another register and another memory area for Haskell stack.
18:12:33 <dolio> That's probably not the only reason.
18:13:26 × Guest86 quits (~Guest86@186.82.99.37) (Client Quit)
18:14:02 <monochrom> Ah yeah, then also N Haskell threads can have N distinct Haskell stacks too.
18:14:21 <monochrom> As a bonus, stack is also growable and movable.
18:14:25 <dolio> Yeah. Switching out OS stacks is bad news, I think.
18:16:02 → awnmp joins (~awnmp@user/awnmp)
18:16:02 × gentauro quits (~gentauro@user/gentauro) (Read error: Connection reset by peer)
18:16:25 <monochrom> OS stacks would be OK if there were a 1-1 mapping from Haskell threads to OS threads. OS threads already enjoy individual stacks. But of course we are more ambitious, we want our own cramming M Haskell threads into 1 OS thread.
18:17:19 <monochrom> It also turns out we want to liberally move Haskell threads to any OS thread at a whim.
18:17:59 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds)
18:18:20 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 260 seconds)
18:18:44 <dolio> Yeah, I guess. The problem is that you can't get away with having as many OS threads as people want Haskell threads.
18:19:21 <dolio> At least, last I heard.
18:20:01 <geekosaur> C/Gtk programmers have told me otherwise (thousands of threads)
18:20:32 <monochrom> We certainly recommend "don't bother writing your own select event loop, just fork more threads". So the RTS has to actually optimize for that. >:)
18:21:11 <lxsameer> mauke: cheers
18:21:43 <dolio> Are they actually using OS threads? I thought there was some other C thing that people used when they wanted that level of concurrency.
18:21:53 → gentauro joins (~gentauro@user/gentauro)
18:21:56 <monochrom> But lazy evaluation is the major difference. It also has the domino effect of causing many other differences e.g. how and why GHC does heap, closures, and GC in a way a C compiler doesn't.
18:21:57 <Rembane> The uv thing?
18:22:06 <dolio> Yeah, that sounds right.
18:23:44 <geekosaur> pthread_create. and libuv is an event loop, not a thread multiplexer
18:24:07 <geekosaur> Gtk provides its own event loop
18:35:03 → ft joins (~ft@p508db8fc.dip0.t-ipconnect.de)
18:35:38 <mauke> fibers, maybe
18:38:02 <mauke> last time I tried to benchmark thread systems (by creating an ever-growing bucket chain of threads in various systems/languages), C/pthreads maxed out at a couple hundred threads IIRC
18:38:25 <mauke> perl was under 100
18:39:04 <mauke> haskell got very slow, but still made visible progress at 300,000 threads
18:39:09 <[exa]> let's take a moment now to commemorate the magnificent glorious 1 globally interpreter-locked thread of python
18:39:42 <mauke> (mind, this was a 32-bit system with limited RAM)
18:40:41 → Guest86 joins (~Guest86@186.82.99.37)
18:41:02 <[exa]> dolio: btw the last time I read the RTS the total haskell IO-thread (_not_ OS thread) count was much more like memory-bounded than actually switch-starvation-bounded
18:41:24 <dolio> Yeah.
18:41:59 <dolio> There's an old ghc tracker ticker where Simon Marlow says he ran 1 million threads without a problem.
18:42:12 <dolio> Although I assume they weren't doing much.
18:42:38 → raehik joins (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net)
18:42:39 <[exa]> like, most threads in existence just wait for some resource to arrive anyway, right
18:43:28 → ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
18:50:01 × kuribas quits (~user@ptr-17d51encis8jg2ccf48.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
18:50:40 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
18:52:29 → yin joins (~yin@user/zero)
18:54:51 × mesaoptimizer quits (~mesaoptim@user/PapuaHardyNet) (Quit: mesaoptimizer)
18:55:05 → mesaoptimizer joins (~mesaoptim@user/PapuaHardyNet)
18:58:18 <EvanR> worker threads that can wait for work, furiously accomplish something and go back to sleep in ~0 time, vs the thread running the black hole merger simulation
19:08:59 × Guest86 quits (~Guest86@186.82.99.37) (Quit: Client closed)
19:17:23 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds)
19:17:58 × JimL quits (~quassel@89.162.16.26) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
19:17:59 × raehik quits (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 264 seconds)
19:18:20 → JimL joins (~quassel@89.162.16.26)
19:19:06 × mrmonday quits (~robert@what.i.hope.is.not.a.tabernaevagant.es) (Quit: .)
19:21:29 → mrmonday joins (~robert@what.i.hope.is.not.a.tabernaevagant.es)
19:21:51 tolt_ is now known as tolt
19:26:22 × causal quits (~eric@50.35.88.207) (Quit: WeeChat 4.1.1)
19:27:18 → justsomeguy joins (~justsomeg@user/justsomeguy)
19:27:30 × justsomeguy quits (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer)
19:33:32 → justsomeguy joins (~justsomeg@user/justsomeguy)
19:34:57 → y04nn joins (~username@2a03:1b20:8:f011::e10d)
19:34:57 × justsomeguy quits (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer)
19:34:59 × mei quits (~mei@user/mei) (Remote host closed the connection)
19:37:25 → mei joins (~mei@user/mei)
19:40:46 → justsomeguy joins (~justsomeg@user/justsomeguy)
19:40:48 × jstolarek quits (~jstolarek@staticline-31-183-174-191.toya.net.pl) (Quit: Lost terminal)
19:41:22 × justsomeguy quits (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer)
19:41:42 × aryah quits (~aryah@141-138-38-218.dsl.iskon.hr) (Read error: Connection reset by peer)
19:47:00 → justsomeguy joins (~justsomeg@user/justsomeguy)
19:47:00 × justsomeguy quits (~justsomeg@user/justsomeguy) (Read error: Connection reset by peer)
19:47:34 × y04nn quits (~username@2a03:1b20:8:f011::e10d) (Remote host closed the connection)
19:47:40 → aryah joins (~aryah@141-138-38-218.dsl.iskon.hr)
19:47:48 → y04nn joins (~username@2a03:1b20:8:f011::e10d)
19:49:49 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
19:52:42 → basicnpc joins (~asleep@user/basicnpc)
19:52:42 × basicnpc quits (~asleep@user/basicnpc) (Remote host closed the connection)
19:58:33 <lxsameer> is there any library to manage user configurations? for exmaple automatically map cli args to yaml keys and env vars?
20:01:31 → jmdaemon joins (~jmdaemon@user/jmdaemon)
20:03:39 → jcarpenter2 joins (~lol@2603:3016:1e01:b980:f1ac:fe7d:6abe:6f13)
20:04:57 <monochrom> I would think I would prefer mapping all of cli args, yaml keys, env vars to my internal algebaric data type, not among themselves, why would I need that.
20:05:23 <monochrom> At which point it is 3 libraries, one for each input format. But then all 3 already exist.
20:07:20 <lxsameer> monochrom: i'm looking for a way to let the user configure the app
20:12:19 → machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net)
20:14:56 → kayvank joins (~user@52-119-115-185.PUBLIC.monkeybrains.net)
20:15:56 × danse-nr3 quits (~danse-nr3@151.43.113.96) (Ping timeout: 260 seconds)
20:16:17 → zetef joins (~quassel@5.2.182.98)
20:20:30 × ec quits (~ec@gateway/tor-sasl/ec) (Ping timeout: 260 seconds)
20:20:57 × jinsun quits (~jinsun@user/jinsun) (Ping timeout: 272 seconds)
20:23:44 × awnmp quits (~awnmp@user/awnmp) (Quit: WeeChat 4.2.2)
20:28:10 → jinsun joins (~jinsun@user/jinsun)
20:30:17 × jinsun quits (~jinsun@user/jinsun) (Read error: Connection reset by peer)
20:36:52 × iteratee quits (~kyle@162.218.222.207) (Read error: Connection reset by peer)
20:37:07 → iteratee joins (~kyle@162.218.222.207)
20:40:04 <EvanR> app :: Config -> IO ()
20:47:48 × phma quits (phma@2001:5b0:210f:6338:6b26:1f57:9336:4cb3) (Read error: Connection reset by peer)
20:47:59 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds)
20:52:42 → phma joins (~phma@host-67-44-208-11.hnremote.net)
20:54:01 × xstill_ quits (xstill@fimu/xstill) (Quit: Ping timeout (120 seconds))
20:54:53 → xstill_ joins (xstill@fimu/xstill)
20:54:53 × mauke quits (~mauke@user/mauke) (Ping timeout: 268 seconds)
20:55:13 × migas97 quits (~migas@static.140.65.63.178.clients.your-server.de) (Quit: Ping timeout (120 seconds))
20:55:13 → mauke joins (~mauke@user/mauke)
20:55:30 → migas97 joins (~migas@static.140.65.63.178.clients.your-server.de)
20:56:08 × Dykam quits (Dykam@dykam.nl) (Remote host closed the connection)
20:57:18 → Dykam joins (Dykam@dykam.nl)
20:57:39 → philopsos1 joins (~caecilius@user/philopsos)
21:01:46 × philopsos1 quits (~caecilius@user/philopsos) (Client Quit)
21:02:08 × takuan quits (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 260 seconds)
21:04:24 → philopsos1 joins (~caecilius@user/philopsos)
21:05:20 × euleritian quits (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 256 seconds)
21:06:37 → pavonia joins (~user@user/siracusa)
21:11:00 × jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 260 seconds)
21:11:53 × zetef quits (~quassel@5.2.182.98) (Remote host closed the connection)
21:12:52 × hgolden quits (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Remote host closed the connection)
21:15:20 → hgolden joins (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9)
21:15:35 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds)
21:15:40 → lol_ joins (~lol@2603:3016:1e01:b980:557b:2881:fb5f:f7b0)
21:15:57 × jcarpenter2 quits (~lol@2603:3016:1e01:b980:f1ac:fe7d:6abe:6f13) (Read error: Connection reset by peer)
21:17:02 lol_ is now known as jcarpenter2
21:19:00 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
21:22:32 × motherfsck quits (~motherfsc@user/motherfsck) (Quit: quit)
21:24:17 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
21:24:48 → jmdaemon joins (~jmdaemon@user/jmdaemon)
21:27:58 × jcarpenter2 quits (~lol@2603:3016:1e01:b980:557b:2881:fb5f:f7b0) (Read error: Connection reset by peer)
21:28:05 → jcarpenter2 joins (~lol@2603:3016:1e01:b980:6c3b:ba23:fce8:e37c)
21:28:48 × michalz quits (~michalz@185.246.207.221) (Quit: ZNC 1.9.0 - https://znc.in)
21:35:12 → Square joins (~Square@user/square)
21:36:40 → emmanuelux joins (~emmanuelu@user/emmanuelux)
21:36:40 → lol_ joins (~lol@2603:3016:1e01:b9a0:a184:6ee0:68d5:cf53)
21:38:15 × Square2 quits (~Square4@user/square) (Ping timeout: 255 seconds)
21:40:11 × titibandit quits (~user@user/titibandit) (Ping timeout: 264 seconds)
21:40:45 × jcarpenter2 quits (~lol@2603:3016:1e01:b980:6c3b:ba23:fce8:e37c) (Ping timeout: 272 seconds)
21:41:59 × waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 264 seconds)
21:43:21 lol_ is now known as jcarpenter2
21:45:21 → waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
21:48:09 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
21:48:39 × mei quits (~mei@user/mei) (Remote host closed the connection)
21:49:35 → lol_ joins (~lol@2603:3016:1e01:b9a0:f567:9fc4:eb72:a51c)
21:51:05 → mei joins (~mei@user/mei)
21:53:17 × jcarpenter2 quits (~lol@2603:3016:1e01:b9a0:a184:6ee0:68d5:cf53) (Ping timeout: 240 seconds)
21:53:38 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
21:56:18 lol_ is now known as jcarpenter2
22:02:54 → Sgeo joins (~Sgeo@user/sgeo)
22:04:35 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
22:06:19 × __monty__ quits (~toonn@user/toonn) (Quit: leaving)
22:07:11 → sawilagar joins (~sawilagar@user/sawilagar)
22:08:29 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 240 seconds)
22:09:23 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
22:09:29 → Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915)
22:11:58 × sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937)
22:15:17 × talismanick quits (~user@2601:644:937c:ed10::ae5) (Remote host closed the connection)
22:15:30 → talismanick joins (~user@2601:644:937c:ed10::ae5)
22:18:08 × philopsos1 quits (~caecilius@user/philopsos) (Ping timeout: 252 seconds)
22:20:28 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
22:25:51 → dsrt^ joins (~cd@c-98-242-74-66.hsd1.ga.comcast.net)
22:29:06 × gmg quits (~user@user/gehmehgeh) (Quit: Leaving)
22:39:35 × Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving)
22:47:44 × destituion quits (~destituio@2a02:2121:607:127a:483a:846b:b497:f738) (Remote host closed the connection)
22:48:26 → destituion joins (~destituio@2a02:2121:607:127a:483a:846b:b497:f738)
22:50:10 × ezzieyguywuf quits (~Unknown@user/ezzieyguywuf) (Quit: Lost terminal)
22:52:40 × jmdaemon quits (~jmdaemon@user/jmdaemon) (Ping timeout: 268 seconds)
22:52:53 × troydm quits (~troydm@user/troydm) (Ping timeout: 240 seconds)
22:52:54 → ezzieyguywuf joins (~Unknown@user/ezzieyguywuf)
23:01:57 × mei quits (~mei@user/mei) (Remote host closed the connection)
23:03:33 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
23:03:37 → joeyadams joins (~joeyadams@2603:6010:5100:2ed:21cd:c9e2:b2de:eff)
23:04:23 → mei joins (~mei@user/mei)
23:13:20 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
23:14:37 → barak joins (~barak@2a0d:6fc2:68c1:7200:3cf2:a87d:a02b:3e21)
23:18:38 × destituion quits (~destituio@2a02:2121:607:127a:483a:846b:b497:f738) (Remote host closed the connection)
23:22:04 → tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
23:26:05 → destituion joins (~destituio@2a02:2121:607:127a:483a:846b:b497:f738)
23:27:34 → Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
23:32:04 × tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
23:35:06 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds)
23:37:46 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
23:40:09 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 268 seconds)
23:46:44 × kayvank quits (~user@52-119-115-185.PUBLIC.monkeybrains.net) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.3))
23:56:24 × acidjnk_new quits (~acidjnk@p200300d6e714dc192d105e993ca958d7.dip0.t-ipconnect.de) (Ping timeout: 255 seconds)

All times are in UTC on 2024-05-21.