Newest at the top
| 2025-03-21 18:26:44 +0100 | wootehfoot | (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 2025-03-21 18:25:41 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2025-03-21 18:24:29 +0100 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2025-03-21 18:21:55 +0100 | euleritian | (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) |
| 2025-03-21 18:20:59 +0100 | euleritian | (~euleritia@95.90.214.149) (Ping timeout: 252 seconds) |
| 2025-03-21 18:17:25 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2025-03-21 18:16:52 +0100 | euleritian | (~euleritia@95.90.214.149) |
| 2025-03-21 18:16:30 +0100 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds) |
| 2025-03-21 18:12:31 +0100 | chiselfu1e | chiselfuse |
| 2025-03-21 18:11:36 +0100 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2025-03-21 18:11:33 +0100 | euleritian | (~euleritia@ip5f5ad695.dynamic.kabel-deutschland.de) |
| 2025-03-21 18:11:14 +0100 | euleritian | (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-03-21 18:10:09 +0100 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2025-03-21 17:57:27 +0100 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 268 seconds) |
| 2025-03-21 17:56:59 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 260 seconds) |
| 2025-03-21 17:56:34 +0100 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-03-21 17:52:42 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-21 17:50:19 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2025-03-21 17:49:50 +0100 | Square | (~Square@user/square) (Ping timeout: 252 seconds) |
| 2025-03-21 17:48:56 +0100 | vpan | (~vpan@212.117.1.172) (Quit: Leaving.) |
| 2025-03-21 17:45:23 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod |
| 2025-03-21 17:43:58 +0100 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2025-03-21 17:38:10 +0100 | <EvanR> | or homomorphism |
| 2025-03-21 17:37:58 +0100 | <EvanR> | sounds like a luxury to be able to pick a "real" equality relation so you can call other mappings congruence |
| 2025-03-21 17:36:42 +0100 | <haskellbridge> | <Bowuigi> That's usually called congruence I think |
| 2025-03-21 17:36:30 +0100 | <EvanR> | (automatically preserves equality, perhaps without using normal forms) |
| 2025-03-21 17:35:41 +0100 | <EvanR> | which we might take for granted and otherwise never had language for |
| 2025-03-21 17:35:25 +0100 | <EvanR> | or you could talk about, however you did it, any function you manage to define automatically preserves (a) notion of equality |
| 2025-03-21 17:34:03 +0100 | <haskellbridge> | <Bowuigi> Being able to ignore equality means that you can inspect the internal structure of something without that being in "normal form" |
| 2025-03-21 17:33:58 +0100 | <EvanR> | yes we have functions between types that might not agree with one or more notions of equality we have in mind on the domains |
| 2025-03-21 17:33:10 +0100 | <haskellbridge> | <Bowuigi> The concept of prefunction seems useful |
| 2025-03-21 17:32:20 +0100 | <EvanR> | either because there's no Eq instance or because more serious issues |
| 2025-03-21 17:31:49 +0100 | <EvanR> | also you could attempt to construe haskell's datatypes as presets because not all of them have a way to, at least decidably, know two values are equal |
| 2025-03-21 17:30:05 +0100 | <EvanR> | it was the 60s, so maybe they were tripping AF |
| 2025-03-21 17:29:23 +0100 | <EvanR> | something about foundations https://ncatlab.org/nlab/show/preset |
| 2025-03-21 17:28:33 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Client Quit) |
| 2025-03-21 17:27:37 +0100 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) lortabac |
| 2025-03-21 17:27:09 +0100 | euleritian | (~euleritia@dynamic-176-000-195-182.176.0.pool.telefonica.de) |
| 2025-03-21 17:26:29 +0100 | acidjnk | (~acidjnk@p200300d6e71c4f937555fc5a67c80b19.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-03-21 17:24:58 +0100 | <haskellbridge> | <Bowuigi> Quotients become central in proofs, that's nice |
| 2025-03-21 17:23:25 +0100 | notdabs | (~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) |
| 2025-03-21 17:23:06 +0100 | <haskellbridge> | <Bowuigi> How are those useful? I mean, order dependency is nice but do they make something more elegant? |
| 2025-03-21 17:23:03 +0100 | notdabs | (~Owner@2600:1700:69cf:9000:314f:c6fc:a776:72e4) (Remote host closed the connection) |
| 2025-03-21 17:11:20 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 252 seconds) |
| 2025-03-21 17:07:55 +0100 | Square | (~Square@user/square) Square |
| 2025-03-21 17:07:55 +0100 | euleritian | (~euleritia@dynamic-176-006-136-021.176.6.pool.telefonica.de) (Ping timeout: 244 seconds) |
| 2025-03-21 17:06:58 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-03-21 17:05:51 +0100 | <EvanR> | so x doesn't equal x because equal doesn't exist |
| 2025-03-21 17:04:57 +0100 | <EvanR> | (yet) |
| 2025-03-21 17:04:31 +0100 | <EvanR> | I actually veered off, the presets are "sets" without equality among the elements |