Logs: liberachat/#haskell
| 2026-01-15 22:08:05 | <EvanR> | that's the point |
| 2026-01-15 22:08:11 | <int-e> | EvanR: Well, in isolation, assuming it isn't fused away :P |
| 2026-01-15 22:08:33 | <EvanR> | you can't generate a stream of all the lists |
| 2026-01-15 22:08:34 | <monochrom> | I thought I explained that. A model that contains impractical elements can be a useful approximation and/or abstraction. |
| 2026-01-15 22:08:47 | <EvanR> | some are necessarily missing |
| 2026-01-15 22:08:55 | <EvanR> | no matter how you go about it |
| 2026-01-15 22:09:01 | <dolio> | Uncomputable lists aren't real. |
| 2026-01-15 22:09:20 | <EvanR> | and cantor's proof produces a constructive example list which isn't there |
| 2026-01-15 22:09:21 | <jreicher> | And if they're missing, how is it meaningful to say the type is uncountable? (I feel like this is hitting downward lowenheim-skolem somehow) |
| 2026-01-15 22:09:21 | <int-e> | If you don't model this mathematically, countability doesn't even come up; there is no set whose cardinality you could possibly discuss. |
| 2026-01-15 22:09:22 | <EvanR> | kind of cool |
| 2026-01-15 22:09:52 | <EvanR> | jreicher, this is like saying any map from N into A necessarily misses some As |
| 2026-01-15 22:10:05 | <EvanR> | which is what we're trying to say |
| 2026-01-15 22:10:05 | <jreicher> | Not "some". Most. |
| 2026-01-15 22:10:09 | <EvanR> | sure |
| 2026-01-15 22:10:18 | <EvanR> | that's what uncountable is |
| 2026-01-15 22:10:42 | → | Zemy joins (~Zemy@72.178.108.235) |
| 2026-01-15 22:10:58 | <dolio> | Every computable map misses many computable streams. |
| 2026-01-15 22:11:04 | <jreicher> | So let me re-ask the question. Do you think it's possible to model all this mathematically such that BitStream is a countable infinite type? |
| 2026-01-15 22:11:21 | <EvanR> | sure |
| 2026-01-15 22:11:26 | <monochrom> | Yes. For example operational semantics. |
| 2026-01-15 22:11:44 | <jreicher> | OK. So what do we gain from adding the assertion (because we'd need to) that makes it uncountable? |
| 2026-01-15 22:11:47 | <monochrom> | Another example: Translating Haskell to Turing machines. |
| 2026-01-15 22:12:00 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-15 22:12:03 | <EvanR> | this is why I began by phrasing the whole thing as "are you sure" about not having uncountable things, it depends on how you think about it |
| 2026-01-15 22:12:03 | <int-e> | When you model programs mathematically, you typically do not impose a running time bound up front, so the modelled program behavior is effectively infinite (since you can run it to any arbitrary length, giving you a state after n steps for all natural numbers n). |
| 2026-01-15 22:12:14 | <int-e> | It's a simplification. |
| 2026-01-15 22:12:18 | <EvanR> | jreicher, it's not an assertion, there's a constructive proof xD |
| 2026-01-15 22:12:22 | <monochrom> | Avoiding the cumbersomeness and missing-the-forest-for-the-trees of operational semantics and Turing machines. |
| 2026-01-15 22:12:27 | <EvanR> | yielding the missing stream |
| 2026-01-15 22:12:57 | <jreicher> | EvanR: the proof (like all proofs) starts with axioms. The axioms are the assertions. |
| 2026-01-15 22:13:00 | <EvanR> | that you can't run a program for infinite time isn't the secret sauce to model it as countable |
| 2026-01-15 22:13:04 | <EvanR> | that's more like ultrafinitism |
| 2026-01-15 22:13:13 | <monochrom> | My lecture notes also shows that if you use this "unrealistic" (but still sound) denotational approach, it is easier to predict the outcome of certain recursive definitions. |
| 2026-01-15 22:13:20 | <EvanR> | jreicher, in type theory, we don't always have axioms! |
| 2026-01-15 22:13:33 | <jreicher> | How can you have a theory without axioms? |
| 2026-01-15 22:13:37 | <EvanR> | definitions |
| 2026-01-15 22:13:40 | <int-e> | And, correspondingly, the easiest model for streams of Bools gives you an arbitrary boolean value for the n-th element of the stream, for each natural number N. The set of all these functions is uncountable. |
| 2026-01-15 22:13:46 | <jreicher> | Definitions are axioms |
| 2026-01-15 22:13:55 | <int-e> | Again, keeping things as mathematically simple as possible. |
| 2026-01-15 22:13:57 | <EvanR> | well that's muddying things a lot isn't it |
| 2026-01-15 22:14:10 | <jreicher> | Not for a formal theory, no |
| 2026-01-15 22:14:16 | <EvanR> | definition is just naming something that you could already say long winded |
| 2026-01-15 22:14:22 | <EvanR> | to save space |
| 2026-01-15 22:14:51 | <monochrom> | The hardest example made easy being fs = 1 : 1 : zipWith (+) fs (tail fs). |
| 2026-01-15 22:14:53 | <jreicher> | int-e: monochrom: I appreciate the use of "extra" infinity as a simplification. Not the first time I've heard that argument. |
| 2026-01-15 22:15:12 | <EvanR> | an example of an axiom in type theory is the law of excluded middle. Introduces by fiat. As opposed to proven as a theorem somehow |
| 2026-01-15 22:15:21 | <EvanR> | introduced* |
| 2026-01-15 22:15:24 | <monochrom> | Every textbook or tutorial I saw tried to explain it poorly with lazy evaluation. |
| 2026-01-15 22:15:24 | <jreicher> | "fiar" is "assertion" |
| 2026-01-15 22:15:25 | × | chromoblob quits (~chromoblo@user/chromob1ot1c) (Ping timeout: 256 seconds) |
| 2026-01-15 22:15:27 | <jreicher> | *fiat |
| 2026-01-15 22:16:07 | <monochrom> | But if you do the denotational "construct the approximation sequence, take limit" it's plain as day. |
| 2026-01-15 22:18:26 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 2026-01-15 22:20:16 | <dolio> | All you need to do to have uncountable bit streams is live within constructive mathematics, recognizing that it holds for computable things (computability allows extra principles on top of bare constructive mathematics, actually). |
| 2026-01-15 22:20:31 | <dolio> | Cantor's diagonal argument is constructive, ergo bit streams are uncountable. |
| 2026-01-15 22:20:41 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 22:20:50 | <monochrom> | (About theory with/wo axioms. I don't draw lines between axioms, definitions, inference rules either.) |
| 2026-01-15 22:20:54 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 22:20:55 | <int-e> | dolio: see me 15 minutes ago ;-) |
| 2026-01-15 22:20:56 | <dolio> | The only way they look countable is if you believe in classical mathematics and try to build computability within that. |
| 2026-01-15 22:21:22 | <EvanR> | another thing, my kneejerk devil's advocate arguement for the countable Bitstream is that you can only have finite many programs. However in haskell you can obtain Bitstream other ways... which perhaps also avoids computability |
| 2026-01-15 22:21:32 | <EvanR> | s/finite/countable/ |
| 2026-01-15 22:21:56 | <dolio> | But in the natural mathematics of computable things, they are uncountable. The ways to count them are not computable. |
| 2026-01-15 22:22:17 | <dolio> | So reject them. |
| 2026-01-15 22:22:56 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 22:23:26 | <monochrom> | That gives very different feel... But I confess I'm classical in my core, I only pretend to be intuitionistic when it's convenient. :) |
| 2026-01-15 22:23:54 | <EvanR> | monochrom, I'm calling definitions shorthand that expands to something we already had. Unlike e.g. "the answer to any LEM question you name" |
| 2026-01-15 22:23:56 | <dolio> | The diagonal argument shows that any computable way to enumerate computable bit streams misses some of the computable bit streams. You don't need uncomputable ones for the enumeration to be incomplete. |
| 2026-01-15 22:24:34 | <EvanR> | basically syntactic sugar |
| 2026-01-15 22:24:39 | <monochrom> | Because classical uncountability gives me a feeling of size, but constructive uncountability doesn't feel like "bigger size", just "unreachable". |
| 2026-01-15 22:25:03 | <EvanR> | again, isn't this saying more about misunderstanding classical notions ? xD |
| 2026-01-15 22:25:03 | <dolio> | Yes, the idea that uncountability is about "size" is an erroneous extrapolation from finite sets. |
| 2026-01-15 22:25:34 | <dolio> | The extended natural numbers are uncountable. |
| 2026-01-15 22:25:36 | <monochrom> | EvanR, I clone every definition to be an axiom, e.g., definition "x := 4" is cloned so I add an axiom "x = 4". |
| 2026-01-15 22:25:42 | <dolio> | How many more are there? At most one. |
| 2026-01-15 22:25:43 | × | takuan quits (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 240 seconds) |
| 2026-01-15 22:25:56 | <EvanR> | monochrom, what do you achieve by doing this xD |
| 2026-01-15 22:26:02 | <EvanR> | twice as many definitions / axioms? xD |
| 2026-01-15 22:26:15 | <monochrom> | I achieve "they are all axioms". |
| 2026-01-15 22:26:17 | <dolio> | But infinity + 1 = infinity, right? |
| 2026-01-15 22:26:58 | <EvanR> | monochrom, it's a slippery slope from there to buffyspeak anything can be anythinged! |
| 2026-01-15 22:27:17 | <dolio> | (That uncountability part requires more committment to computable principles.) |
| 2026-01-15 22:27:31 | <monochrom> | Oh sure, I then further consider axioms to be special cases of theorems! |
| 2026-01-15 22:28:02 | <EvanR> | 🤢 |
| 2026-01-15 22:28:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 22:28:24 | <int-e> | has anybody said "global assumptions" |
| 2026-01-15 22:28:41 | <EvanR> | theorems ideally come with proofs, while you wouldn't expect a proof |
| 2026-01-15 22:28:45 | <monochrom> | But I stop there. When I prove something, I only need a line between theorems and non-theorems. Why should I care about further distinctions between "different kinds" of theorems? |
| 2026-01-15 22:28:51 | <EvanR> | if we don't want anything to mean anything, we can do that I guess xD |
| 2026-01-15 22:29:01 | <EvanR> | wouldn't expect proof of an axiom* |
| 2026-01-15 22:29:23 | <EvanR> | and "proving a definition" is itself like a classic fallacy xD |
| 2026-01-15 22:30:23 | <monochrom> | Consider a tree as in computer science or programming. There are root nodes, there are children nodes, there are greatgreatgrandganddaughter nodes, you can make infinitely many artificial distinctions between nodes living at different positions in the tree... |
| 2026-01-15 22:30:32 | <monochrom> | WHY SHOULD I CARE. They're all nodes. |
| 2026-01-15 22:30:35 | <int-e> | EvanR: You can prove that adding a definitional axiom (of the shape <new name> = <expression>) is a conservative extension for any [add suitable adjective] logic |
| 2026-01-15 22:30:56 | <EvanR> | monochrom, really, all these things fit inside a neat tree of life somehow? |
| 2026-01-15 22:30:58 | <int-e> | EvanR: thereby proving all definitions at once ;-) |
| 2026-01-15 22:30:58 | <monochrom> | For the simple purpose of traversing or generating that tree, they are all nodes, period. |
| 2026-01-15 22:31:03 | <EvanR> | I was trying to get away from that with jreicher |
| 2026-01-15 22:31:25 | <int-e> | @quote |
All times are in UTC.