Newest at the top
| 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. |
| 2026-01-15 22:47:03 +0100 | <monochrom> | Not even when that someone is me. I don't bother to write a paper for that. |
| 2026-01-15 22:46:53 +0100 | <EvanR> | if you disagree that haskell has uncountable datatypes, it's possible normal set theory also doesn't xD |
| 2026-01-15 22:46:37 +0100 | <monochrom> | I don't have a reference. |
| 2026-01-15 22:46:06 +0100 | <jreicher> | monochrom: got a reference? That doesn't sound sensible to me |
| 2026-01-15 22:44:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-15 22:43:44 +0100 | <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 22:41:52 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 22:41:35 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 22:40:00 +0100 | <davean> | dolio: I just don't recally how they define their boundary |
| 2026-01-15 22:39:45 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:35:48 +0100 | <dolio> | Maybe not super surprised. |
| 2026-01-15 22:35:27 +0100 | <EvanR> | of the values |
| 2026-01-15 22:35:17 +0100 | <EvanR> | i.e. make a full list of them |
| 2026-01-15 22:35:03 +0100 | <EvanR> | datatypes which could not possibly be enumerated (in haskell) |
| 2026-01-15 22:35:02 +0100 | <jreicher> | I can't see how it's possible. You only get countable infinities with recursion. |
| 2026-01-15 22:35:01 +0100 | <dolio> | I'd be a little surprised if the lexing were undecidable, but I'm not much of a C++ guru. |
| 2026-01-15 22:34:32 +0100 | <EvanR> | are you sure we don't already? |
| 2026-01-15 22:34:21 +0100 | <jreicher> | Not sure we want uncountable datatypes in Haskell |
| 2026-01-15 22:33:54 +0100 | peterbecich | (~Thunderbi@71.84.33.135) peterbecich |
| 2026-01-15 22:33:48 +0100 | <EvanR> | you could make the case to come up with semantics to mediate between haskell and set theory if that was relevant, but it's often not xD |
| 2026-01-15 22:33:39 +0100 | <jreicher> | And also "personally" |
| 2026-01-15 22:33:30 +0100 | <jreicher> | That's why I used the word "unhygienic". |
| 2026-01-15 22:33:18 +0100 | <EvanR> | this is a bit too dogmatic |
| 2026-01-15 22:33:11 +0100 | <davean> | dolio: I forget exactly which level of lex vs. parse is undecidable |
| 2026-01-15 22:32:58 +0100 | <jreicher> | Personally I think it's unhygienic to talk about a logistic language as a logic. A logic is a logic when it's used for proof, and so it can only be a metalanguage. But because it is a formal system it can be "reflected" as a language, but when that's done it shouldn't be called a logic (in my opinion) |
| 2026-01-15 22:32:42 +0100 | <dolio> | davean: lexing? |
| 2026-01-15 22:32:18 +0100 | <monochrom> | Why do we even care about traditional set theory in #haskell? :) |
| 2026-01-15 22:32:07 +0100 | <davean> | dolio: C++ is undecidable |
| 2026-01-15 22:31:58 +0100 | <monochrom> | Oh, the original language was Haskell. |
| 2026-01-15 22:31:35 +0100 | <monochrom> | (Generally in any CoC + user-definable inductive types.) |
| 2026-01-15 22:31:20 +0100 | <jreicher> | monochrom: yes, and so that's a different kind of language. It all depends on how you understand the original question about "where" in the language comparison "operators" are |
| 2026-01-15 22:31:01 +0100 | <monochrom> | In Agda, Lean, and Haskell, T and F are even user-definable. |
| 2026-01-15 22:30:29 +0100 | <EvanR> | ok then we can reel it back in and have T an F just be haskell T and F |
| 2026-01-15 22:30:26 +0100 | <monochrom> | HoTT, CoC, Agda, Lean, Haskell all have T and F in the language domain. |
| 2026-01-15 22:30:09 +0100 | <jreicher> | Except I'm not a platonist. :p |
| 2026-01-15 22:29:58 +0100 | <EvanR> | you might have spontaneously created a new platonic semantics for haskell beyond the ones we already had |
| 2026-01-15 22:29:25 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 22:29:17 +0100 | <jreicher> | Put another way, when the "output" of the "operator" is T or F, those values don't exist in the language domain. They are the semantic values in the metalanguage. |
| 2026-01-15 22:28:40 +0100 | <EvanR> | operator one of the most overloaded terms, in the process also overloading the term operator overloading |
| 2026-01-15 22:27:44 +0100 | <monochrom> | That too. Just look at GHC being written in GHC. |
| 2026-01-15 22:27:40 +0100 | <jreicher> | When we say a comparison "operator" is a predicate, the operator is linguistic, but the predication is metalinguistic. |
| 2026-01-15 22:27:11 +0100 | <EvanR> | it's relative right, you could have two of the same theories one standing for metatheory one for theory but they're the same language |
| 2026-01-15 22:26:42 +0100 | <monochrom> | In fact how about I use HoTT as the metalanguage for defining the language and semantics of set theory? |
| 2026-01-15 22:26:31 +0100 | <jreicher> | Exactly. And to me the original question was about the metalinguistic objects, and not the linguistic ones. |