Newest at the top
| 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) |
| 2025-12-05 09:42:56 +0100 | lambda_gibbon | (~lambda_gi@2603:7080:ee00:37d8:35d4:1aac:9a2f:cd11) (Ping timeout: 256 seconds) |
| 2025-12-05 09:42:24 +0100 | <ski> | if you take assocative law, such that all applications on one side satisfies this condition, do the ones on the other side also satisfy it ? |
| 2025-12-05 09:41:05 +0100 | <lucabtz> | yep |
| 2025-12-05 09:40:49 +0100 | <ski> | (m0 == m1 || any (1 ==) [m0,m1]) && (n0 == n1 || any (1 ==) [n0,n1]) -- ? |
| 2025-12-05 09:40:41 +0100 | <lucabtz> | *instead of equality to 1 |
| 2025-12-05 09:40:28 +0100 | <lucabtz> | technically i suppose you could weaken the constraint with divisibility instead of 1, but it is not like that in numpy |
| 2025-12-05 09:39:53 +0100 | <lucabtz> | if you have say (w, 1) (w, h) the result is (w, h) and the first one is broadcasted to (w, h) by repeating the row h times over the columns |
| 2025-12-05 09:39:07 +0100 | <lucabtz> | either widths are equal or some are 1 and same for height |
| 2025-12-05 09:39:01 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2025-12-05 09:38:20 +0100 | lambda_gibbon | (~lambda_gi@2603:7080:ee00:37d8:35d4:1aac:9a2f:cd11) |