Newest at the top
| 2024-04-19 21:42:59 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-04-19 21:42:44 +0200 | <tomsmeding> | probie: definitional, going by what they've said so far |
| 2024-04-19 21:42:01 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-04-19 21:41:57 +0200 | <probie> | masaeedu: Normally I'm used to people talking about leibniz equality if they haven't explicitly specified a definition. Those two things are definitely leibniz equal (assuming functional extensionality). What is your definition of equality? |
| 2024-04-19 21:40:00 +0200 | <ncf> | true |
| 2024-04-19 21:38:59 +0200 | <dolio> | Haskell doesn't need them to say the type is meant to be a quotient when you're reasoning about it. |
| 2024-04-19 21:38:59 +0200 | <monochrom> | Right for example Data.Set binary search trees. |
| 2024-04-19 21:37:54 +0200 | <ncf> | haskell needs quotient inductive types |
| 2024-04-19 21:37:16 +0200 | <dolio> | So the appropriate equality incorporates that. |
| 2024-04-19 21:36:34 +0200 | <ncf> | right |
| 2024-04-19 21:36:18 +0200 | <dolio> | If I import some .Internals module, I can tell the difference between abstract structures. Or maybe there is no technical barrier to telling them apart, but I am meant to not care about some differences in representation. |
| 2024-04-19 21:35:15 +0200 | <ncf> | dolio: do you have an example? |
| 2024-04-19 21:34:25 +0200 | <dolio> | Sometimes even observational (in Haskell) equality is not appropriate. |
| 2024-04-19 21:33:38 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 2024-04-19 21:31:48 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-04-19 21:30:44 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) (Remote host closed the connection) |
| 2024-04-19 21:30:10 +0200 | <monochrom> | No, like I said, the problem does not exist in Haskell because we use denotational equality here, even generally mathematical equality. |
| 2024-04-19 21:30:08 +0200 | <tomsmeding> | anything I would want to use typeclass laws for would be about observational equality |
| 2024-04-19 21:29:22 +0200 | <masaeedu> | the problem exists in both Haskell in Agda, assuming the laws actually mean anything and you're actually trying to prove what you claim in the typeclass laws |
| 2024-04-19 21:29:17 +0200 | akshar | (~user@209.94.142.169) |
| 2024-04-19 21:29:15 +0200 | <monochrom> | Or rather, why would one restrict oneself to definitional equality, then bolt on codata, then also throw up hands and declare "nothing can be proved about codata" and so it is all a waste of time? |
| 2024-04-19 21:28:33 +0200 | <tomsmeding> | in agda you might, because there one cares about what the type checker can automaticall reduce for you and what it cannot |
| 2024-04-19 21:28:11 +0200 | <monochrom> | Why would one restrict onself to definitional equality? |
| 2024-04-19 21:27:11 +0200 | <monochrom> | To a large extent, I am betting on: 1. No one dares to contrive a denotational semantics that distinguish coding styles; 2. No one bothers to contrive a denotational semantics that distinguish time/space complexity. |
| 2024-04-19 21:26:59 +0200 | <tomsmeding> | not about a proof assistant where we care a lot about what holds definitionally and what does not |
| 2024-04-19 21:26:39 +0200 | <tomsmeding> | masaeedu: we're talking about haskell, right? |
| 2024-04-19 21:26:26 +0200 | <tomsmeding> | yes I'm not arguing against you, just calibrating my understanding of the terminology |
| 2024-04-19 21:26:22 +0200 | <masaeedu> | tomsmeding: you seem to be imagining "observational equality" as some kind of drop in substitute for definitional equality. it doesn't really work like that |
| 2024-04-19 21:25:33 +0200 | <monochrom> | Fortunately even then all existing choices agree on infinite lists. |
| 2024-04-19 21:25:25 +0200 | <tomsmeding> | right, then I still understand things :) |
| 2024-04-19 21:25:06 +0200 | <monochrom> | We only have the (or one of several) intuitively reasonable one. :) |
| 2024-04-19 21:24:29 +0200 | <tomsmeding> | (doesn't this depend on what denotational semantics you assign to Haskell? Are we assuming the intuitively reasonable one, or a specific formalised one?) |
| 2024-04-19 21:24:04 +0200 | <monochrom> | Fortunately if you gross over computational complexity, "denotation" and "observation" are, um, observationally equal >:) |
| 2024-04-19 21:23:00 +0200 | <monochrom> | But given that a lot of people haven't heard of that, observation will have to do as a proxy. |
| 2024-04-19 21:22:29 +0200 | <monochrom> | In the Haskell community you are supposed to eventually pick up the implicit convention that laws in type classes use denotational equality not C programmer equality. |
| 2024-04-19 21:21:33 +0200 | <Franciman> | nice |
| 2024-04-19 21:21:31 +0200 | <Franciman> | I must leave, so i give up. I'll read the answer tho! |
| 2024-04-19 21:21:06 +0200 | <Franciman> | maybe for this codata it's more indirectly applicable |
| 2024-04-19 21:20:55 +0200 | <monochrom> | Eventually I will be advocating for denotational equality/inequality but yeah. |
| 2024-04-19 21:20:35 +0200 | <Franciman> | it's the confluence theorem no? |
| 2024-04-19 21:20:29 +0200 | <Franciman> | uhm, if they both terminate they can't different answers |
| 2024-04-19 21:20:12 +0200 | <tomsmeding> | (absent unsafePerformIO and precise performance measurement, but that's surely outside the realm of reasoning here) |
| 2024-04-19 21:19:33 +0200 | <monochrom> | I would hope both terminate. But I posit that you can't get two different answers. |
| 2024-04-19 21:18:18 +0200 | <Franciman> | if there is a context where the two lambda terms don't both terminate |
| 2024-04-19 21:17:59 +0200 | <Franciman> | ok so you mean |
| 2024-04-19 21:17:45 +0200 | <monochrom> | I'm OK with re-negotiation those terms, but let's start somewhere. |
| 2024-04-19 21:17:42 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-19 21:17:09 +0200 | <monochrom> | Perhaps even restrict f :: [Integer] -> Bool as a first attempt. |
| 2024-04-19 21:16:38 +0200 | <monochrom> | Franciman: There are many ways to convey the meaning. Perhaps we can start with: Write a function f such that f (map (2*) [1..]) gives a different answer from f [2, 4, ..]. |
| 2024-04-19 21:16:16 +0200 | tremon | (~tremon@83.80.159.219) |