Newest at the top
| 2026-04-15 19:42:29 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-15 19:41:50 +0000 | pavonia | (~user@user/siracusa) siracusa |
| 2026-04-15 19:31:55 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-15 19:29:03 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 244 seconds) |
| 2026-04-15 19:28:24 +0000 | tromp | (~textual@2001:1c00:340e:2700:60c1:e0e:2c45:a3f6) |
| 2026-04-15 19:26:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-15 19:21:56 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 19:19:39 +0000 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 244 seconds) |
| 2026-04-15 19:18:57 +0000 | ouilemur | (~jgmerritt@user/ouilemur) ouilemur |
| 2026-04-15 19:17:05 +0000 | tromp | (~textual@2001:1c00:340e:2700:60c1:e0e:2c45:a3f6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-15 19:16:02 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-15 19:11:08 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-15 19:07:34 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 268 seconds) |
| 2026-04-15 19:07:32 +0000 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-04-15 19:03:17 +0000 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-04-15 18:59:55 +0000 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-04-15 18:59:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-15 18:59:15 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 18:58:31 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 264 seconds) |
| 2026-04-15 18:55:18 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-15 18:53:43 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 18:52:08 +0000 | arandombit | (~arandombi@user/arandombit) arandombit |
| 2026-04-15 18:44:15 +0000 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2026-04-15 18:44:12 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-04-15 18:41:23 +0000 | <monochrom> | Just like how both real math and ideal math exists and co-evolve, both real haskell and ideal haskell exists and co-evolve. |
| 2026-04-15 18:40:30 +0000 | <alter2000> | ok fair my bad, I meant "since it's in active use and development on concrete imperfect machines" |
| 2026-04-15 18:40:03 +0000 | Logio | (em@kapsi.fi) Logio |
| 2026-04-15 18:39:54 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-15 18:38:13 +0000 | uli-fem | (~uli-fem@203.87.114.209) (Ping timeout: 265 seconds) |
| 2026-04-15 18:37:24 +0000 | arandombit | (~arandombi@user/arandombit) (Remote host closed the connection) |
| 2026-04-15 18:36:54 +0000 | <EvanR> | nothing unreal exists:tm: |
| 2026-04-15 18:36:41 +0000 | <alter2000> | since it exists it's real no? |
| 2026-04-15 18:36:08 +0000 | <EvanR> | is haskell real math or ideal math |
| 2026-04-15 18:35:52 +0000 | <EvanR> | eventually non-standard interpretations and incompleteness would force another change in attitude, but this mentality seems interesting |
| 2026-04-15 18:34:17 +0000 | <EvanR> | it seems that an early (?) attitude of hilbert, continually faced with mathematical surprises while trying to carry out a formalist agenda, imagined a distinction between "real math" and "ideal math". Someone like cantor would report the discover of various infinities. It would be the formalists job to eventually account for this in the ideal formal version. Like their doing empirical science |
| 2026-04-15 18:33:28 +0000 | uli-fem | (~uli-fem@203.87.114.209) |
| 2026-04-15 18:28:34 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-15 18:27:37 +0000 | ft | (~ft@p508db287.dip0.t-ipconnect.de) ft |
| 2026-04-15 18:26:26 +0000 | <monochrom> | Recently I learned a bit of non-standard real analysis. We can just s/exotic/non-standard/. Wooo infinitestimals and extra bottoms and infinite lists... |
| 2026-04-15 18:24:08 +0000 | misterfish | (~misterfis@84.53.85.146) misterfish |
| 2026-04-15 18:23:50 +0000 | <EvanR> | all the proofs can go through formally and haskell is just an exotic model |
| 2026-04-15 18:21:51 +0000 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-04-15 18:21:40 +0000 | <monochrom> | I can imagine Bob Harper looking at all these annoyances and conclude "forget Haskell". :) |
| 2026-04-15 18:18:25 +0000 | Square2 | (~Square@user/square) Square |
| 2026-04-15 18:17:38 +0000 | Square2 | (~Square@user/square) (Remote host closed the connection) |
| 2026-04-15 18:16:04 +0000 | <monochrom> | Unfortunately Z has fewer bottoms than Either () Z too. Either Void Z should work, but it's a hack. |
| 2026-04-15 18:16:02 +0000 | Square2 | (~Square@user/square) Square |
| 2026-04-15 18:11:14 +0000 | <monochrom> | Err no, I have to re-think it. |
| 2026-04-15 18:11:09 +0000 | alter2000 | (~alter2000@user/alter2000) alter2000 |
| 2026-04-15 18:10:09 +0000 | <monochrom> | Whereas for less mind-boggling examples like "data Z = Z | S Z" you have the expected isomorphism again! So all is not lost. |