2026/01/15

Newest at the top

2026-01-15 20:50:38 +0100 <ncf> can you prove a taboo from it?
2026-01-15 20:50:27 +0100 <ncf> yeah i don't think it is
2026-01-15 20:50:21 +0100 <dolio> ncf: Definitely seems like the associativity is not constructive.
2026-01-15 20:50:21 +0100bitdex_(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds)
2026-01-15 20:49:21 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-15 20:49:15 +0100 <ncf> those are extremely different!
2026-01-15 20:49:08 +0100 <ncf> the intended meaning of a O b O c when O is a (homogeneous, binary, associative) operator is a O (b O c)
2026-01-15 20:48:28 +0100 <ncf> the intended meaning of a R b R c when R is a relation is a R b ∧ b R c
2026-01-15 20:48:11 +0100 <ncf> have you heard of concepts with attitudes
2026-01-15 20:44:16 +0100Hardyhardhard(~Hardyhard@user/hardyhardhard) (Quit: Client closed)
2026-01-15 20:39:20 +0100Lord_of_Life_Lord_of_Life
2026-01-15 20:39:00 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds)
2026-01-15 20:38:01 +0100Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2026-01-15 20:33:03 +0100 <monochrom> We have a real type system, so we don't need artificial lines between relations, functions, numbers, values, constants.
2026-01-15 20:32:11 +0100 <monochrom> A relation is a function. A function is an operator. So a relation is also an operator. >:)
2026-01-15 20:29:33 +0100 <__monty__> Maybe the right type for (==) should be `Eq a => Maybe a -> Maybe a -> Maybe a`? Then we can get associativity.
2026-01-15 20:26:52 +0100jreicher(~joelr@user/jreicher) (Quit: In transit)
2026-01-15 20:26:12 +0100 <dolio> Parity for the 0 bits instead of 1 bits.
2026-01-15 20:25:33 +0100 <dolio> Or wait, (/=) is parity. (==) is like anti-parity or something.
2026-01-15 20:25:20 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2026-01-15 20:24:57 +0100Hardyhardhard(~Hardyhard@user/hardyhardhard) hardyhardhard
2026-01-15 20:24:05 +0100jle`(~jle`@2603:8001:3b00:11::1156) (Ping timeout: 245 seconds)
2026-01-15 20:23:26 +0100 <tomsmeding> __monty__: sure :p
2026-01-15 20:22:37 +0100Hardyhardhard(~Hardyhard@user/hardyhardhard) (Quit: Client closed)
2026-01-15 20:20:42 +0100 <dolio> The induced operator on booleans calculates parity.
2026-01-15 20:20:23 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-15 20:20:12 +0100 <dolio> This isn't a relation. It's a decision procedure for a relation.
2026-01-15 20:19:53 +0100 <ncf> (also, logical equivalence is not actually associative constructively, is it?)
2026-01-15 20:19:07 +0100 <ncf> equality is a relation, not an operator. asking whether a relation is associative is usually a type error, except in the case where the relation is on propositions (in this case decidable ones), but that doesn't mean it's a good idea to do it
2026-01-15 20:18:44 +0100 <__monty__> Are there any languages where a successful equality check "returns" the value, while an unsuccessful check returns False or something?
2026-01-15 20:17:36 +0100 <dolio> Also the binary operator on booleans is pretty niche.
2026-01-15 20:17:32 +0100 <__monty__> tomsmeding: I'm not so sure, `False == False == True` doesn't seem very useful.
2026-01-15 20:16:55 +0100 <dolio> And that's kind of a dumb thing to depend on.
2026-01-15 20:16:19 +0100 <dolio> The problem is that in situations with other types, the way parentheses are inserted affects whether it's well typed.
2026-01-15 20:13:02 +0100 <dolio> Yeah.
2026-01-15 20:12:25 +0100 <tomsmeding> I feel like the nonassociativity of the (==) operator in haskell is mostly because it is polymorphic. Had it been monomorphic for Bool, I'm sure it would have been made associative (in some direction)
2026-01-15 20:11:52 +0100Tuplanolla(~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) Tuplanolla
2026-01-15 20:09:19 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds)
2026-01-15 20:04:14 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-15 19:53:25 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-01-15 19:48:21 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-15 19:46:49 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds)
2026-01-15 19:41:50 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn
2026-01-15 19:39:50 +0100Everything(~Everythin@172-232-54-192.ip.linodeusercontent.com) Everything
2026-01-15 19:36:41 +0100Googulator(~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu)
2026-01-15 19:36:28 +0100Googulator(~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed)
2026-01-15 19:30:31 +0100merijn(~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2026-01-15 19:30:23 +0100Hardyhardhard(~Hardyhard@user/hardyhardhard) hardyhardhard
2026-01-15 19:25:48 +0100ljdarj(~Thunderbi@user/ljdarj) ljdarj
2026-01-15 19:24:12 +0100ljdarj(~Thunderbi@user/ljdarj) (Quit: ljdarj)