Logs: liberachat/#haskell
| 2026-01-15 23:55:38 | <Inline> | the egotist set |
| 2026-01-15 23:55:43 | <Inline> | lol |
| 2026-01-15 23:55:43 | <EvanR> | jreicher, the original definition of Bitstream and SillyType both have nothing but infinite streams. Not really a double standard |
| 2026-01-15 23:55:51 | <jreicher> | I'm not insisting anything of the sort. I also don't think they're analogous. I'm just trying to understand why. |
| 2026-01-15 23:55:58 | <TMA> | jreicher: BUT there is just a single such string in the smallest model of the data SillyType = I SillyType theory |
| 2026-01-15 23:56:09 | <int-e> | Also has it really been 2 hours of this... |
| 2026-01-15 23:56:12 | <EvanR> | this is haskell an we have infinite lists |
| 2026-01-15 23:56:16 | × | ttybitnik quits (~ttybitnik@user/wolper) (Ping timeout: 256 seconds) |
| 2026-01-15 23:56:17 | <EvanR> | turns out |
| 2026-01-15 23:56:41 | <jreicher> | But not transfinite lists |
| 2026-01-15 23:56:59 | <EvanR> | they're not needed to make the original point, just as in cantor |
| 2026-01-15 23:57:21 | <jreicher> | No, I know. I'm just picking out where the line is. |
| 2026-01-15 23:57:24 | <EvanR> | though if you want to get into that there's more exotic constructions |
| 2026-01-15 23:58:57 | trickard_ | is now known as trickard |
| 2026-01-16 00:05:34 | × | trickard quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 00:05:48 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 00:08:50 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 00:10:48 | <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 00:11:37 | <EvanR> | all the ordinals is ... problematic but you can have a lot of them |
| 2026-01-16 00:12:16 | <jreicher> | Yeah it seems to me the "first few" would be straightforward |
| 2026-01-16 00:14:00 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-16 00:18:01 | × | k0zy quits (~user@user/k0zy) (Ping timeout: 264 seconds) |
| 2026-01-16 00:19:09 | <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 00:19:50 | <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 00:20:27 | <monochrom> | which is again just the counterintuitive "change '1' to '2' suddenly everything is different". |
| 2026-01-16 00:21:11 | <jreicher> | I certainly think it's interesting. It just doesn't seem to be something that should happen, but it does. |
| 2026-01-16 00:21:16 | <monochrom> | I mean, if a theorem is counterintuitive, then question the intuition not the theorem. |
| 2026-01-16 00:21:22 | <jreicher> | Yes |
| 2026-01-16 00:21:44 | <EvanR> | intuition can be adjusted to fit the facts :tm: |
| 2026-01-16 00:21:51 | <jreicher> | or question the definitions/axioms that result in the theorem. |
| 2026-01-16 00:22:26 | <EvanR> | that's like questioning the game of chess itself if you lose |
| 2026-01-16 00:22:39 | <EvanR> | better to play / define another game |
| 2026-01-16 00:22:42 | <int-e> | "Young man, in mathematics you don't understand things. You just get used to them." -- John von Neumann |
| 2026-01-16 00:22:47 | <jreicher> | More like questioning it if it's too easy or too hard to play. Or not fun. Something like that. |
| 2026-01-16 00:23:01 | <jreicher> | Then it arguably doesn't satisfy its goal |
| 2026-01-16 00:23:11 | → | DetourNe- joins (~DetourNet@user/DetourNetworkUK) |
| 2026-01-16 00:23:12 | <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 00:23:14 | <EvanR> | the game in which you lost nonetheless exists |
| 2026-01-16 00:23:16 | <EvanR> | and is valid |
| 2026-01-16 00:23:31 | × | DetourNetworkUK quits (DetourNetw@user/DetourNetworkUK) (Read error: Connection reset by peer) |
| 2026-01-16 00:23:40 | <int-e> | EvanR: Now that's different. Clearly chess was designed to make me lose! |
| 2026-01-16 00:23:51 | <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 00:23:59 | <EvanR> | I'm good |
| 2026-01-16 00:24:37 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 00:24:43 | <EvanR> | monochrom, the zero, infinity, ... rule |
| 2026-01-16 00:25:28 | DetourNe- | is now known as DetourNetworkUK |
| 2026-01-16 00:26:43 | <TMA> | monochrom: you can still have uncomputable subsets of unary strings though |
| 2026-01-16 00:26:53 | <monochrom> | "my car can do 0 to infinity in 60 seconds" >:) |
| 2026-01-16 00:27:25 | <monochrom> | TMA: Please don't go there :( >:) |
| 2026-01-16 00:29:18 | <TMA> | monochrom: good idea, I'll go to bed instead |
| 2026-01-16 00:29:26 | <monochrom> | haha |
| 2026-01-16 00:30:01 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 00:32:56 | × | Tuplanolla quits (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2026-01-16 00:40:25 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 00:45:23 | → | newmind joins (~newmind@91-133-90-252.dyn.cablelink.at) |
| 2026-01-16 00:45:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 00:46:07 | <geekosaur> | I really should start kicking those things into #haskell-in-depth |
| 2026-01-16 00:46:41 | <monochrom> | But I think we're done. :) |
| 2026-01-16 00:47:04 | <monochrom> | But OK! Kicking people into the deep end feels good haha. |
| 2026-01-16 00:48:19 | × | xff0x quits (~xff0x@2405:6580:b080:900:5f60:7a2f:94c6:623e) (Ping timeout: 244 seconds) |
| 2026-01-16 00:48:33 | <geekosaur> | yeh, I've only been peeking in occasionally since I'm busy this afternoon/evening |
| 2026-01-16 00:53:28 | <jreicher> | I didn't even know about that channel |
| 2026-01-16 00:54:29 | <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 00:54:52 | <dolio> | That can be a useful perspective. |
| 2026-01-16 00:56:09 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 00:57:28 | <dolio> | Not because there are 'really' uncomputable bit streams, but because a stream being uncomputable and you not knowing exactly how to compute it (because it doesn't come from some particular definition) act in sort of the same way. |
| 2026-01-16 00:58:41 | <dolio> | Like, you can model the bits coming in from your ethernet cable as an 'uncomputable' bit stream, because it is an external entity not subject to your computational model. But you can computably act on the stream. |
| 2026-01-16 01:01:26 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-16 01:01:55 | <dolio> | It can even be useful within a computing system. |
| 2026-01-16 01:02:51 | <dolio> | Like, `unsafeInterleaveIO` lets you access a bit stream that has no corresponding Haskell term. |
| 2026-01-16 01:06:59 | × | Zemy quits (~Zemy@72.178.108.235) (Read error: Connection reset by peer) |
| 2026-01-16 01:07:09 | → | Zemy joins (~Zemy@2600:100c:b0a0:7e6f:e8ca:c9ff:fea3:b5f7) |
| 2026-01-16 01:07:45 | → | Zemy_ joins (~Zemy@72.178.108.235) |
| 2026-01-16 01:09:44 | × | gmg quits (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-01-16 01:09:45 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-16 01:10:09 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 2026-01-16 01:10:25 | → | gmg joins (~user@user/gehmehgeh) |
| 2026-01-16 01:11:45 | × | Zemy quits (~Zemy@2600:100c:b0a0:7e6f:e8ca:c9ff:fea3:b5f7) (Ping timeout: 252 seconds) |
| 2026-01-16 01:11:56 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 01:16:31 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 01:24:42 | × | divlamir quits (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-01-16 01:25:05 | → | divlamir joins (~divlamir@user/divlamir) |
| 2026-01-16 01:27:43 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 01:32:08 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 01:39:13 | → | xff0x joins (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-01-16 01:43:04 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 01:50:01 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-16 01:52:19 | → | omidmash3 joins (~omidmash@user/omidmash) |
| 2026-01-16 01:53:56 | × | omidmash quits (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 2026-01-16 01:53:56 | omidmash3 | is now known as omidmash |
| 2026-01-16 01:57:51 | → | ryanbooker joins (uid4340@id-4340.hampstead.irccloud.com) |
| 2026-01-16 02:01:09 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 02:04:15 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Ping timeout: 240 seconds) |
| 2026-01-16 02:04:38 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 02:06:19 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 02:16:56 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-16 02:21:50 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 02:23:43 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-16 02:24:22 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 02:29:59 | × | haskellbridge quits (~hackager@96.28.224.214) (Remote host closed the connection) |
All times are in UTC.