Newest at the top
| 2026-01-15 23:08:11 +0100 | <int-e> | EvanR: Well, in isolation, assuming it isn't fused away :P |
| 2026-01-15 23:08:05 +0100 | <EvanR> | that's the point |
| 2026-01-15 23:07:56 +0100 | <jreicher> | EvanR: I don't think so, no. I'm saying something more like you can't generate ALL infinite lists that way (e.g. uncomputable ones) |
| 2026-01-15 23:07:46 +0100 | <EvanR> | if you're lucky |
| 2026-01-15 23:07:39 +0100 | <EvanR> | in ghc! |
| 2026-01-15 23:07:32 +0100 | <int-e> | (once fully evaluated) |
| 2026-01-15 23:07:25 +0100 | <int-e> | it's a very finite graph :P |
| 2026-01-15 23:07:09 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:07:04 +0100 | <EvanR> | in haskell xD |
| 2026-01-15 23:07:00 +0100 | <EvanR> | you're trying to say like > repeat 'a' is not an infinite list |
| 2026-01-15 23:06:25 +0100 | <jreicher> | If we say infinite bitstreams exist, then the type is uncountable. I'm not arguing with that. But in practice (and I hesitate as I say that) you're never going to have an infinite bitstream, so I'm not sure this is a sensible thing to say. |
| 2026-01-15 23:06:21 +0100 | <dolio> | I.E. given a computable enumeration of computable bit streams, one can compute a bit stream not in the enumeration. |
| 2026-01-15 23:06:03 +0100 | <EvanR> | i.e. the only thing that is real is a real running program on a computer, which will never be infinite, because the universe is purely finite or something. Which is the kind of stuff I'd like to use math to avoid entirely |
| 2026-01-15 23:05:51 +0100 | <dolio> | Viewed externally as built in classical mathematics, that is the statement, 'the set of recursive bit streams is "computably uncountable."' |
| 2026-01-15 23:05:23 +0100 | <int-e> | And a clear distinction between object and meta levels, because at the object level, for any sequence of sequences f :: Nat -> (Nat -> Bool) you can apply Cantor's diagonal construction, s n = not (f n n) to obtain a sequence that's not in the enumeration. (I'll skip how Nat -> Bool is equivalent to streams of bools) |
| 2026-01-15 23:05:11 +0100 | <dolio> | Internally to the world of recursive mathematics, Cantor's diagonal argument holds, and the type of infinite bit streams is uncountable. |
| 2026-01-15 23:05:09 +0100 | <EvanR> | sounds like operational semantics |
| 2026-01-15 23:04:52 +0100 | <jreicher> | I have to think this through carefully, but I think you are all accepting the existence of infinitely-running programs? |
| 2026-01-15 23:04:26 +0100 | <dolio> | E.G. if you build recursive things in classical mathematics, it will appear that the set of recursively definable streams is countable. But the enumeration of all such streams is not recursive. |
| 2026-01-15 23:04:20 +0100 | <EvanR> | (but I might be wrong here beacuse of higher order programs) |
| 2026-01-15 23:03:54 +0100 | Inline | (~User@cgn-195-14-218-118.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/) |
| 2026-01-15 23:03:46 +0100 | <EvanR> | or definability, because you have to write the code, and code is countable |
| 2026-01-15 23:03:29 +0100 | <dolio> | jreicher: The only way to believe that being recursive makes things countable is by not taking recursion seriously enough. When you set up your mathematics such that everything is inherently recursive, some things in that mathematics become uncountable again. |
| 2026-01-15 23:03:22 +0100 | <int-e> | (I can defend the idea that streams are countable but it'll involve computability and/or Scott domains) |
| 2026-01-15 23:02:58 +0100 | <EvanR> | jreicher, good xD |
| 2026-01-15 23:02:48 +0100 | <EvanR> | you first need to know what Bitstreams even are, and then you can progress to the cantor style proof which mirrors the classic version for binary strings |
| 2026-01-15 23:02:39 +0100 | <jreicher> | I'm not finitist. I just said infinite series of finite objects. |
| 2026-01-15 23:02:30 +0100 | <monochrom> | OK sure. Read my lecture notes first? |
| 2026-01-15 23:02:25 +0100 | <int-e> | But how can you discuss countability in a finitist context? :P |
| 2026-01-15 23:02:17 +0100 | <jreicher> | I'm not rejecting denotational semantics. I'd just like a pointer to something that explains where/how/why anything uncountable comes in. |
| 2026-01-15 23:01:52 +0100 | <monochrom> | I can respect that you reject denotational semantics altogether, but then you should also be rejecting "bottom". |
| 2026-01-15 23:01:08 +0100 | <EvanR> | the corresponding complaint about infinite objects in normal math is getting worse than I thought, though allowing "infinite" versions of each value at least isn't ultrafinite |
| 2026-01-15 23:01:01 +0100 | <monochrom> | If you don't complain that I said "bottom", then you have accepted that I am doing a denotational semantics model, and therefore there are infinite strings in the model. |
| 2026-01-15 23:00:54 +0100 | <lambdabot> | [0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1,0,1... |
| 2026-01-15 23:00:53 +0100 | <dolio> | > cycle [0,1] |
| 2026-01-15 23:00:25 +0100 | <int-e> | . o O ( it must be nice to have convictions ) |
| 2026-01-15 23:00:10 +0100 | EvanR | looks at jreicher |
| 2026-01-15 22:59:58 +0100 | <EvanR> | I guess including all these partially defined possibilities is making it even more infinite |
| 2026-01-15 22:59:48 +0100 | <jreicher> | You have an infinite series of finite strings |
| 2026-01-15 22:59:40 +0100 | <jreicher> | monochrom: My only point is that none of these recursive datatypes give you infinite strings. |
| 2026-01-15 22:58:55 +0100 | peterbecich | (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds) |
| 2026-01-15 22:58:52 +0100 | <monochrom> | The increasing sequence I bottom, I (I bottom), I (I (I bottom)) ... needs a least upper bound. |
| 2026-01-15 22:58:18 +0100 | <EvanR> | there's no finite strings by design, so I'm confused by that |
| 2026-01-15 22:57:57 +0100 | <monochrom> | You need infinite strings for completeness. |
| 2026-01-15 22:57:12 +0100 | <jreicher> | monochrom: Exactly. So making it a "binary choice" recursion doesn't magically make it uncountable |
| 2026-01-15 22:56:59 +0100 | <EvanR> | so cardinalty 1 |
| 2026-01-15 22:56:54 +0100 | <EvanR> | jreicher, is the only (respectable) value here I (I (I (I ...)))? |
| 2026-01-15 22:56:47 +0100 | <monochrom> | SillyType is countable. |
| 2026-01-15 22:56:46 +0100 | <jreicher> | monochrom: there aren't any infinite bit strings in the set |
| 2026-01-15 22:56:23 +0100 | <monochrom> | With my notes, you can either take the watered-down take in the first half, where I just assert that all infinite bit strings are in the set for the type, then use the usual diagonizable argument; or use the second half where I describe the recipe for the set for non-strict ADTs in general, then do it for BitStream yourself... |