Newest at the top
| 2024-04-19 22:13:22 +0200 | <dolio> | (Or even formal reasoning.) |
| 2024-04-19 22:13:03 +0200 | _ht | (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Remote host closed the connection) |
| 2024-04-19 22:10:40 +0200 | <dolio> | But, you know, we don't need to to do informal reasoning about our Haskell code. |
| 2024-04-19 22:09:18 +0200 | <dolio> | Sections 5 and beyond of that paper are actually about how to design a tractable theory that does justify coinduction. |
| 2024-04-19 22:07:27 +0200 | peutri | (~peutri@bobo.desast.re) |
| 2024-04-19 22:07:18 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 22:07:18 +0200 | peutri | (~peutri@bobo.desast.re) (Ping timeout: 256 seconds) |
| 2024-04-19 22:07:17 +0200 | lyxia | (~lyxia@poisson.chat) |
| 2024-04-19 22:07:00 +0200 | lyxia | (~lyxia@poisson.chat) (Ping timeout: 260 seconds) |
| 2024-04-19 22:06:17 +0200 | catties | (~catties@user/meow/catties) (Ping timeout: 256 seconds) |
| 2024-04-19 22:06:05 +0200 | Catty | (~catties@user/meow/catties) |
| 2024-04-19 22:05:47 +0200 | Benzi-Junior | (~BenziJuni@232-148-209-31.dynamic.hringdu.is) |
| 2024-04-19 22:05:31 +0200 | Benzi-Junior | (~BenziJuni@232-148-209-31.dynamic.hringdu.is) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-04-19 21:58:16 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
| 2024-04-19 21:57:27 +0200 | <monochrom> | Generally trying to say that scaremongering about undecidability is silly. Even extensional equality for functions will get you enough undecidability issues. Well, "issues". |
| 2024-04-19 21:56:56 +0200 | <dolio> | You don't even get the point-wise version by definition, usually. |
| 2024-04-19 21:56:04 +0200 | <ncf> | see https://proofassistants.stackexchange.com/questions/1885/strong-eta-rules-for-functions-on-sum-types |
| 2024-04-19 21:55:51 +0200 | <ncf> | you could if you had both eta for functions and for booleans, but i think the latter is problematic |
| 2024-04-19 21:55:36 +0200 | <dolio> | Usually that is not included, no. |
| 2024-04-19 21:55:31 +0200 | <monochrom> | At best you can prove "forall x. (not . not) x = id x" but you can't make the extensional leap. |
| 2024-04-19 21:55:10 +0200 | tremon | (~tremon@83.80.159.219) (Quit: getting boxed in) |
| 2024-04-19 21:55:01 +0200 | <monochrom> | Am I even wrong to assert that under the restriction of definitional equality you can't even prove not . not = id? |
| 2024-04-19 21:51:54 +0200 | <monochrom> | I am not sure that inductive data are free of undecidable problems either. |
| 2024-04-19 21:49:43 +0200 | <ncf> | or do you mean another part of this? |
| 2024-04-19 21:49:36 +0200 | <monochrom> | If you add a feature, you've got to axiomatize useful proof techniques for it. |
| 2024-04-19 21:49:29 +0200 | <ncf> | sounds like maybe you *were* talking about decidability after all? |
| 2024-04-19 21:49:21 +0200 | <ncf> | » By transitivity, a complete de- cision procedure for ≡ must find the intermediate value for itself, effectively solving the halting problem. Hence it does not exist. |
| 2024-04-19 21:49:00 +0200 | <monochrom> | I am saying that if you take the stance of "let's add a feature, but oh you can't prove shit when people actually use that feature, it's UB", then you may like the C standard committee. |
| 2024-04-19 21:48:13 +0200 | <masaeedu> | sure. a good starting point is: http://strictlypositive.org/ObsCoin.pdf |
| 2024-04-19 21:48:11 +0200 | <monochrom> | I am not a problems guy when people don't talk about solutions instead. |
| 2024-04-19 21:47:41 +0200 | <ncf> | can you name a paper? |
| 2024-04-19 21:46:56 +0200 | <masaeedu> | i'm not strongly motivated enough to continue debating this, but for anyone interested in actually learning something about the problems involved in equality proofs on codata, i strongly recommend Conor McBride's writing on the subject |
| 2024-04-19 21:46:50 +0200 | <ph88> | dmj`, https://abhiroop.github.io/vectorization.pdf |
| 2024-04-19 21:45:43 +0200 | ph88 | (~ph88@ip5b403f30.dynamic.kabel-deutschland.de) |
| 2024-04-19 21:44:38 +0200 | notzmv | (~daniel@user/notzmv) (Read error: Connection reset by peer) |
| 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) |