Newest at the top
| 2025-12-05 11:06:26 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2025-12-05 10:52:31 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 264 seconds) |
| 2025-12-05 10:44:56 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2025-12-05 10:44:11 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2025-12-05 10:43:15 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2025-12-05 10:33:37 +0100 | trickard_ | trickard |
| 2025-12-05 10:32:36 +0100 | lambda_gibbon | (~lambda_gi@2603:7080:ee00:37d8:35d4:1aac:9a2f:cd11) (Ping timeout: 252 seconds) |
| 2025-12-05 10:29:45 +0100 | <ski> | since it is uniform in the dimensions, you only need to consider an arbitrary dimension, yes |
| 2025-12-05 10:28:58 +0100 | <lucabtz> | i suppose maybe it can be shown for 1D grids where there a are few cases and then handled inductively for all dimensions |
| 2025-12-05 10:28:35 +0100 | <ski> | you just have to handle all the cases |
| 2025-12-05 10:28:10 +0100 | lambda_gibbon | (~lambda_gi@2603:7080:ee00:37d8:35d4:1aac:9a2f:cd11) |
| 2025-12-05 10:23:12 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-05 10:23:01 +0100 | <lucabtz> | though honestly idk if it is so trivial to come up with an actual proof, maybe it is |
| 2025-12-05 10:22:24 +0100 | <lucabtz> | i dont see why associativity wouldnt be satified here because this is just about tiling up the grids to match the bigger grid, if the grids are all equal then associativity is a consequence of associativity of ., if some have dimension 1 it shouldn't matter when you tile them bigger |
| 2025-12-05 10:22:21 +0100 | <ski> | hm, yea, i think you're right (after pondering the conditions) |
| 2025-12-05 10:20:07 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2025-12-05 10:19:49 +0100 | <ski> | (yea .. in terms of `liftA2 (,) :: Applicative i => i a -> i b -> i (a,b)', we're asking whether this operation is associative, up to reassociating the `((a,b),c)' vs. `(a,(b,c))' in the result. it's just that we then have rexpressed this (not "on the nose") associative law in terms of its equivalent condition in terms of `(<*>)') |
| 2025-12-05 10:19:03 +0100 | <lucabtz> | i still think it is satified by broadcasting, for example say in order you have (w, 1) <*> (1, h) <*> (w, h), associating on the left you have (w, 1) <*> (1, h) = (w, h) and then (w, h) <*> (w, h) = (w, h), on the right (1, h) <*> (w, h) = (w, h) and then (w, 1) <*> (w, h) = (w, h) |
| 2025-12-05 10:17:38 +0100 | <ski> | anyway, the question is whether in `(M * N) * O' and `M * (N * O)', where `*' is some operation doing this kind of broadcasting, whether `M * N' and then `(M * N) * O' is well-defined is equivalent to `N * O' and then `M * (N * O)' being well-defined |
| 2025-12-05 10:16:53 +0100 | <lucabtz> | literal associativity of <*> makes no sense because the domains of the operator on the left and right are different |
| 2025-12-05 10:16:16 +0100 | <lucabtz> | it's not literal associativity of <*> but i get it makes sense to call is associativity |
| 2025-12-05 10:15:38 +0100 | <lucabtz> | it's okay i understood already from u <*> (v <*> w) = pure (.) <*> u <*> v <*> w |
| 2025-12-05 10:15:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-05 10:14:47 +0100 | <ski> | liftA2 (uncurry . f) ia (liftA2 (,) ib ic) = liftA2 (uncurry f) (liftA2 (,) ia ib) ic -- or, with an arbitrary function `f', rather than triples |
| 2025-12-05 10:13:16 +0100 | <lucabtz> | yeah i get what you mean |
| 2025-12-05 10:13:05 +0100 | <ski> | liftA2 (\a (b,c) -> (a,b,c)) ia (liftA2 (,) ib ic) = liftA2 (\(a,b) c -> (a,b,c)) (liftA2 (,) ia ib) ic -- same law, in terms of `liftA2', and tuples, might make the name "associativity" more reasonable |
| 2025-12-05 10:12:43 +0100 | <ski> | (do note that `pure (.) <*> u <*> v <*> w' means `((pure (.) <*> u) <*> v) <*> w', so that that side is left-associated) |
| 2025-12-05 10:10:50 +0100 | <lucabtz> | if you mean that it does satisfy it i believe, the constraint becomes for each width and height that all the ones that are not equal to each other are 1 |
| 2025-12-05 10:09:33 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Remote host closed the connection) |
| 2025-12-05 10:09:00 +0100 | chele | (~chele@user/chele) chele |
| 2025-12-05 10:08:40 +0100 | <ski> | that law is a kind of associativity law |
| 2025-12-05 10:08:28 +0100 | <ski> | u <*> (v <*> w) = pure (.) <*> u <*> v <*> w -- <https://wiki.haskell.org/Typeclassopedia#Laws_2> |
| 2025-12-05 10:08:25 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-12-05 10:03:21 +0100 | bggd | (~bgg@2a01:e0a:fd5:f510:b178:c96:453a:4d0f) |
| 2025-12-05 10:03:12 +0100 | fp | (~Thunderbi@130.233.70.22) fp |
| 2025-12-05 10:03:03 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-05 10:01:33 +0100 | trickard_ | (~trickard@cpe-85-98-47-163.wireline.com.au) |
| 2025-12-05 10:01:19 +0100 | trickard | (~trickard@cpe-85-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2025-12-05 09:57:45 +0100 | acidjnk | (~acidjnk@p200300d6e7171916e981ce74d2c64e2e.dip0.t-ipconnect.de) acidjnk |
| 2025-12-05 09:55:39 +0100 | <lucabtz> | though i agree it would make more sense to keep it a separate function |
| 2025-12-05 09:55:18 +0100 | <lucabtz> | <*> is not associative |
| 2025-12-05 09:55:06 +0100 | <lucabtz> | im a bit confused by what associative law you are speaking about |
| 2025-12-05 09:54:32 +0100 | peterbecich | (~Thunderbi@172.222.148.214) (Ping timeout: 244 seconds) |
| 2025-12-05 09:53:55 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-12-05 09:52:46 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-12-05 09:49:21 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-12-05 09:45:49 +0100 | <ski> | (i don't much like this kind of implicit broadcasting) |
| 2025-12-05 09:45:16 +0100 | <ski> | btw, i'd probably just define a separate function |
| 2025-12-05 09:44:39 +0100 | <ski> | it'd be annoying, if rewriting a total use, with one of the laws, would give a partial use |
| 2025-12-05 09:43:44 +0100 | <ski> | (and similarly for the other laws) |