Newest at the top
| 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... |
| 2026-01-15 22:56:22 +0100 | <jreicher> | EvanR: Take (as a silly example) data SillyType = I SillyType. Countable or uncountable? |
| 2026-01-15 22:56:13 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2026-01-15 22:56:02 +0100 | <dolio> | https://hub.darcs.net/dolio/unpossible/browse/src/Cantor/Properties.agda#66 |
| 2026-01-15 22:55:57 +0100 | <EvanR> | possibly infinite |
| 2026-01-15 22:55:45 +0100 | <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 22:54:55 +0100 | <jreicher> | dolio: reference? I don't see how that would be the case |
| 2026-01-15 22:54:40 +0100 | <dolio> | The type of lazy streams is uncountable. |
| 2026-01-15 22:54:02 +0100 | <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 22:53:53 +0100 | <EvanR> | all things constructed are finite? |
| 2026-01-15 22:53:41 +0100 | <EvanR> | I don't follow... |
| 2026-01-15 22:53:29 +0100 | <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 22:52:47 +0100 | <EvanR> | what makes you say that |
| 2026-01-15 22:52:36 +0100 | <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 22:51:39 +0100 | <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 22:51:37 +0100 | <EvanR> | ignoring bottoms there's no way to make a finite Bitstream |
| 2026-01-15 22:51:21 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:50:56 +0100 | <EvanR> | we're about to jump the shark from uncountability to ultrafinitism |
| 2026-01-15 22:50:44 +0100 | <jreicher> | You can't have an infinite bitstream value |
| 2026-01-15 22:50:31 +0100 | <EvanR> | wat |
| 2026-01-15 22:50:22 +0100 | <jreicher> | Any bitstream value is INDEFINITE length, but it's still FINITE. |
| 2026-01-15 22:50:06 +0100 | <EvanR> | that's .. neither here nor there |
| 2026-01-15 22:49:55 +0100 | <jreicher> | You can't make the diagonalisation from it |
| 2026-01-15 22:49:53 +0100 | <EvanR> | reals? |
| 2026-01-15 22:49:46 +0100 | <jreicher> | Yes, but that datatype is not all the reals |
| 2026-01-15 22:49:28 +0100 | <geekosaur> | that was my thought, it either proves countability or provides a recipe to construct uncountably many values |
| 2026-01-15 22:49:24 +0100 | <EvanR> | it made a lot of people very angry and was generally considered a bad idea |
| 2026-01-15 22:49:09 +0100 | <geekosaur> | ^ |
| 2026-01-15 22:49:00 +0100 | <EvanR> | jreicher, there was this guy cantor with this diagonalization argument |
| 2026-01-15 22:48:32 +0100 | <EvanR> | nothing wrong with definitions |
| 2026-01-15 22:48:27 +0100 | <EvanR> | you define things and then see if this or that satisfies the definition |
| 2026-01-15 22:48:10 +0100 | <jreicher> | EvanR: how is that uncountable? |
| 2026-01-15 22:48:09 +0100 | <monochrom> | Oh it is asserted. Denotational semantics are seldom constructive. |
| 2026-01-15 22:47:58 +0100 | <EvanR> | jreicher, why do you think this xD |
| 2026-01-15 22:47:48 +0100 | <EvanR> | here is one... data Bitstream = I Bitstream | O Bitstream |
| 2026-01-15 22:47:45 +0100 | <jreicher> | Uncountability, in a way, "comes from nowhere". It has to be asserted. You can't constructit. |
| 2026-01-15 22:47:06 +0100 | <jreicher> | I don't disagree. I just can't see how it's possible. |