Newest at the top
| 2026-01-15 21:26:08 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 21:25:54 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 21:23:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 21:21:20 +0100 | <monochrom> | (I had known of: choose one: EM, double-negation elim, Pierce.) |
| 2026-01-15 21:21:17 +0100 | <davean> | dolio: and end up like C++? Lol |
| 2026-01-15 21:18:18 +0100 | <monochrom> | Oh nice, one more way to restore classical logic. :) |
| 2026-01-15 21:14:14 +0100 | <ncf> | cool |
| 2026-01-15 21:14:07 +0100 | <ncf> | oh right, if you take A = ⊥ you get ¬¬B ↔ B |
| 2026-01-15 21:13:38 +0100 | <ncf> | aha |
| 2026-01-15 21:13:29 +0100 | <ncf> | which is a conversation i remember having but don't remember the conclusion |
| 2026-01-15 21:13:24 +0100 | <dolio> | ncf: https://paste.tomsmeding.com/a6qxdKdh |
| 2026-01-15 21:13:16 +0100 | <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 21:12:13 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-01-15 21:11:47 +0100 | <monochrom> | Speaking of which, how is RecordDot done? |
| 2026-01-15 21:11:40 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 21:10:31 +0100 | <[exa]> | dolio: <3 |
| 2026-01-15 21:10:20 +0100 | <[exa]> | btw Julia had a special case for that too: Meta.show_sexpr(:(a <= b < c)) == (:comparison, :a, :<=, :b, :<, :c) |
| 2026-01-15 21:10:19 +0100 | <dolio> | Haskell should just extend its rules so that lexing depends not only on parsing, but type checking. |
| 2026-01-15 21:08:27 +0100 | <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 21:06:48 +0100 | <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 21:06:46 +0100 | <[exa]> | anyway I saw this somewhere with matlabby dots, like (a <. b .< c), it even extended to (a <. b .<. c .< d) |
| 2026-01-15 21:06:32 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-15 21:05:12 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 21:04:32 +0100 | <[exa]> | (binary relations are overrated) |
| 2026-01-15 21:04:00 +0100 | <ncf> | you say continuing operator i say relation |
| 2026-01-15 21:01:41 +0100 | <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:59:04 +0100 | ttybitnik | (~ttybitnik@user/wolper) ttybitnik |
| 2026-01-15 20:54:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 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 +0100 | bitdex_ | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-15 20:49:21 +0100 | merijn | (~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 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) (Quit: Client closed) |
| 2026-01-15 20:39:20 +0100 | Lord_of_Life_ | Lord_of_Life |
| 2026-01-15 20:39:00 +0100 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2026-01-15 20:38:01 +0100 | Lord_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 +0100 | jreicher | (~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 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-15 20:24:57 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) hardyhardhard |
| 2026-01-15 20:24:05 +0100 | jle` | (~jle`@2603:8001:3b00:11::1156) (Ping timeout: 245 seconds) |