Logs: liberachat/#haskell
| 2026-01-15 20:30:37 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 2026-01-15 20:30:56 | × | collide2954 quits (~collide29@user/collide2954) (Quit: The Lounge - https://thelounge.chat) |
| 2026-01-15 20:31:43 | → | collide2954 joins (~collide29@user/collide2954) |
| 2026-01-15 20:36:01 | <dolio> | davean: Does C++ do that, too? I thought that was perl's distinction. |
| 2026-01-15 20:36:21 | <dolio> | I guess perl has to actually evaluate code. |
| 2026-01-15 20:37:42 | <davean> | dolio: https://blog.reverberate.org/2013/08/parsing-c-is-literally-undecidable.html "C++ grammar: the type name vs object name issue" and others |
| 2026-01-15 20:38:47 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 20:40:35 | × | divlamir quits (~divlamir@user/divlamir) (Ping timeout: 240 seconds) |
| 2026-01-15 20:41:03 | → | humasect joins (~humasect@dyn-192-249-132-90.nexicom.net) |
| 2026-01-15 20:42:11 | <dolio> | Anyhow, as I said, Haskell can take it to the next level by making lexing undecidable. |
| 2026-01-15 20:42:23 | <dolio> | That's innovation. |
| 2026-01-15 20:42:25 | <humasect> | yeah |
| 2026-01-15 20:42:52 | → | divlamir joins (~divlamir@user/divlamir) |
| 2026-01-15 20:42:59 | <monochrom> | TypeDirectedLexicalResolution? >:) |
| 2026-01-15 20:43:35 | → | jreicher joins (~joelr@user/jreicher) |
| 2026-01-15 20:43:37 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 256 seconds) |
| 2026-01-15 20:43:37 | → | Enrico63 joins (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) |
| 2026-01-15 20:46:01 | <[exa]> | -XLexicalKinds |
| 2026-01-15 20:46:48 | × | Enrico63 quits (~Enrico63@2001:b07:646b:5fed:9efc:e8ff:fe24:3213) (Client Quit) |
| 2026-01-15 20:49:50 | × | peterbecich quits (~Thunderbi@71.84.33.135) (Ping timeout: 256 seconds) |
| 2026-01-15 20:50:21 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 20:51:08 | <jreicher> | thenightmail: I'm fairly sure in mathematics the comparison "operators" are not operators at all. In algebra an operator on a set produces another element from the same set. Comparison, on the other hand, is a predicate. |
| 2026-01-15 20:52:58 | <c_wraith> | > LT `compare` GT |
| 2026-01-15 20:52:59 | <lambdabot> | LT |
| 2026-01-15 20:53:03 | <c_wraith> | it's closed! |
| 2026-01-15 20:53:04 | × | trickard_ quits (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 20:54:35 | <jreicher> | monochrom: a function is a relation, but the converse is not true |
| 2026-01-15 20:55:31 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 20:55:46 | → | trickard_ joins (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 21:01:25 | <EvanR> | you can get a relation for any function, then functions don't need to be implemented as literal relations if you don't want them to be! |
| 2026-01-15 21:01:55 | <int-e> | "in mathematics" - there is no such thing really; mathematicians will take whatever view is most convenient in a context. In classical logic, predicates can and will be used as functions. Logicians who want to allow logics without the law of excluded middle will disagree. |
| 2026-01-15 21:02:54 | <int-e> | First-order logic has many-sorted variants. There are algebras with more than one carrier set and operators that aren't homogenous either, like vector spaces. |
| 2026-01-15 21:03:35 | <EvanR> | math entities are a pure construction of the mind |
| 2026-01-15 21:03:49 | <EvanR> | :D |
| 2026-01-15 21:04:33 | <EvanR> | how concepts interrelate is more interesting than "what they are really" |
| 2026-01-15 21:04:49 | <EvanR> | sometimes taking the place of |
| 2026-01-15 21:06:56 | <dolio> | jreicher: But does every relation contain a function? |
| 2026-01-15 21:07:38 | <EvanR> | you can get a relation for any function also lets you avoid subtyping |
| 2026-01-15 21:08:39 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 21:09:22 | <dolio> | jreicher: Also, relations are functions in that they are maps into a collection of truth values. |
| 2026-01-15 21:09:49 | <dolio> | Not that every relation from A to B is a function from A to B. |
| 2026-01-15 21:12:07 | <jreicher> | dolio: I'm not sure what you mean by "contain", but I'm fairly sure the answer will be "no", regardless of what meaning you choose. |
| 2026-01-15 21:12:55 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds) |
| 2026-01-15 21:13:19 | → | Lears joins (~Leary@user/Leary/x-0910699) |
| 2026-01-15 21:13:26 | <jreicher> | int-e: I suspect you underestimate the significance of "most convenient". Mathematical definitions are language design in much the same way that programming languages are designed. So if a mathematician says something is "convenient", it means it's a good design. And mathematicians have been working on this much longer than computer scientists. |
| 2026-01-15 21:13:40 | <dolio> | It means there's a sub-relation that is a function. |
| 2026-01-15 21:14:14 | <jreicher> | dolio: And what do you mean by sub-relation? Does it also mean restricting the domain to a subset? |
| 2026-01-15 21:14:35 | × | Leary quits (~Leary@user/Leary/x-0910699) (Ping timeout: 240 seconds) |
| 2026-01-15 21:15:09 | <dolio> | No, R is a sub-relation of S if R(x,y) implies S(x,y) forall x and y. |
| 2026-01-15 21:15:28 | Lears | is now known as Leary |
| 2026-01-15 21:16:18 | <dolio> | I guess, you should be able to restrict the domain, too. |
| 2026-01-15 21:16:32 | <dolio> | Otherwise you could only hope to get a partial function in general. |
| 2026-01-15 21:17:26 | <jreicher> | Yes partial functions will definitely happen. But maybe we can accept those. The bigger problem is that if there are many y for a given x for which S(x,y) then a sub relation that is a function will not really resemble S in any meaningful way |
| 2026-01-15 21:19:37 | <monochrom> | jreicher: I am clearly siding with type theory rather than traditional mathematics. |
| 2026-01-15 21:22:20 | <monochrom> | dolio: To obtain a functional subrelation from a relation with an infinite co-domain, we quickly run into the axiom of choice... :) |
| 2026-01-15 21:22:32 | <jreicher> | monochrom: what do you mean? |
| 2026-01-15 21:22:33 | <dolio> | :) |
| 2026-01-15 21:23:13 | <dolio> | Yeah, that assertion is equivalent to the axiom of choice. |
| 2026-01-15 21:23:14 | <monochrom> | In type theory, predicates are special cases of functions. |
| 2026-01-15 21:23:50 | <dolio> | 'For every x with multiple related ys, pick one of the ys.' |
| 2026-01-15 21:23:57 | → | merijn joins (~merijn@host-cl.cgnat-g.v4.dfn.nl) |
| 2026-01-15 21:24:11 | <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 21:24:51 | × | humasect quits (~humasect@dyn-192-249-132-90.nexicom.net) (Quit: Leaving...) |
| 2026-01-15 21:24:53 | <EvanR> | type theory *is* logic |
| 2026-01-15 21:24:55 | <dolio> | Type theory has no need of logic. It has subsumed it. |
| 2026-01-15 21:25:06 | × | Everything quits (~Everythin@172-232-54-192.ip.linodeusercontent.com) (Quit: leaving) |
| 2026-01-15 21:25:28 | <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 21:25:37 | <jreicher> | Language and metalanguage. |
| 2026-01-15 21:25:54 | <EvanR> | if you're proving things about the logic itself |
| 2026-01-15 21:26:08 | <EvanR> | instead of using it for actual purposes xD |
| 2026-01-15 21:26:10 | <monochrom> | Traditional mathematics also needs a language and a metalanguage. |
| 2026-01-15 21:26:16 | → | pavonia joins (~user@user/siracusa) |
| 2026-01-15 21:26:31 | <jreicher> | Exactly. And to me the original question was about the metalinguistic objects, and not the linguistic ones. |
| 2026-01-15 21:26:42 | <monochrom> | In fact how about I use HoTT as the metalanguage for defining the language and semantics of set theory? |
| 2026-01-15 21:27:11 | <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 21:27:40 | <jreicher> | When we say a comparison "operator" is a predicate, the operator is linguistic, but the predication is metalinguistic. |
| 2026-01-15 21:27:44 | <monochrom> | That too. Just look at GHC being written in GHC. |
| 2026-01-15 21:28:40 | <EvanR> | operator one of the most overloaded terms, in the process also overloading the term operator overloading |
| 2026-01-15 21:29:17 | <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 21:29:25 | × | merijn quits (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-15 21:29:58 | <EvanR> | you might have spontaneously created a new platonic semantics for haskell beyond the ones we already had |
| 2026-01-15 21:30:09 | <jreicher> | Except I'm not a platonist. :p |
| 2026-01-15 21:30:26 | <monochrom> | HoTT, CoC, Agda, Lean, Haskell all have T and F in the language domain. |
| 2026-01-15 21:30:29 | <EvanR> | ok then we can reel it back in and have T an F just be haskell T and F |
| 2026-01-15 21:31:01 | <monochrom> | In Agda, Lean, and Haskell, T and F are even user-definable. |
| 2026-01-15 21:31:20 | <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 21:31:35 | <monochrom> | (Generally in any CoC + user-definable inductive types.) |
| 2026-01-15 21:31:58 | <monochrom> | Oh, the original language was Haskell. |
| 2026-01-15 21:32:07 | <davean> | dolio: C++ is undecidable |
| 2026-01-15 21:32:18 | <monochrom> | Why do we even care about traditional set theory in #haskell? :) |
| 2026-01-15 21:32:42 | <dolio> | davean: lexing? |
| 2026-01-15 21:32:58 | <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 21:33:11 | <davean> | dolio: I forget exactly which level of lex vs. parse is undecidable |
| 2026-01-15 21:33:18 | <EvanR> | this is a bit too dogmatic |
| 2026-01-15 21:33:30 | <jreicher> | That's why I used the word "unhygienic". |
| 2026-01-15 21:33:39 | <jreicher> | And also "personally" |
| 2026-01-15 21:33:48 | <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 21:33:54 | → | peterbecich joins (~Thunderbi@71.84.33.135) |
| 2026-01-15 21:34:21 | <jreicher> | Not sure we want uncountable datatypes in Haskell |
| 2026-01-15 21:34:32 | <EvanR> | are you sure we don't already? |
All times are in UTC.