Newest at the top
| 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. |
| 2026-01-15 22:26:16 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2026-01-15 22:26:10 +0100 | <monochrom> | Traditional mathematics also needs a language and a metalanguage. |
| 2026-01-15 22:26:08 +0100 | <EvanR> | instead of using it for actual purposes xD |
| 2026-01-15 22:25:54 +0100 | <EvanR> | if you're proving things about the logic itself |
| 2026-01-15 22:25:37 +0100 | <jreicher> | Language and metalanguage. |
| 2026-01-15 22:25:28 +0100 | <jreicher> | Yes, but you then have two logics. The logic which is the object of study (proof), and the logic being used to study it (prove things about it). |
| 2026-01-15 22:25:06 +0100 | Everything | (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving) |
| 2026-01-15 22:24:55 +0100 | <dolio> | Type theory has no need of logic. It has subsumed it. |
| 2026-01-15 22:24:53 +0100 | <EvanR> | type theory *is* logic |
| 2026-01-15 22:24:51 +0100 | humasect | (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 22:24:11 +0100 | <jreicher> | I think that mixes up language levels. Type theory itself needs to be written in logic, which means predicates are used to describe it. It will be different predicates that are objects within type theory. |
| 2026-01-15 22:23:57 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 22:23:50 +0100 | <dolio> | 'For every x with multiple related ys, pick one of the ys.' |
| 2026-01-15 22:23:14 +0100 | <monochrom> | In type theory, predicates are special cases of functions. |
| 2026-01-15 22:23:13 +0100 | <dolio> | Yeah, that assertion is equivalent to the axiom of choice. |
| 2026-01-15 22:22:33 +0100 | <dolio> | :) |