Logs: liberachat/#haskell
| 2026-01-15 21:35:01 | <dolio> | I'd be a little surprised if the lexing were undecidable, but I'm not much of a C++ guru. |
| 2026-01-15 21:35:02 | <jreicher> | I can't see how it's possible. You only get countable infinities with recursion. |
| 2026-01-15 21:35:03 | <EvanR> | datatypes which could not possibly be enumerated (in haskell) |
| 2026-01-15 21:35:17 | <EvanR> | i.e. make a full list of them |
| 2026-01-15 21:35:27 | <EvanR> | of the values |
| 2026-01-15 21:35:48 | <dolio> | Maybe not super surprised. |
| 2026-01-15 21:39:45 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 21:40:00 | <davean> | dolio: I just don't recally how they define their boundary |
| 2026-01-15 21:41:35 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 21:41:52 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 21:43:44 | <monochrom> | Denotational semantics for lazy infinite streams are full of uncountable data types. So someone wants it. But that someone also acknowledges that it is just a model, and it is chosen for a trade-off. Uncontability is weird and unrealistic, but it buys simplcity for something else. |
| 2026-01-15 21:44:15 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 21:46:06 | <jreicher> | monochrom: got a reference? That doesn't sound sensible to me |
| 2026-01-15 21:46:37 | <monochrom> | I don't have a reference. |
| 2026-01-15 21:46:53 | <EvanR> | if you disagree that haskell has uncountable datatypes, it's possible normal set theory also doesn't xD |
| 2026-01-15 21:47:03 | <monochrom> | Not even when that someone is me. I don't bother to write a paper for that. |
| 2026-01-15 21:47:06 | <jreicher> | I don't disagree. I just can't see how it's possible. |
| 2026-01-15 21:47:45 | <jreicher> | Uncountability, in a way, "comes from nowhere". It has to be asserted. You can't constructit. |
| 2026-01-15 21:47:48 | <EvanR> | here is one... data Bitstream = I Bitstream | O Bitstream |
| 2026-01-15 21:47:58 | <EvanR> | jreicher, why do you think this xD |
| 2026-01-15 21:48:09 | <monochrom> | Oh it is asserted. Denotational semantics are seldom constructive. |
| 2026-01-15 21:48:10 | <jreicher> | EvanR: how is that uncountable? |
| 2026-01-15 21:48:27 | <EvanR> | you define things and then see if this or that satisfies the definition |
| 2026-01-15 21:48:32 | <EvanR> | nothing wrong with definitions |
| 2026-01-15 21:49:00 | <EvanR> | jreicher, there was this guy cantor with this diagonalization argument |
| 2026-01-15 21:49:09 | <geekosaur> | ^ |
| 2026-01-15 21:49:24 | <EvanR> | it made a lot of people very angry and was generally considered a bad idea |
| 2026-01-15 21:49:28 | <geekosaur> | that was my thought, it either proves countability or provides a recipe to construct uncountably many values |
| 2026-01-15 21:49:46 | <jreicher> | Yes, but that datatype is not all the reals |
| 2026-01-15 21:49:53 | <EvanR> | reals? |
| 2026-01-15 21:49:55 | <jreicher> | You can't make the diagonalisation from it |
| 2026-01-15 21:50:06 | <EvanR> | that's .. neither here nor there |
| 2026-01-15 21:50:22 | <jreicher> | Any bitstream value is INDEFINITE length, but it's still FINITE. |
| 2026-01-15 21:50:31 | <EvanR> | wat |
| 2026-01-15 21:50:44 | <jreicher> | You can't have an infinite bitstream value |
| 2026-01-15 21:50:56 | <EvanR> | we're about to jump the shark from uncountability to ultrafinitism |
| 2026-01-15 21:51:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 21:51:37 | <EvanR> | ignoring bottoms there's no way to make a finite Bitstream |
| 2026-01-15 21:51:39 | <monochrom> | Consider the usual denotational sematnics of BitStream, as opposed to the usual operational semantics of it in Haskell? So do you mean that you seek materials for teaching denotational semantics? |
| 2026-01-15 21:52:36 | <jreicher> | I'm just after anything that will prove (without question-begging assertions) that BitStream is uncountable. It looks entirely countable to me. |
| 2026-01-15 21:52:47 | <EvanR> | what makes you say that |
| 2026-01-15 21:53:29 | <jreicher> | I've already explained. The "recursion" of the construction is infinite, but all the things constructed are finite. So you don't get diagonalisation. |
| 2026-01-15 21:53:41 | <EvanR> | I don't follow... |
| 2026-01-15 21:53:53 | <EvanR> | all things constructed are finite? |
| 2026-01-15 21:54:02 | <monochrom> | Well here goes shameless plug. This is my lecture notes for this stuff: https://www.cs.utoronto.ca/~trebla/CSCC24-latest/partial-order-recursion.html |
| 2026-01-15 21:54:40 | <dolio> | The type of lazy streams is uncountable. |
| 2026-01-15 21:54:55 | <jreicher> | dolio: reference? I don't see how that would be the case |
| 2026-01-15 21:55:45 | <EvanR> | one way to look at countable A is you can make a [A] which contains at some point all possible A values |
| 2026-01-15 21:55:57 | <EvanR> | possibly infinite |
| 2026-01-15 21:56:02 | <dolio> | https://hub.darcs.net/dolio/unpossible/browse/src/Cantor/Properties.agda#66 |
| 2026-01-15 21:56:13 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 21:56:22 | <jreicher> | EvanR: Take (as a silly example) data SillyType = I SillyType. Countable or uncountable? |
| 2026-01-15 21:56:23 | <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... |
| 2026-01-15 21:56:46 | <jreicher> | monochrom: there aren't any infinite bit strings in the set |
| 2026-01-15 21:56:47 | <monochrom> | SillyType is countable. |
| 2026-01-15 21:56:54 | <EvanR> | jreicher, is the only (respectable) value here I (I (I (I ...)))? |
| 2026-01-15 21:56:59 | <EvanR> | so cardinalty 1 |
| 2026-01-15 21:57:12 | <jreicher> | monochrom: Exactly. So making it a "binary choice" recursion doesn't magically make it uncountable |
| 2026-01-15 21:57:57 | <monochrom> | You need infinite strings for completeness. |
| 2026-01-15 21:58:18 | <EvanR> | there's no finite strings by design, so I'm confused by that |
| 2026-01-15 21:58:52 | <monochrom> | The increasing sequence I bottom, I (I bottom), I (I (I bottom)) ... needs a least upper bound. |
| 2026-01-15 21:58:55 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 240 seconds) |
| 2026-01-15 21:59:40 | <jreicher> | monochrom: My only point is that none of these recursive datatypes give you infinite strings. |
| 2026-01-15 21:59:48 | <jreicher> | You have an infinite series of finite strings |
| 2026-01-15 21:59:58 | <EvanR> | I guess including all these partially defined possibilities is making it even more infinite |
| 2026-01-15 22:00:10 | EvanR | looks at jreicher |
| 2026-01-15 22:00:25 | <int-e> | . o O ( it must be nice to have convictions ) |
| 2026-01-15 22:00:53 | <dolio> | > cycle [0,1] |
| 2026-01-15 22:00:54 | <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 22:01:01 | <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 22:01:08 | <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 22:01:52 | <monochrom> | I can respect that you reject denotational semantics altogether, but then you should also be rejecting "bottom". |
| 2026-01-15 22:02:17 | <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 22:02:25 | <int-e> | But how can you discuss countability in a finitist context? :P |
| 2026-01-15 22:02:30 | <monochrom> | OK sure. Read my lecture notes first? |
| 2026-01-15 22:02:39 | <jreicher> | I'm not finitist. I just said infinite series of finite objects. |
| 2026-01-15 22:02:48 | <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 22:02:58 | <EvanR> | jreicher, good xD |
| 2026-01-15 22:03:22 | <int-e> | (I can defend the idea that streams are countable but it'll involve computability and/or Scott domains) |
| 2026-01-15 22:03:29 | <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 22:03:46 | <EvanR> | or definability, because you have to write the code, and code is countable |
| 2026-01-15 22:03:54 | × | Inline quits (~User@cgn-195-14-218-118.nc.de) (Quit: KVIrc 5.2.6 Quasar http://www.kvirc.net/) |
| 2026-01-15 22:04:20 | <EvanR> | (but I might be wrong here beacuse of higher order programs) |
| 2026-01-15 22:04:26 | <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 22:04:52 | <jreicher> | I have to think this through carefully, but I think you are all accepting the existence of infinitely-running programs? |
| 2026-01-15 22:05:09 | <EvanR> | sounds like operational semantics |
| 2026-01-15 22:05:11 | <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 22:05:23 | <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 22:05:51 | <dolio> | Viewed externally as built in classical mathematics, that is the statement, 'the set of recursive bit streams is "computably uncountable."' |
| 2026-01-15 22:06:03 | <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 22:06:21 | <dolio> | I.E. given a computable enumeration of computable bit streams, one can compute a bit stream not in the enumeration. |
| 2026-01-15 22:06:25 | <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 22:07:00 | <EvanR> | you're trying to say like > repeat 'a' is not an infinite list |
| 2026-01-15 22:07:04 | <EvanR> | in haskell xD |
| 2026-01-15 22:07:09 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 22:07:25 | <int-e> | it's a very finite graph :P |
| 2026-01-15 22:07:32 | <int-e> | (once fully evaluated) |
| 2026-01-15 22:07:39 | <EvanR> | in ghc! |
| 2026-01-15 22:07:46 | <EvanR> | if you're lucky |
| 2026-01-15 22:07:56 | <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) |
All times are in UTC.