| 2026-01-16 00:00:48 +0100 | <geekosaur> | right, I was abbreviating "countably finite", thought that would be fairly obvious from the ongoing context |
| 2026-01-16 00:00:53 +0100 | <geekosaur> | *infinite |
| 2026-01-16 00:01:02 +0100 | <geekosaur> | damn, fingers ahead of brain again |
| 2026-01-16 00:01:58 +0100 | <monochrom> | Me is even finger-disobeys-brain. (How else do you think I mistyped "you" for "mean"?! :) ) |
| 2026-01-16 00:02:17 +0100 | <dolio> | Presumably the prefix code is going to be set up so that there's a unique prefix for each binary expansion. |
| 2026-01-16 00:02:27 +0100 | <dolio> | Hopefully each real number. |
| 2026-01-16 00:03:12 +0100 | <dolio> | So even though the expansions are infinitely long, you only need to look at a finite portion. |
| 2026-01-16 00:03:13 +0100 | <EvanR> | jreicher, classic article in the earth days of modern math, "does every real number have a decimal expansion" |
| 2026-01-16 00:03:16 +0100 | <EvanR> | early* |
| 2026-01-16 00:03:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 00:04:07 +0100 | <EvanR> | this was before classical math "won" and "asserted" "yes" xD |
| 2026-01-16 00:04:27 +0100 | <EvanR> | no one will drive us out of the paradise cantor created for us |
| 2026-01-16 00:04:34 +0100 | <jreicher> | EvanR: OK.... Not sure what the point is? (And FYI I don't think classical math has won, but that's a debate for another day/channel) |
| 2026-01-16 00:04:51 +0100 | <EvanR> | around 1940s debate of this sort died out |
| 2026-01-16 00:05:01 +0100 | <EvanR> | resurrected way later |
| 2026-01-16 00:05:17 +0100 | <EvanR> | but hopefully now we can just state our systems and assumptions ahead of time and not debate vibes |
| 2026-01-16 00:05:41 +0100 | <EvanR> | jreicher, the point of the paper? well that's in the paper, and relevant to the above story about chaitin's number |
| 2026-01-16 00:05:41 +0100 | <monochrom> | Leibniz would have loved that. |
| 2026-01-16 00:06:03 +0100 | <jreicher> | EvanR: no, not the point of the paper, the point you are wanting to make by providing the paper |
| 2026-01-16 00:06:38 +0100 | <EvanR> | remarks about about the "construction" hinging on obtaining a digital expansion of any real number |
| 2026-01-16 00:06:49 +0100 | <TMA> | mapping digit sequences of countably infinite lenght to real numbers is a classic way to show that {0,1}^* (or {0..9}^*) is not countable set |
| 2026-01-16 00:07:22 +0100 | <EvanR> | we just did that |
| 2026-01-16 00:07:24 +0100 | <EvanR> | xD |
| 2026-01-16 00:07:32 +0100 | <EvanR> | except skipping the reals |
| 2026-01-16 00:07:38 +0100 | <jreicher> | EvanR: you mean the construction of diagonalisation? |
| 2026-01-16 00:07:42 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-16 00:07:57 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-16 00:08:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.54) (Read error: Connection reset by peer) |
| 2026-01-16 00:08:48 +0100 | AlexNoo | (~AlexNoo@5.139.232.54) |
| 2026-01-16 00:10:17 +0100 | <jreicher> | (Because you don't need every real number to have a decimal/binary expansion for that construction) |
| 2026-01-16 00:11:48 +0100 | <EvanR> | you don't even need reals for that, since it's demonstrating uncountability of *something*, in this case just streams of bits |
| 2026-01-16 00:12:08 +0100 | <jreicher> | Yes, which is why I wasn't entirely understanding why you provided that paper |
| 2026-01-16 00:12:19 +0100 | <EvanR> | you brought up chaitin |
| 2026-01-16 00:12:26 +0100 | <EvanR> | that was being discussed |
| 2026-01-16 00:12:35 +0100 | <EvanR> | that's specifically about reals |
| 2026-01-16 00:13:49 +0100 | <EvanR> | if you keep getting confused thinking stream of bits means "oh reals", and reals means "oh, just a binary expansion", then that equivocation is the point of this old paper |
| 2026-01-16 00:14:20 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 00:14:22 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 00:14:36 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 00:14:38 +0100 | <EvanR> | if you didn't guess already the argument in the paper is answering "no" to its title... like betteridge's law |
| 2026-01-16 00:15:08 +0100 | <dolio> | Yeah, like I said, there's a paper about a topos where the reals are countable. But the diagonal argument holds in every topos. |
| 2026-01-16 00:15:12 +0100 | <jreicher> | I'm not confused about that. Every bitstream can be interpreted as a numeral corresponding to a number. But that says nothing about the converse, especially since nothing stops you from throwing in all kinds of exotic objects to the set you want to call "the reals" |
| 2026-01-16 00:15:39 +0100 | Googulator69 | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-16 00:15:43 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-16 00:15:43 +0100 | <dolio> | So you can't assume that real numbers are the same things as expansions. |
| 2026-01-16 00:15:49 +0100 | <jreicher> | I never have |
| 2026-01-16 00:17:34 +0100 | <EvanR> | I don't doubt you can throw exotic objects in |
| 2026-01-16 00:17:49 +0100 | <EvanR> | but it would seem kind of odd that these objects don't "sit" somewhere on the real line xD |
| 2026-01-16 00:18:11 +0100 | <EvanR> | at least approximately |
| 2026-01-16 00:18:19 +0100 | <jreicher> | yes of course. :) |
| 2026-01-16 00:19:04 +0100 | <jreicher> | I'm pretty sure non-standard analysis does this with asserting the existence of infinitisimals |
| 2026-01-16 00:19:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-16 00:19:08 +0100 | <EvanR> | if were doing vibes, this kind of defeats the point of the real line, and the idea of quantity or ordering |
| 2026-01-16 00:19:21 +0100 | <EvanR> | well you know where infinitesimals are |
| 2026-01-16 00:19:26 +0100 | <EvanR> | at least approximately |
| 2026-01-16 00:19:29 +0100 | <jreicher> | I'm really not doing vibes, so I don't know why you keep saying that |
| 2026-01-16 00:19:40 +0100 | <EvanR> | I'm doing vibes there |
| 2026-01-16 00:19:43 +0100 | <int-e> | EvanR: "real number" is a misnomer :P |
| 2026-01-16 00:19:48 +0100 | <EvanR> | lol |
| 2026-01-16 00:20:04 +0100 | <jreicher> | Fictionalists unite |
| 2026-01-16 00:20:08 +0100 | <monochrom> | My beef is that "imaginary number" is a misnomer. But I digress. |
| 2026-01-16 00:20:22 +0100 | <EvanR> | imaginary numbers are real and real numbers are fictional |
| 2026-01-16 00:25:35 +0100 | <jreicher> | I still don't understand why anyone would say SillyType is countable but BitStream is uncountable. |
| 2026-01-16 00:25:59 +0100 | <jreicher> | Surely they're either both countable, or both uncountable, depending on your "definitions" |
| 2026-01-16 00:26:11 +0100 | <monochrom> | I can prove them, but if you're asking for intuition, I think I don't have any. |
| 2026-01-16 00:26:25 +0100 | <jreicher> | No, prove away, please. I'd like to understand. |
| 2026-01-16 00:26:51 +0100 | <jreicher> | Every proof I sketch out results in an inconsistency. |
| 2026-01-16 00:27:29 +0100 | <monochrom> | I map 0 to the infinite stream z = I z, 1 to bottom, 2 to I bottom, 3 to I (I bottom), etc. |
| 2026-01-16 00:28:51 +0100 | <jreicher> | And so SillyType is countable, yes? |
| 2026-01-16 00:29:36 +0100 | <monochrom> | But intuitively I'm not surprised. Expressing natural numbers in unary requires n units of memory for n; "merely" switching to binary, that drops down to lg n. |
| 2026-01-16 00:29:37 +0100 | <int-e> | Sure. It's morally finite ("morally" being the view where you don't have bottoms) |
| 2026-01-16 00:29:43 +0100 | k0zy | (~user@75-164-179-179.ptld.qwest.net) |
| 2026-01-16 00:29:51 +0100 | k0zy | (~user@75-164-179-179.ptld.qwest.net) (Changing host) |
| 2026-01-16 00:29:51 +0100 | k0zy | (~user@user/k0zy) k0zy |
| 2026-01-16 00:29:56 +0100 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2026-01-16 00:30:04 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 00:30:22 +0100 | <monochrom> | Generally there are multiple instance when switching from 1 to 2, or 2 to 3, or 3 to 4 makes breaking changes. |
| 2026-01-16 00:30:35 +0100 | <jreicher> | monochrom: hang on, are you now saying bitstream is countable? I was hoping that, having proved SillyType is countable, you'd now prove bitstream is uncountable. |
| 2026-01-16 00:30:51 +0100 | <int-e> | jreicher: NO! |
| 2026-01-16 00:30:54 +0100 | <monochrom> | SillyType is countable, BitStream is uncountable. |
| 2026-01-16 00:31:10 +0100 | <int-e> | bitstream adds additional observations for each natural number. |
| 2026-01-16 00:31:21 +0100 | <monochrom> | 2-colourability is polynomial-time, 3-colourability is NP-complete. |
| 2026-01-16 00:31:29 +0100 | <int-e> | 1^N has cardinality 1; 2^N or 3^N is uncountable. |
| 2026-01-16 00:31:40 +0100 | <jreicher> | monochrom: what's your preferred proof that bitstream is uncountable? I'm looking for what it uses that SillyType isn't entitled to |
| 2026-01-16 00:32:08 +0100 | <monochrom> | BitStream has more than infinite bit strings. |
| 2026-01-16 00:32:25 +0100 | <monochrom> | (so use Cantor diagonlization again) |
| 2026-01-16 00:32:49 +0100 | <jreicher> | monochrom: am I allowed to say SillyType has more the infinite unary strings? |
| 2026-01-16 00:32:53 +0100 | <monochrom> | (You can also attempt diagonalization on SillyType and get stuck.) |
| 2026-01-16 00:33:13 +0100 | <monochrom> | Sure. That's doesn't get you anywhere per se. |
| 2026-01-16 00:33:41 +0100 | <monochrom> | For BitStream I'm using: if a subset is uncountable, then a superset is also uncountable. |
| 2026-01-16 00:33:55 +0100 | <monochrom> | so "more than" is helpful for me. |
| 2026-01-16 00:34:23 +0100 | <EvanR> | there's other fun stuff like subcountable |
| 2026-01-16 00:35:03 +0100 | <EvanR> | and subfinite |
| 2026-01-16 00:35:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 00:35:31 +0100 | <int-e> | jreicher: Anyway, at an intuitive level, SillyType has no bits that you could flip to make Cantor's diagonal argument work. |
| 2026-01-16 00:35:52 +0100 | <int-e> | So it's nothing like a bit stream. |
| 2026-01-16 00:36:27 +0100 | <jreicher> | OK, but depending on what we allow for BitStream, can't I be allowed to construct all the aleph numbers from SillyType? That would make it uncountable i think |
| 2026-01-16 00:37:03 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 00:37:17 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 00:37:24 +0100 | <int-e> | you're also stepping beyond what's useful for modelling program semantics |
| 2026-01-16 00:37:25 +0100 | <EvanR> | there's like 1 possible value of SillyType |
| 2026-01-16 00:37:38 +0100 | <EvanR> | if this is uncountable then, I'll eat my hat |
| 2026-01-16 00:37:54 +0100 | <jreicher> | int-e: which is why I queried the use of an "infinitely running program" to begin with. It's an interesting dividing line. |
| 2026-01-16 00:38:07 +0100 | <EvanR> | you're not asking about the number of 1s in the stream |
| 2026-01-16 00:38:12 +0100 | <EvanR> | it's about the number of possible streams |
| 2026-01-16 00:38:22 +0100 | <EvanR> | (like 1) |
| 2026-01-16 00:38:43 +0100 | <int-e> | like, sure, you can pretend that there is an element of SillyType for every ordinal number. Or that there's some other unobservable feature that makes the values more plentiful. There's no purpose to it though, since none of this will be observable. |
| 2026-01-16 00:39:02 +0100 | <jreicher> | ...just like infinitely running programs are not observable |
| 2026-01-16 00:39:08 +0100 | <EvanR> | are you sure? |
| 2026-01-16 00:39:12 +0100 | <jreicher> | (I'm just arguing devil's advocate now) |
| 2026-01-16 00:39:17 +0100 | <int-e> | No it's not the same. |
| 2026-01-16 00:39:34 +0100 | <Leary> | jreicher: SillyType caps out at omega since you can only "add 1" on the left to get 1 + omega = omega; there's no omega + 1. |
| 2026-01-16 00:39:57 +0100 | <jreicher> | I know. That's kind of what I mean by "fine line". We seem to be saying we've got "observable", "unobservable", and then something like "observable in principle" (conceivable?) |
| 2026-01-16 00:40:09 +0100 | <int-e> | omega arises naturally as the least upper bound of all natural numbers, corresponding to having computations of arbitrary length |
| 2026-01-16 00:40:20 +0100 | <int-e> | nothing beyond omega arises in this fashion |
| 2026-01-16 00:40:24 +0100 | <EvanR> | that's the point of semantics to define what the values (what the programs mean) |
| 2026-01-16 00:40:40 +0100 | <EvanR> | if you're counting values, you're not counting programs, unless that's the semantics you're using |
| 2026-01-16 00:40:45 +0100 | <EvanR> | or counting runtime behaviors |
| 2026-01-16 00:40:52 +0100 | <jreicher> | Leary: but then why wouldn't we say BitStream caps out at computable streams? (I know it's not the same) |
| 2026-01-16 00:41:17 +0100 | <EvanR> | I missed how we're distinguishing any values of SillyType beyond the obvious 1 |
| 2026-01-16 00:42:46 +0100 | <int-e> | EvanR: "we" apparently allow bottoms |
| 2026-01-16 00:43:44 +0100 | <TMA> | ackshually, if we take SillyType as constructed then there is one value in it. if we take the definition as an axiom in a theory, there might exists a nonstandard model, in which there are more members of the SillyType |
| 2026-01-16 00:44:29 +0100 | <EvanR> | so like, bottom, 1 bottom, 1 (1 bottom) etc are all consistent |
| 2026-01-16 00:44:37 +0100 | <EvanR> | so maybe they all count as 1 |
| 2026-01-16 00:44:53 +0100 | <jreicher> | Would you prefer data SillyType = I | I SillyType? |
| 2026-01-16 00:45:06 +0100 | <EvanR> | that would allow finite strings |
| 2026-01-16 00:45:11 +0100 | <int-e> | TMA: You're disallowing bottoms so what you said is not true since we can show coinductively that for all a, b in SillyType, a = b. |
| 2026-01-16 00:45:28 +0100 | <int-e> | IOW, there can't be any distinct non-standard element of that type. |
| 2026-01-16 00:45:51 +0100 | <EvanR> | now you have many distinguishable SillyType strings |
| 2026-01-16 00:45:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 00:46:04 +0100 | <jreicher> | But still countable? |
| 2026-01-16 00:46:11 +0100 | <EvanR> | looks like yes |
| 2026-01-16 00:46:30 +0100 | <int-e> | Yes, that's still countable. |
| 2026-01-16 00:46:34 +0100 | <EvanR> | exercise write the function from Nat to SillyType which witnesses it |
| 2026-01-16 00:46:40 +0100 | Inline | (~User@2001-4dd6-dd24-0-f7db-3cda-3b52-1dd2.ipv6dyn.netcologne.de) Inline |
| 2026-01-16 00:46:51 +0100 | <TMA> | so the sequence of ω⁺Is could also be in SillyType |
| 2026-01-16 00:46:51 +0100 | <int-e> | (It's an infinite type though so adding non-standard elements will generally work.) |
| 2026-01-16 00:46:56 +0100 | <jreicher> | OK. So I'm still curious why we think it's OK to throw in bitstreams that can't be computed, but we can't throw in sillytype strings that can't be computed |
| 2026-01-16 00:47:00 +0100 | <jreicher> | TMA: exactly |
| 2026-01-16 00:47:15 +0100 | <EvanR> | nobody threw in bitstreams that can't be computed that was iterated like 3 times |
| 2026-01-16 00:47:28 +0100 | <EvanR> | (though I tried to once but everyone ignored me) |
| 2026-01-16 00:47:30 +0100 | int-e | loves moving goalposts btw. Not. |
| 2026-01-16 00:48:16 +0100 | <Leary> | jreicher: You can say that if you want to, but as has already been pointed out, you're "crossing the streams" of two settings. You can model BitStream in either a constructive or a classical setting, but it's uncountable in both /because the notion of countability also depends on the setting/. |
| 2026-01-16 00:48:36 +0100 | <jreicher> | EvanR: sorry, I must be missing something fundamental. I thought bitstream can't be (classically) uncountable without including non-computable streams |
| 2026-01-16 00:48:51 +0100 | <TMA> | but the smallest model contains just one infinite sequence of Is |
| 2026-01-16 00:48:53 +0100 | <EvanR> | well I never brought up classical uncountability |
| 2026-01-16 00:49:02 +0100 | <EvanR> | you're beyond me now |
| 2026-01-16 00:50:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 00:50:08 +0100 | <EvanR> | you can map (ok... lazy?) Nat to any SillyType = End | I SillyType |
| 2026-01-16 00:50:20 +0100 | <EvanR> | I mean, all |
| 2026-01-16 00:50:44 +0100 | <TMA> | jreicher: BitStream is uncountable. |
| 2026-01-16 00:50:45 +0100 | <EvanR> | seems countable |
| 2026-01-16 00:51:27 +0100 | <EvanR> | specifically, f Z = End; f (S n) = I (f n) |
| 2026-01-16 00:52:05 +0100 | <int-e> | (that's borderline stupid; SillyType is obviously isomorphic to Nat) |
| 2026-01-16 00:52:12 +0100 | <EvanR> | if you try that on Bitstream, then somebody can come along and get a counterexample stream |
| 2026-01-16 00:52:18 +0100 | <EvanR> | int-e, looooool |
| 2026-01-16 00:52:23 +0100 | <int-e> | (data Nat = Z | S N) |
| 2026-01-16 00:52:33 +0100 | <EvanR> | it's borderline Silly |
| 2026-01-16 00:52:37 +0100 | <int-e> | (data SillyType = End | I SillyType) |
| 2026-01-16 00:52:47 +0100 | <int-e> | EvanR: No, we've crossed that line long ago. |
| 2026-01-16 00:53:10 +0100 | <jreicher> | If we disallow infinite bitstreams, bitstream becomes countable. If we allow infinite bitstreams, why can't we allow transfinite silly strings? |
| 2026-01-16 00:53:32 +0100 | <EvanR> | why didn't cantor think of disallowing infinite streams |
| 2026-01-16 00:53:38 +0100 | <EvanR> | would have saved us a lot of trouble |
| 2026-01-16 00:53:42 +0100 | <int-e> | . o O ( if you disallow inifinte bitstreams, bitstream becomes empty ) |
| 2026-01-16 00:53:47 +0100 | <jreicher> | I'm not suggesting we do that. I'm just trying to understand the double standard. |
| 2026-01-16 00:53:58 +0100 | EvanR | boggles |
| 2026-01-16 00:54:54 +0100 | <TMA> | jreicher: there is transfinite silly string... it goes: I I I I I I I I I ... |
| 2026-01-16 00:55:24 +0100 | <Inline> | aye aye aye eye eye aye....... |
| 2026-01-16 00:55:29 +0100 | <int-e> | jreicher: You're insisting that two things are analogous despite strong evidence to the contrary, all of which has been laid out in front of you above. |
| 2026-01-16 00:55:38 +0100 | <Inline> | the egotist set |
| 2026-01-16 00:55:43 +0100 | <Inline> | lol |
| 2026-01-16 00:55:43 +0100 | <EvanR> | jreicher, the original definition of Bitstream and SillyType both have nothing but infinite streams. Not really a double standard |
| 2026-01-16 00:55:51 +0100 | <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-16 00:55:58 +0100 | <TMA> | jreicher: BUT there is just a single such string in the smallest model of the data SillyType = I SillyType theory |
| 2026-01-16 00:56:09 +0100 | <int-e> | Also has it really been 2 hours of this... |
| 2026-01-16 00:56:12 +0100 | <EvanR> | this is haskell an we have infinite lists |
| 2026-01-16 00:56:16 +0100 | ttybitnik | (~ttybitnik@user/wolper) (Ping timeout: 256 seconds) |
| 2026-01-16 00:56:17 +0100 | <EvanR> | turns out |
| 2026-01-16 00:56:41 +0100 | <jreicher> | But not transfinite lists |
| 2026-01-16 00:56:59 +0100 | <EvanR> | they're not needed to make the original point, just as in cantor |
| 2026-01-16 00:57:21 +0100 | <jreicher> | No, I know. I'm just picking out where the line is. |
| 2026-01-16 00:57:24 +0100 | <EvanR> | though if you want to get into that there's more exotic constructions |
| 2026-01-16 00:58:57 +0100 | trickard_ | trickard |
| 2026-01-16 01:05:34 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 01:05:48 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 01:08:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 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:11:37 +0100 | <EvanR> | all the ordinals is ... problematic but you can have a lot of them |
| 2026-01-16 01:12:16 +0100 | <jreicher> | Yeah it seems to me the "first few" would be straightforward |
| 2026-01-16 01:14:00 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-16 01:18:01 +0100 | k0zy | (~user@user/k0zy) (Ping timeout: 264 seconds) |
| 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: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:20:27 +0100 | <monochrom> | which is again just the counterintuitive "change '1' to '2' suddenly everything is different". |
| 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:21:16 +0100 | <monochrom> | I mean, if a theorem is counterintuitive, then question the intuition not the theorem. |
| 2026-01-16 01:21:22 +0100 | <jreicher> | Yes |
| 2026-01-16 01:21:44 +0100 | <EvanR> | intuition can be adjusted to fit the facts :tm: |
| 2026-01-16 01:21:51 +0100 | <jreicher> | or question the definitions/axioms that result in the theorem. |
| 2026-01-16 01:22:26 +0100 | <EvanR> | that's like questioning the game of chess itself if you lose |
| 2026-01-16 01:22:39 +0100 | <EvanR> | better to play / define another game |
| 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: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:23:01 +0100 | <jreicher> | Then it arguably doesn't satisfy its goal |
| 2026-01-16 01:23:11 +0100 | DetourNe- | (~DetourNet@user/DetourNetworkUK) DetourNetworkUK |
| 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:14 +0100 | <EvanR> | the game in which you lost nonetheless exists |
| 2026-01-16 01:23:16 +0100 | <EvanR> | and is valid |
| 2026-01-16 01:23:31 +0100 | DetourNetworkUK | (DetourNetw@user/DetourNetworkUK) (Read error: Connection reset by peer) |
| 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: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:59 +0100 | <EvanR> | I'm good |
| 2026-01-16 01:24:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:24:43 +0100 | <EvanR> | monochrom, the zero, infinity, ... rule |
| 2026-01-16 01:25:28 +0100 | DetourNe- | DetourNetworkUK |
| 2026-01-16 01:26:43 +0100 | <TMA> | monochrom: you can still have uncomputable subsets of unary strings though |
| 2026-01-16 01:26:53 +0100 | <monochrom> | "my car can do 0 to infinity in 60 seconds" >:) |
| 2026-01-16 01:27:25 +0100 | <monochrom> | TMA: Please don't go there :( >:) |
| 2026-01-16 01:29:18 +0100 | <TMA> | monochrom: good idea, I'll go to bed instead |
| 2026-01-16 01:29:26 +0100 | <monochrom> | haha |
| 2026-01-16 01:30:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 01:32:56 +0100 | Tuplanolla | (~Tuplanoll@88-114-88-95.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2026-01-16 01:40:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:45:23 +0100 | newmind | (~newmind@91-133-90-252.dyn.cablelink.at) |
| 2026-01-16 01:45:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 01:46:07 +0100 | <geekosaur> | I really should start kicking those things into #haskell-in-depth |
| 2026-01-16 01:46:41 +0100 | <monochrom> | But I think we're done. :) |
| 2026-01-16 01:47:04 +0100 | <monochrom> | But OK! Kicking people into the deep end feels good haha. |
| 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:48:33 +0100 | <geekosaur> | yeh, I've only been peeking in occasionally since I'm busy this afternoon/evening |
| 2026-01-16 01:53:28 +0100 | <jreicher> | I didn't even know about that channel |
| 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:54:52 +0100 | <dolio> | That can be a useful perspective. |
| 2026-01-16 01:56:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 01:57:28 +0100 | <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 01:58:41 +0100 | <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 02:01:26 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-16 02:01:55 +0100 | <dolio> | It can even be useful within a computing system. |
| 2026-01-16 02:02:51 +0100 | <dolio> | Like, `unsafeInterleaveIO` lets you access a bit stream that has no corresponding Haskell term. |
| 2026-01-16 02:06:59 +0100 | Zemy | (~Zemy@72.178.108.235) (Read error: Connection reset by peer) |
| 2026-01-16 02:07:09 +0100 | Zemy | (~Zemy@2600:100c:b0a0:7e6f:e8ca:c9ff:fea3:b5f7) |
| 2026-01-16 02:07:45 +0100 | Zemy_ | (~Zemy@72.178.108.235) |
| 2026-01-16 02:09:44 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-01-16 02:09:45 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-16 02:10:09 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-01-16 02:10:25 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-01-16 02:11:45 +0100 | Zemy | (~Zemy@2600:100c:b0a0:7e6f:e8ca:c9ff:fea3:b5f7) (Ping timeout: 252 seconds) |
| 2026-01-16 02:11:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 02:16:31 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 02:24:42 +0100 | divlamir | (~divlamir@user/divlamir) (Read error: Connection reset by peer) |
| 2026-01-16 02:25:05 +0100 | divlamir | (~divlamir@user/divlamir) divlamir |
| 2026-01-16 02:27:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 02:32:08 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 02:39:13 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-01-16 02:43:04 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 02:50:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-16 02:52:19 +0100 | omidmash3 | (~omidmash@user/omidmash) omidmash |
| 2026-01-16 02:53:56 +0100 | omidmash | (~omidmash@user/omidmash) (Ping timeout: 244 seconds) |
| 2026-01-16 02:53:56 +0100 | omidmash3 | omidmash |
| 2026-01-16 02:57:51 +0100 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) ryanbooker |
| 2026-01-16 03:01:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 03:04:15 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Ping timeout: 240 seconds) |
| 2026-01-16 03:04:38 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 03:06:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 03:16:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 03:21:50 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 03:23:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-16 03:24:22 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 03:29:59 +0100 | haskellbridge | (~hackager@96.28.224.214) (Remote host closed the connection) |
| 2026-01-16 03:30:46 +0100 | haskellbridge | (~hackager@96.28.224.214) hackager |
| 2026-01-16 03:30:47 +0100 | ChanServ | +v haskellbridge |
| 2026-01-16 03:30:59 +0100 | acidjnk | (~acidjnk@p200300d6e7171948e4551533bd5d7598.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2026-01-16 03:36:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 03:41:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 03:41:20 +0100 | tomboy64 | (~tomboy64@user/tomboy64) (Ping timeout: 240 seconds) |
| 2026-01-16 03:43:19 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 03:43:33 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 03:44:44 +0100 | Googulator69 | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-16 03:44:59 +0100 | Googulator69 | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-16 03:47:56 +0100 | omidmash | (~omidmash@user/omidmash) (Quit: The Lounge - https://thelounge.chat) |
| 2026-01-16 03:51:14 +0100 | omidmash | (~omidmash@user/omidmash) omidmash |
| 2026-01-16 03:51:25 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) emmanuelux |
| 2026-01-16 03:52:18 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 03:55:56 +0100 | tomboy64 | (~tomboy64@user/tomboy64) tomboy64 |
| 2026-01-16 03:56:58 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 04:08:03 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 04:13:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 04:16:22 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-16 04:16:35 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-16 04:17:12 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-16 04:23:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 04:30:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 04:34:56 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-01-16 04:35:38 +0100 | catties | Catty |
| 2026-01-16 04:36:47 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-01-16 04:36:53 +0100 | Zemy | (~Zemy@2600:100c:b000:db1:e431:70ff:fe61:4d09) |
| 2026-01-16 04:38:55 +0100 | Zemy_ | (~Zemy@72.178.108.235) (Ping timeout: 240 seconds) |
| 2026-01-16 04:39:43 +0100 | Zemy_ | (~Zemy@72.178.108.235) |
| 2026-01-16 04:40:55 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 240 seconds) |
| 2026-01-16 04:41:53 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 04:42:34 +0100 | jle` | (~jle`@2603:8001:3b00:11:930a:850f:3a65:f2e0) jle` |
| 2026-01-16 04:43:10 +0100 | Zemy | (~Zemy@2600:100c:b000:db1:e431:70ff:fe61:4d09) (Ping timeout: 246 seconds) |
| 2026-01-16 04:46:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 04:48:15 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Ping timeout: 240 seconds) |
| 2026-01-16 04:51:18 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 04:57:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 04:58:31 +0100 | CloneOfNone_ | (~CloneOfNo@user/CloneOfNone) CloneOfNone |
| 2026-01-16 05:01:31 +0100 | CloneOfNone | (~CloneOfNo@user/CloneOfNone) (Ping timeout: 264 seconds) |
| 2026-01-16 05:01:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 05:02:03 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 252 seconds) |
| 2026-01-16 05:06:58 +0100 | jmcantrell | (~weechat@user/jmcantrell) (Ping timeout: 246 seconds) |
| 2026-01-16 05:07:33 +0100 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2026-01-16 05:09:13 +0100 | pipsquak-bird | (~g@c-71-235-170-34.hsd1.ma.comcast.net) |
| 2026-01-16 05:11:23 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-16 05:12:39 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 05:13:01 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 05:13:14 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 05:16:46 +0100 | weary-traveler | (~user@user/user363627) user363627 |
| 2026-01-16 05:16:58 +0100 | She | (haveident@libera/staff/she/her) (Quit: Either upgrades, or the world's ending.) |
| 2026-01-16 05:17:34 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 05:18:30 +0100 | She | (haveident@libera/staff/she/her) She |
| 2026-01-16 05:25:21 +0100 | comonad | (~comonad@p200300d02722ae00dce4ce9451b59974.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 2026-01-16 05:28:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 05:28:58 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-01-16 05:29:51 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 05:30:05 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 05:32:52 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Remote host closed the connection) |
| 2026-01-16 05:33:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 05:34:55 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) (Ping timeout: 240 seconds) |
| 2026-01-16 05:39:23 +0100 | Zemy | (~Zemy@2600:100c:b000:db1:d457:8cff:fed5:dff0) |
| 2026-01-16 05:39:23 +0100 | Zemy_ | (~Zemy@72.178.108.235) (Read error: Connection reset by peer) |
| 2026-01-16 05:40:06 +0100 | Zemy_ | (~Zemy@72.178.108.235) |
| 2026-01-16 05:43:59 +0100 | Zemy | (~Zemy@2600:100c:b000:db1:d457:8cff:fed5:dff0) (Ping timeout: 260 seconds) |
| 2026-01-16 05:44:12 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 05:45:27 +0100 | Zemy | (~Zemy@2600:100c:b000:db1:c051:aeff:fe7a:2412) |
| 2026-01-16 05:45:28 +0100 | Zemy_ | (~Zemy@72.178.108.235) (Read error: Connection reset by peer) |
| 2026-01-16 05:46:05 +0100 | Zemy_ | (~Zemy@72.178.108.235) |
| 2026-01-16 05:47:54 +0100 | trickard__ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-16 05:48:17 +0100 | trickard__ | trickard |
| 2026-01-16 05:48:34 +0100 | ystael | (~ystael@user/ystael) (Ping timeout: 244 seconds) |
| 2026-01-16 05:49:13 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Ping timeout: 264 seconds) |
| 2026-01-16 05:49:31 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 05:49:49 +0100 | Zemy | (~Zemy@2600:100c:b000:db1:c051:aeff:fe7a:2412) (Ping timeout: 260 seconds) |
| 2026-01-16 05:59:53 +0100 | tessier | (~tessier@ip68-8-117-219.sd.sd.cox.net) tessier |
| 2026-01-16 05:59:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 06:01:22 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) chromoblob\0 |
| 2026-01-16 06:01:56 +0100 | <jreicher> | monochrom: do you also have lecture notes that deal with countability? (I don't want to restart the topic here; asking only this question) |
| 2026-01-16 06:04:59 +0100 | jle` | (~jle`@2603:8001:3b00:11:930a:850f:3a65:f2e0) (Ping timeout: 250 seconds) |
| 2026-01-16 06:06:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 06:06:48 +0100 | jle` | (~jle`@2603:8001:3b00:11:de64:4c9b:8263:d4ce) jle` |
| 2026-01-16 06:15:09 +0100 | bggd_ | (~bgg@2a01:e0a:fd5:f510:8d9:51ba:2d0b:e2a0) |
| 2026-01-16 06:18:02 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 06:21:19 +0100 | jle` | (~jle`@2603:8001:3b00:11:de64:4c9b:8263:d4ce) (Quit: WeeChat 4.7.1) |
| 2026-01-16 06:22:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-16 06:23:34 +0100 | trickard | (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 06:23:48 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-16 06:26:13 +0100 | jle` | (~jle`@2603:8001:3b00:11:a778:c925:9c27:688d) jle` |
| 2026-01-16 06:29:49 +0100 | michalz | (~michalz@185.246.207.201) |
| 2026-01-16 06:30:22 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) humasect |
| 2026-01-16 06:31:29 +0100 | karenw | (~karenw@user/karenw) karenw |
| 2026-01-16 06:33:23 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 06:38:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 06:38:27 +0100 | mange | (~mange@user/mange) (Quit: Quittin' time!) |
| 2026-01-16 06:44:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 06:46:38 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 06:46:52 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-16 06:48:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 250 seconds) |
| 2026-01-16 06:53:07 +0100 | trickard_ | trickard |
| 2026-01-16 06:55:12 +0100 | jreicher | (~joelr@user/jreicher) (Quit: In transit) |
| 2026-01-16 06:55:13 +0100 | troydm | (~troydm@user/troydm) (Ping timeout: 244 seconds) |
| 2026-01-16 06:56:09 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-16 06:58:57 +0100 | trickard | (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 06:59:10 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-16 06:59:41 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 07:04:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2026-01-16 07:05:10 +0100 | doyougnu | (~doyougnu@38.175.72.111) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2026-01-16 07:06:26 +0100 | doyougnu | (~doyougnu@38.175.72.111) doyougnu |
| 2026-01-16 07:08:33 +0100 | machinedgod | (~machinedg@d75-159-126-101.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2026-01-16 07:15:27 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 07:18:03 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) |
| 2026-01-16 07:20:26 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 07:23:36 +0100 | pabs3 | (~pabs3@user/pabs3) (Ping timeout: 252 seconds) |
| 2026-01-16 07:23:48 +0100 | ft | (~ft@p4fc2a9d7.dip0.t-ipconnect.de) (Quit: leaving) |
| 2026-01-16 07:24:34 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) Enrico63 |
| 2026-01-16 07:29:24 +0100 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2026-01-16 07:30:06 +0100 | gmg | (~user@user/gehmehgeh) gehmehgeh |
| 2026-01-16 07:30:50 +0100 | doyougnu | (~doyougnu@38.175.72.111) (Ping timeout: 265 seconds) |
| 2026-01-16 07:31:14 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 07:31:26 +0100 | pabs3 | (~pabs3@user/pabs3) pabs3 |
| 2026-01-16 07:34:37 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) hardyhardhard |
| 2026-01-16 07:36:02 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 07:37:20 +0100 | trickard_ | trickard |
| 2026-01-16 07:41:43 +0100 | Eoco | (~ian@128.101.131.218) (Ping timeout: 244 seconds) |
| 2026-01-16 07:41:49 +0100 | remexre | (~remexre@user/remexre) (Ping timeout: 260 seconds) |
| 2026-01-16 07:42:07 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) (Ping timeout: 272 seconds) |
| 2026-01-16 07:42:46 +0100 | remexre | (~remexre@user/remexre) remexre |
| 2026-01-16 07:43:28 +0100 | Eoco | (~ian@128.101.131.218) Eoco |
| 2026-01-16 07:43:55 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2026-01-16 07:44:20 +0100 | ChaiTRex | (~ChaiTRex@user/chaitrex) ChaiTRex |
| 2026-01-16 07:47:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 07:53:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 08:05:04 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 08:10:24 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-16 08:11:22 +0100 | jreicher | (~joelr@user/jreicher) jreicher |
| 2026-01-16 08:12:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 08:17:06 +0100 | sord937 | (~sord937@gateway/tor-sasl/sord937) sord937 |
| 2026-01-16 08:17:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-16 08:20:45 +0100 | trickard | (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 08:20:59 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-16 08:27:38 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 08:32:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 08:33:28 +0100 | GdeVolpi1 | (~GdeVolpia@user/GdeVolpiano) (Quit: WeeChat 4.7.2) |
| 2026-01-16 08:33:30 +0100 | haskellbridge | (~hackager@96.28.224.214) (Read error: Connection reset by peer) |
| 2026-01-16 08:33:45 +0100 | GdeVolpiano | (~GdeVolpia@user/GdeVolpiano) GdeVolpiano |
| 2026-01-16 08:33:51 +0100 | doyougnu | (~doyougnu@38.175.72.111) |
| 2026-01-16 08:35:14 +0100 | haskellbridge | (~hackager@96.28.224.214) hackager |
| 2026-01-16 08:35:15 +0100 | ChanServ | +v haskellbridge |
| 2026-01-16 08:36:39 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) hardyhardhard |
| 2026-01-16 08:40:07 +0100 | housemate | (~housemate@203.56.146.214) (Quit: https://ineedsomeacidtocalmmedown.space/) |
| 2026-01-16 08:41:22 +0100 | Hardyhardhard | (~Hardyhard@user/hardyhardhard) (Client Quit) |
| 2026-01-16 08:43:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 08:43:37 +0100 | housemate | (~housemate@203.56.146.214) housemate |
| 2026-01-16 08:49:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 08:51:49 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2026-01-16 09:00:58 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 09:02:11 +0100 | jessicara | (~shirogits@user/meow/jessicara) jessicara |
| 2026-01-16 09:05:52 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-16 09:06:31 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 240 seconds) |
| 2026-01-16 09:07:29 +0100 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2026-01-16 09:08:35 +0100 | poscat0x04 | (~poscat@user/poscat) poscat |
| 2026-01-16 09:08:39 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) |
| 2026-01-16 09:08:54 +0100 | CiaoSen | (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen |
| 2026-01-16 09:10:31 +0100 | poscat | (~poscat@user/poscat) (Ping timeout: 264 seconds) |
| 2026-01-16 09:11:38 +0100 | Googulator69 | Googulator |
| 2026-01-16 09:12:19 +0100 | krei-se- | (~krei-se@p3ee0fe0e.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2026-01-16 09:13:58 +0100 | krei-se | (~krei-se@p50829ec0.dip0.t-ipconnect.de) krei-se |
| 2026-01-16 09:14:58 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) (Quit: Client closed) |
| 2026-01-16 09:16:29 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Ping timeout: 272 seconds) |
| 2026-01-16 09:16:42 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 09:21:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-16 09:21:47 +0100 | trickard_ | trickard |
| 2026-01-16 09:26:30 +0100 | trickard | (~trickard@cpe-82-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 09:26:44 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-16 09:32:30 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 09:33:45 +0100 | chele | (~chele@user/chele) chele |
| 2026-01-16 09:37:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-16 09:41:38 +0100 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2026-01-16 09:45:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 09:45:20 +0100 | emmanuelux | (~emmanuelu@user/emmanuelux) (Remote host closed the connection) |
| 2026-01-16 09:50:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 09:53:25 +0100 | fgarcia | (~lei@user/fgarcia) (Ping timeout: 264 seconds) |
| 2026-01-16 09:53:33 +0100 | __monty__ | (~toonn@user/toonn) toonn |
| 2026-01-16 09:56:30 +0100 | danza | (~danza@user/danza) danza |
| 2026-01-16 09:56:57 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) Enrico63 |
| 2026-01-16 10:00:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 10:05:46 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 10:15:16 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 10:17:52 +0100 | Googulator | (~Googulato@team.broadbit.hu) |
| 2026-01-16 10:19:35 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 10:20:05 +0100 | danza | (~danza@user/danza) (Remote host closed the connection) |
| 2026-01-16 10:20:25 +0100 | karenw | (~karenw@user/karenw) (Ping timeout: 264 seconds) |
| 2026-01-16 10:25:46 +0100 | acidjnk | (~acidjnk@p200300d6e71719276ddc164bdcca8bf0.dip0.t-ipconnect.de) acidjnk |
| 2026-01-16 10:30:47 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 10:32:24 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 2026-01-16 10:33:43 +0100 | danza | (~danza@user/danza) danza |
| 2026-01-16 10:34:20 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-01-16 10:35:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 10:46:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 10:47:09 +0100 | Brumaire | (~no@94.140.114.73) Brumaire |
| 2026-01-16 10:47:09 +0100 | Brumaire | (~no@94.140.114.73) (Client Quit) |
| 2026-01-16 10:52:50 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-16 10:54:05 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) (Ping timeout: 245 seconds) |
| 2026-01-16 10:54:26 +0100 | trickard_ | (~trickard@cpe-82-98-47-163.wireline.com.au) |
| 2026-01-16 10:54:40 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 256 seconds) |
| 2026-01-16 10:56:03 +0100 | Lycurgus | (~juan@user/Lycurgus) (Quit: alsoknownas.renjuan.org ( juan@acm.org )) |
| 2026-01-16 10:59:30 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 245 seconds) |
| 2026-01-16 11:00:56 +0100 | trickard_ | trickard |
| 2026-01-16 11:04:11 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 11:05:25 +0100 | newmind | (~newmind@91-133-90-252.dyn.cablelink.at) (Ping timeout: 272 seconds) |
| 2026-01-16 11:08:15 +0100 | fgarcia | (~lei@user/fgarcia) fgarcia |
| 2026-01-16 11:08:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 11:19:59 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 11:25:17 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-16 11:35:46 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 11:39:55 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 11:45:21 +0100 | fp | (~Thunderbi@130.233.70.149) fp |
| 2026-01-16 11:45:31 +0100 | fp | (~Thunderbi@130.233.70.149) (Remote host closed the connection) |
| 2026-01-16 11:47:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 11:48:33 +0100 | caubert | (~caubert@user/caubert) caubert |
| 2026-01-16 11:52:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 12:01:45 +0100 | fp | (~Thunderbi@2001:708:20:1406::10c5) fp |
| 2026-01-16 12:03:06 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 12:08:01 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-16 12:17:00 +0100 | ZLima12_ | ZLima12 |
| 2026-01-16 12:18:51 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 12:23:43 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 12:33:31 +0100 | Lycurgus | (~juan@user/Lycurgus) Lycurgus |
| 2026-01-16 12:34:36 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 12:39:19 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds) |
| 2026-01-16 12:47:56 +0100 | <gentauro> | build elm-compiler 0.19.1 (7 years last commit) with stack, just works as a charm. Trying to build "something" with cabal + flakes … "yeah, let me build that ghc 8.10.7 which isn't really needed for scratch. See you in several hours" :| |
| 2026-01-16 12:48:01 +0100 | <gentauro> | haha |
| 2026-01-16 12:48:12 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 12:48:24 +0100 | L29Ah | (~L29Ah@wikipedia/L29Ah) L29Ah |
| 2026-01-16 12:48:27 +0100 | <gentauro> | «avoid success at all costs» (Y) |
| 2026-01-16 12:51:27 +0100 | dyniec | (~dyniec@dybiec.info) (Remote host closed the connection) |
| 2026-01-16 12:52:05 +0100 | dyniec | (~dyniec@dybiec.info) dyniec |
| 2026-01-16 12:52:30 +0100 | <danza> | it's not that bad |
| 2026-01-16 12:52:49 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-16 12:54:16 +0100 | <gentauro> | I guess it has to do with Snoyman transitioning to Rust :'( |
| 2026-01-16 12:57:05 +0100 | Enrico63 | (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) (Quit: Client closed) |
| 2026-01-16 13:01:34 +0100 | <danza> | cabal has improved quite a lot |
| 2026-01-16 13:01:39 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:8c87:65e5:9de1:f975) |
| 2026-01-16 13:01:39 +0100 | chewybread | (~chewybrea@240b:10:9502:4100:8c87:65e5:9de1:f975) (Changing host) |
| 2026-01-16 13:01:39 +0100 | chewybread | (~chewybrea@user/chewybread) chewybread |
| 2026-01-16 13:02:56 +0100 | dyniec | (~dyniec@dybiec.info) (Remote host closed the connection) |
| 2026-01-16 13:03:17 +0100 | Zemy | (~Zemy@2600:100c:b0ab:2acb:a81f:adff:fe14:77e5) |
| 2026-01-16 13:03:17 +0100 | Zemy_ | (~Zemy@72.178.108.235) (Read error: Connection reset by peer) |
| 2026-01-16 13:03:44 +0100 | dyniec | (~dyniec@dybiec.info) dyniec |
| 2026-01-16 13:03:54 +0100 | Zemy_ | (~Zemy@72.178.108.235) |
| 2026-01-16 13:03:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |