Logs: liberachat/#haskell
| 2026-04-15 18:24:08 | → | misterfish joins (~misterfis@84.53.85.146) |
| 2026-04-15 18:26:26 | <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:27:37 | → | ft joins (~ft@p508db287.dip0.t-ipconnect.de) |
| 2026-04-15 18:28:34 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-15 18:33:28 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 18:34:17 | <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:35:52 | <EvanR> | eventually non-standard interpretations and incompleteness would force another change in attitude, but this mentality seems interesting |
| 2026-04-15 18:36:08 | <EvanR> | is haskell real math or ideal math |
| 2026-04-15 18:36:41 | <alter2000> | since it exists it's real no? |
| 2026-04-15 18:36:54 | <EvanR> | nothing unreal exists:tm: |
| 2026-04-15 18:37:24 | × | arandombit quits (~arandombi@user/arandombit) (Remote host closed the connection) |
| 2026-04-15 18:38:13 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 265 seconds) |
| 2026-04-15 18:39:54 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 18:40:03 | → | Logio joins (em@kapsi.fi) |
| 2026-04-15 18:40:30 | <alter2000> | ok fair my bad, I meant "since it's in active use and development on concrete imperfect machines" |
| 2026-04-15 18:41:23 | <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:44:12 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-04-15 18:44:15 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2026-04-15 18:52:08 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-15 18:53:43 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 18:55:18 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 18:58:31 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 264 seconds) |
| 2026-04-15 18:59:15 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 18:59:54 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-04-15 18:59:55 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2026-04-15 19:03:17 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-04-15 19:07:32 | → | gmg joins (~user@user/gehmehgeh) |
| 2026-04-15 19:07:34 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 268 seconds) |
| 2026-04-15 19:11:08 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 19:16:02 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-15 19:17:05 | × | tromp quits (~textual@2001:1c00:340e:2700:60c1:e0e:2c45:a3f6) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2026-04-15 19:18:57 | → | ouilemur joins (~jgmerritt@user/ouilemur) |
| 2026-04-15 19:19:39 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 244 seconds) |
| 2026-04-15 19:21:56 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 19:26:54 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 19:28:24 | → | tromp joins (~textual@2001:1c00:340e:2700:60c1:e0e:2c45:a3f6) |
| 2026-04-15 19:29:03 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 244 seconds) |
| 2026-04-15 19:31:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds) |
| 2026-04-15 19:41:50 | → | pavonia joins (~user@user/siracusa) |
| 2026-04-15 19:42:29 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 19:47:23 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-04-15 19:48:52 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-04-15 19:49:47 | × | srazkvt quits (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2026-04-15 19:50:41 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Quit: Leaving) |
| 2026-04-15 19:51:44 | → | puke joins (~puke@user/puke) |
| 2026-04-15 19:52:12 | → | misterfish joins (~misterfis@84.53.85.146) |
| 2026-04-15 19:56:26 | → | Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915) |
| 2026-04-15 19:57:00 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 246 seconds) |
| 2026-04-15 19:58:17 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 19:59:18 | Lord_of_Life_ | is now known as Lord_of_Life |
| 2026-04-15 20:01:41 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 20:02:43 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 264 seconds) |
| 2026-04-15 20:05:32 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
| 2026-04-15 20:06:09 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 245 seconds) |
| 2026-04-15 20:06:45 | × | tusko quits (~uwu@user/tusko) (Quit: Lost terminal) |
| 2026-04-15 20:07:45 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 20:09:29 | × | arandombit quits (~arandombi@user/arandombit) (Remote host closed the connection) |
| 2026-04-15 20:12:02 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2026-04-15 20:13:09 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-15 20:13:34 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2026-04-15 20:17:44 | × | weary-traveler quits (~user@user/user363627) (Remote host closed the connection) |
| 2026-04-15 20:20:13 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 20:21:08 | × | jreicher quits (~joelr@user/jreicher) (Quit: In transit) |
| 2026-04-15 20:23:07 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 20:23:18 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 244 seconds) |
| 2026-04-15 20:27:20 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 244 seconds) |
| 2026-04-15 20:27:57 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-15 20:36:36 | × | alter2000 quits (~alter2000@user/alter2000) (Ping timeout: 255 seconds) |
| 2026-04-15 20:37:52 | × | jmcantrell_ quits (~weechat@user/jmcantrell) (Ping timeout: 276 seconds) |
| 2026-04-15 20:38:55 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 20:43:03 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 20:43:27 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-04-15 20:47:37 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 248 seconds) |
| 2026-04-15 20:50:17 | × | michalz quits (~michalz@185.246.207.203) (Remote host closed the connection) |
| 2026-04-15 20:54:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 20:55:47 | → | YuutaW joins (~YuutaW@infornography.yta.moe) |
| 2026-04-15 20:59:06 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-15 21:00:44 | → | alter2000 joins (~alter2000@user/alter2000) |
| 2026-04-15 21:05:09 | × | alter2000 quits (~alter2000@user/alter2000) (Ping timeout: 244 seconds) |
| 2026-04-15 21:07:41 | → | arandombit joins (~arandombi@2a02:2455:8656:7100:c853:ec6b:2699:b6f5) |
| 2026-04-15 21:07:41 | × | arandombit quits (~arandombi@2a02:2455:8656:7100:c853:ec6b:2699:b6f5) (Changing host) |
| 2026-04-15 21:07:41 | → | arandombit joins (~arandombi@user/arandombit) |
| 2026-04-15 21:08:25 | × | Square2 quits (~Square@user/square) (Ping timeout: 248 seconds) |
| 2026-04-15 21:09:40 | → | merijn joins (~merijn@62.45.136.136) |
| 2026-04-15 21:14:27 | × | merijn quits (~merijn@62.45.136.136) (Ping timeout: 244 seconds) |
| 2026-04-15 21:19:37 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 21:24:02 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 248 seconds) |
| 2026-04-15 21:25:26 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 21:26:19 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 268 seconds) |
| 2026-04-15 21:29:04 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-04-15 21:30:09 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 255 seconds) |
| 2026-04-15 21:39:30 | → | uli-fem joins (~uli-fem@203.87.114.209) |
| 2026-04-15 21:40:56 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-04-15 21:42:15 | <janus> | found an example of iso-recursive types with haskell-like syntax examples |
| 2026-04-15 21:42:19 | <janus> | https://github.com/solomon-b/lambda-calculus-hs/blob/main/main/09b-IsoInductiveTypes.hs |
| 2026-04-15 21:44:00 | <janus> | it probably isn't lazy but that's ok for now |
| 2026-04-15 21:44:06 | × | uli-fem quits (~uli-fem@203.87.114.209) (Ping timeout: 255 seconds) |
| 2026-04-15 21:44:18 | → | alter2000 joins (~alter2000@user/alter2000) |
| 2026-04-15 21:45:08 | × | arandombit quits (~arandombi@user/arandombit) (Ping timeout: 256 seconds) |
| 2026-04-15 21:47:54 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds) |
All times are in UTC.