Logs: liberachat/#haskell
| 2026-01-15 17:08:49 | <monochrom> | Oh, <=> is iff. |
| 2026-01-15 17:12:14 | → | euphores joins (~SASL_euph@user/euphores) |
| 2026-01-15 17:12:52 | <danza> | cheers monochrom |
| 2026-01-15 17:14:16 | × | danza quits (~danza@user/danza) (Remote host closed the connection) |
| 2026-01-15 17:22:05 | × | Lycurgus quits (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2026-01-15 17:23:37 | → | koz joins (~koz@121.99.240.58) |
| 2026-01-15 17:24:20 | × | larsivi quits (~larsivi@user/larsivi) (Quit: WeeChat 4.8.1) |
| 2026-01-15 17:34:09 | → | fp joins (~Thunderbi@89-27-10-140.bb.dnainternet.fi) |
| 2026-01-15 17:43:25 | × | kuribas quits (~user@2a02-1810-2825-6000-b6e0-77f4-472f-1183.ip6.access.telenet.be) (Remote host closed the connection) |
| 2026-01-15 17:47:10 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 17:48:06 | → | EvanR joins (~EvanR@user/evanr) |
| 2026-01-15 17:57:54 | <dolio> | I expect the "associativity" in the question is not about that associativity. It sounds like it's asking about the rules on how parentheses are automatically inserted. |
| 2026-01-15 17:58:05 | <dolio> | Not about whether how they're inserted matters. |
| 2026-01-15 18:00:24 | <dolio> | Even though (==) is associative as an operation on Bool, Haskell will refuse to accept `x == y == z`. |
| 2026-01-15 18:01:24 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2026-01-15 18:04:15 | <geekosaur> | that seems pretty obvious to me, since as defined either associativity makes the "other" one a comparison on `Bool` |
| 2026-01-15 18:08:01 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 18:13:16 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-15 18:20:52 | × | elarks quits (~elarks@user/yerrii) (Quit: WeeChat 4.7.1) |
| 2026-01-15 18:23:48 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 18:24:12 | × | ljdarj quits (~Thunderbi@user/ljdarj) (Quit: ljdarj) |
| 2026-01-15 18:25:48 | → | ljdarj joins (~Thunderbi@user/ljdarj) |
| 2026-01-15 18:30:23 | → | Hardyhardhard joins (~Hardyhard@user/hardyhardhard) |
| 2026-01-15 18:30:31 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 18:36:28 | × | Googulator quits (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-15 18:36:41 | → | Googulator joins (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-15 18:39:50 | → | Everything joins (~Everythin@172-232-54-192.ip.linodeusercontent.com) |
| 2026-01-15 18:41:50 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 18:46:49 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 18:48:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 18:53:25 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 19:04:14 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 19:09:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 19:11:52 | → | Tuplanolla joins (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) |
| 2026-01-15 19:12:25 | <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 19:13:02 | <dolio> | Yeah. |
| 2026-01-15 19:16:19 | <dolio> | The problem is that in situations with other types, the way parentheses are inserted affects whether it's well typed. |
| 2026-01-15 19:16:55 | <dolio> | And that's kind of a dumb thing to depend on. |
| 2026-01-15 19:17:32 | <__monty__> | tomsmeding: I'm not so sure, `False == False == True` doesn't seem very useful. |
| 2026-01-15 19:17:36 | <dolio> | Also the binary operator on booleans is pretty niche. |
| 2026-01-15 19:18:44 | <__monty__> | Are there any languages where a successful equality check "returns" the value, while an unsuccessful check returns False or something? |
| 2026-01-15 19:19:07 | <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 19:19:53 | <ncf> | (also, logical equivalence is not actually associative constructively, is it?) |
| 2026-01-15 19:20:12 | <dolio> | This isn't a relation. It's a decision procedure for a relation. |
| 2026-01-15 19:20:23 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 19:20:42 | <dolio> | The induced operator on booleans calculates parity. |
| 2026-01-15 19:22:37 | × | Hardyhardhard quits (~Hardyhard@user/hardyhardhard) (Quit: Client closed) |
| 2026-01-15 19:23:26 | <tomsmeding> | __monty__: sure :p |
| 2026-01-15 19:24:05 | × | jle` quits (~jle`@2603:8001:3b00:11::1156) (Ping timeout: 245 seconds) |
| 2026-01-15 19:24:57 | → | Hardyhardhard joins (~Hardyhard@user/hardyhardhard) |
| 2026-01-15 19:25:20 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-15 19:25:33 | <dolio> | Or wait, (/=) is parity. (==) is like anti-parity or something. |
| 2026-01-15 19:26:12 | <dolio> | Parity for the 0 bits instead of 1 bits. |
| 2026-01-15 19:26:52 | × | jreicher quits (~joelr@user/jreicher) (Quit: In transit) |
| 2026-01-15 19:29:33 | <__monty__> | Maybe the right type for (==) should be `Eq a => Maybe a -> Maybe a -> Maybe a`? Then we can get associativity. |
| 2026-01-15 19:32:11 | <monochrom> | A relation is a function. A function is an operator. So a relation is also an operator. >:) |
| 2026-01-15 19:33:03 | <monochrom> | We have a real type system, so we don't need artificial lines between relations, functions, numbers, values, constants. |
| 2026-01-15 19:38:01 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2026-01-15 19:39:00 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2026-01-15 19:39:20 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2026-01-15 19:44:16 | × | Hardyhardhard quits (~Hardyhard@user/hardyhardhard) (Quit: Client closed) |
| 2026-01-15 19:48:11 | <ncf> | have you heard of concepts with attitudes |
| 2026-01-15 19:48:28 | <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 19:49:08 | <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 19:49:15 | <ncf> | those are extremely different! |
| 2026-01-15 19:49:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 19:50:21 | × | bitdex_ quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-15 19:50:21 | <dolio> | ncf: Definitely seems like the associativity is not constructive. |
| 2026-01-15 19:50:27 | <ncf> | yeah i don't think it is |
| 2026-01-15 19:50:38 | <ncf> | can you prove a taboo from it? |
| 2026-01-15 19:54:18 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 19:59:04 | → | ttybitnik joins (~ttybitnik@user/wolper) |
| 2026-01-15 20:01:41 | <monochrom> | I have not heard of concepts with attitudes. But my thesis supervisor coined "continuing" for R in the 1990's. (E.g., https://www.cs.toronto.edu/~hehner/aPToP/aPToP.pdf last page.) We can do this by invoking "syntax sugar" on a per-operator basis. We don't need anything more profound or advanced. |
| 2026-01-15 20:04:00 | <ncf> | you say continuing operator i say relation |
| 2026-01-15 20:04:32 | <[exa]> | (binary relations are overrated) |
| 2026-01-15 20:05:12 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 20:06:32 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-15 20:06:46 | <[exa]> | anyway I saw this somewhere with matlabby dots, like (a <. b .< c), it even extended to (a <. b .<. c .< d) |
| 2026-01-15 20:06:48 | <monochrom> | The difference between yours and mine is that I say that a continuing operator is still an operator, just that it enjoys syntax sugar, whereas you say that it is not even an operator. |
| 2026-01-15 20:08:27 | <geekosaur> | Icon lets you do this chaining, but it's not using a mechanism Haskell could make use of (it's solidly based in its "failure" semantic) |
| 2026-01-15 20:10:19 | <dolio> | Haskell should just extend its rules so that lexing depends not only on parsing, but type checking. |
| 2026-01-15 20:10:20 | <[exa]> | btw Julia had a special case for that too: Meta.show_sexpr(:(a <= b < c)) == (:comparison, :a, :<=, :b, :<, :c) |
| 2026-01-15 20:10:31 | <[exa]> | dolio: <3 |
| 2026-01-15 20:11:40 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 20:11:47 | <monochrom> | Speaking of which, how is RecordDot done? |
| 2026-01-15 20:12:13 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 2026-01-15 20:13:16 | <ncf> | dolio: by yoneda this reduces to ((A ↔ B) ↔ A) ↔ B and the nontrivial direction is →, which is almost curry's paradox except with A ↔ B instead of A → B |
| 2026-01-15 20:13:24 | <dolio> | ncf: https://paste.tomsmeding.com/a6qxdKdh |
| 2026-01-15 20:13:29 | <ncf> | which is a conversation i remember having but don't remember the conclusion |
| 2026-01-15 20:13:38 | <ncf> | aha |
| 2026-01-15 20:14:07 | <ncf> | oh right, if you take A = ⊥ you get ¬¬B ↔ B |
| 2026-01-15 20:14:14 | <ncf> | cool |
| 2026-01-15 20:18:18 | <monochrom> | Oh nice, one more way to restore classical logic. :) |
| 2026-01-15 20:21:17 | <davean> | dolio: and end up like C++? Lol |
| 2026-01-15 20:21:20 | <monochrom> | (I had known of: choose one: EM, double-negation elim, Pierce.) |
| 2026-01-15 20:23:15 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 20:25:54 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 20:26:08 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 20:28:09 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 20:29:41 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
All times are in UTC.