Newest at the top
| 2026-01-16 01:54:52 +0100 | <dolio> | That can be a useful perspective. |
| 2026-01-16 01:54:29 +0100 | <dolio> | Oh, maybe I should mention. You can set things up differently so that there are are uncomputable bit strings to talk about. And you can identify the computable bit strings as a subset, but is still uncountable. |
| 2026-01-16 01:53:28 +0100 | <jreicher> | I didn't even know about that channel |
| 2026-01-16 01:48:33 +0100 | <geekosaur> | yeh, I've only been peeking in occasionally since I'm busy this afternoon/evening |
| 2026-01-16 01:48:19 +0100 | xff0x | (~xff0x@2405:6580:b080:900:5f60:7a2f:94c6:623e) (Ping timeout: 244 seconds) |
| 2026-01-16 01:47:04 +0100 | <monochrom> | But OK! Kicking people into the deep end feels good haha. |
| 2026-01-16 01:46:41 +0100 | <monochrom> | But I think we're done. :) |
| 2026-01-16 01:46:07 +0100 | <geekosaur> | I really should start kicking those things into #haskell-in-depth |
| 2026-01-16 01:45:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 01:45:23 +0100 | newmind | (~newmind@91-133-90-252.dyn.cablelink.at) |
| 2026-01-16 01:40:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:32:56 +0100 | Tuplanolla | (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2026-01-16 01:30:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 01:29:26 +0100 | <monochrom> | haha |
| 2026-01-16 01:29:18 +0100 | <TMA> | monochrom: good idea, I'll go to bed instead |
| 2026-01-16 01:27:25 +0100 | <monochrom> | TMA: Please don't go there :( >:) |
| 2026-01-16 01:26:53 +0100 | <monochrom> | "my car can do 0 to infinity in 60 seconds" >:) |
| 2026-01-16 01:26:43 +0100 | <TMA> | monochrom: you can still have uncomputable subsets of unary strings though |
| 2026-01-16 01:25:28 +0100 | DetourNe- | DetourNetworkUK |
| 2026-01-16 01:24:43 +0100 | <EvanR> | monochrom, the zero, infinity, ... rule |
| 2026-01-16 01:24:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:23:59 +0100 | <EvanR> | I'm good |
| 2026-01-16 01:23:51 +0100 | <jreicher> | Umm, that's philosophical turf on which I'm very comfortable arguing, but that would be even more off-topic than we already have been. Can still go there if you want. |
| 2026-01-16 01:23:40 +0100 | <int-e> | EvanR: Now that's different. Clearly chess was designed to make me lose! |
| 2026-01-16 01:23:31 +0100 | DetourNetworkUK | (DetourNetw@user/DetourNetworkUK) (Read error: Connection reset by peer) |
| 2026-01-16 01:23:16 +0100 | <EvanR> | and is valid |
| 2026-01-16 01:23:14 +0100 | <EvanR> | the game in which you lost nonetheless exists |
| 2026-01-16 01:23:12 +0100 | <monochrom> | Shannon's definition of "information" implies that {0} has 0 bits of information, {0,1} has 1 bit of information. That is already a kind of "everything is different" if you look at the ratio: from 0 to 1 is an infinite percent increase. To a large extent the whole conversation above follows. |
| 2026-01-16 01:23:11 +0100 | DetourNe- | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 2026-01-16 01:23:01 +0100 | <jreicher> | Then it arguably doesn't satisfy its goal |
| 2026-01-16 01:22:47 +0100 | <jreicher> | More like questioning it if it's too easy or too hard to play. Or not fun. Something like that. |
| 2026-01-16 01:22:42 +0100 | <int-e> | "Young man, in mathematics you don't understand things. You just get used to them." -- John von Neumann |
| 2026-01-16 01:22:39 +0100 | <EvanR> | better to play / define another game |
| 2026-01-16 01:22:26 +0100 | <EvanR> | that's like questioning the game of chess itself if you lose |
| 2026-01-16 01:21:51 +0100 | <jreicher> | or question the definitions/axioms that result in the theorem. |
| 2026-01-16 01:21:44 +0100 | <EvanR> | intuition can be adjusted to fit the facts :tm: |
| 2026-01-16 01:21:22 +0100 | <jreicher> | Yes |
| 2026-01-16 01:21:16 +0100 | <monochrom> | I mean, if a theorem is counterintuitive, then question the intuition not the theorem. |
| 2026-01-16 01:21:11 +0100 | <jreicher> | I certainly think it's interesting. It just doesn't seem to be something that should happen, but it does. |
| 2026-01-16 01:20:27 +0100 | <monochrom> | which is again just the counterintuitive "change '1' to '2' suddenly everything is different". |
| 2026-01-16 01:19:50 +0100 | <monochrom> | EvanR: I would be the one that threw in uncomputable bit streams. But I am not being inconsistent; if possible I would threw in uncomputable unary streams too, except that it is impossible, no such thing exists. |
| 2026-01-16 01:19:09 +0100 | <EvanR> | I think agda makes this nicer by letting you define ordinals indexed by universe, then "useful programs using ordinals" (??) can then be universe polymorphic |
| 2026-01-16 01:18:01 +0100 | k0zy | (~user@user/k0zy) (Ping timeout: 264 seconds) |
| 2026-01-16 01:14:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-16 01:12:16 +0100 | <jreicher> | Yeah it seems to me the "first few" would be straightforward |
| 2026-01-16 01:11:37 +0100 | <EvanR> | all the ordinals is ... problematic but you can have a lot of them |
| 2026-01-16 01:10:48 +0100 | <jreicher> | Now you've got me wondering if it's possible to define a type that will allow construction of all the limit ordinals using infinite lists. |
| 2026-01-16 01:08:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:05:48 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 01:05:34 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |