Newest at the top
| 2024-04-19 20:10:33 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-04-19 20:06:36 +0200 | xdminsy | (~xdminsy@117.147.70.233) (Remote host closed the connection) |
| 2024-04-19 20:00:06 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) (Ping timeout: 252 seconds) |
| 2024-04-19 19:51:19 +0200 | elbear | (~lucian@79.118.150.93) (Ping timeout: 268 seconds) |
| 2024-04-19 19:50:21 +0200 | <tomsmeding> | dolio: I see :) |
| 2024-04-19 19:48:47 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-04-19 19:47:23 +0200 | <dolio> | The more rigorous Martin-löf type theory is similarly inadequate. It basically only works for inductive definitions (in its sense, which does not match Haskell's). |
| 2024-04-19 19:45:08 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-19 19:45:07 +0200 | Etabeta1 | (~Etabeta1@151.30.10.212) |
| 2024-04-19 19:42:30 +0200 | philopsos | (~caecilius@user/philopsos) (Ping timeout: 252 seconds) |
| 2024-04-19 19:41:39 +0200 | paddymahoney | (~paddymaho@pool-99-250-26-190.cpe.net.cable.rogers.com) |
| 2024-04-19 19:40:21 +0200 | <monochrom> | :) |
| 2024-04-19 19:40:13 +0200 | <ncf> | it's a HoTT take &c |
| 2024-04-19 19:39:45 +0200 | <dolio> | That's not a hot take. :þ |
| 2024-04-19 19:38:42 +0200 | <ncf> | or sometimes what reference means |
| 2024-04-19 19:37:37 +0200 | <monochrom> | Hot take: Equality is hard. When you see people disagreeing on what referential transparency means, you can trace it all the way back to only disagreeing on what equality means. |
| 2024-04-19 19:35:10 +0200 | <monochrom> | But OK I'm nobody, it doesn't matter. :( :) |
| 2024-04-19 19:34:55 +0200 | <monochrom> | I use ":=" for definitions. |
| 2024-04-19 19:33:39 +0200 | Etabeta1 | (~Etabeta1@user/meow/Etabeta1) (Quit: quit) |
| 2024-04-19 19:32:37 +0200 | <dolio> | Cubical Agda is not so deficient. |
| 2024-04-19 19:32:37 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) |
| 2024-04-19 19:32:30 +0200 | <dolio> | tomsmeding: Normal Agda lacks the ability to prove qualities about coinductive definitions by means other than how their definitions reduce. So it's inappropriate to consider what you could prove in normal Agda as a proxy for what you could prove using the principles that people accept for Haskell. |
| 2024-04-19 19:31:47 +0200 | <ncf> | so in summary syntax is awful and whatever you pick is fine |
| 2024-04-19 19:31:30 +0200 | <ncf> | there's also the whole confusion of sometimes = meaning definitional and ≡ meaning propositional equality and sometimes the opposite |
| 2024-04-19 19:30:25 +0200 | tri | (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 2024-04-19 19:29:47 +0200 | troydm | (~troydm@user/troydm) |
| 2024-04-19 19:26:51 +0200 | troydm | (~troydm@user/troydm) (Quit: What is Hope? That all of your wishes and all of your dreams come true? To turn back time because things were not supposed to happen like that (C) Rau Le Creuset) |
| 2024-04-19 19:23:40 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 2024-04-19 19:23:21 +0200 | <ncf> | if == evokes the boolean equality operator, then = could evoke haskell's =, which is not symmetric equality but rather "is defined to be" |
| 2024-04-19 19:17:03 +0200 | <ski> | (also because they're also supposed to hold, even if there's no `Eq' instance for the type in question) |
| 2024-04-19 19:16:10 +0200 | <ski> | "the equalities in type class laws need not be decidable" -- which is why it annoys me when people write `==' for them (or `===', for that matter, why not simply use `=', what's wrong with that ?) |
| 2024-04-19 19:08:53 +0200 | ski | (~ski@ext-1-033.eduroam.chalmers.se) |
| 2024-04-19 19:03:17 +0200 | ski | (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 272 seconds) |
| 2024-04-19 19:00:04 +0200 | <ncf> | you can prove streams equivalent to functions out of ℕ and transport equality proofs from that (which would usually come from function extensionality), or you might define some sort of bisimilarity relation and either postulate it to imply equality or work in a type theory where it already is (like cubical type theory) |
| 2024-04-19 18:57:38 +0200 | <tomsmeding> | given the words they've used so far, it sounds like dolio knows more about this :) |
| 2024-04-19 18:57:20 +0200 | <tomsmeding> | e.g. agda |
| 2024-04-19 18:57:16 +0200 | <tomsmeding> | masaeedu: right. I'm no expert here, but I think in a type theory with coinduction, you can actually prove certain propositional equalities on streams |
| 2024-04-19 18:52:44 +0200 | jinsun | (~jinsun@user/jinsun) (Ping timeout: 268 seconds) |
| 2024-04-19 18:48:42 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) |
| 2024-04-19 18:48:34 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) (Client Quit) |
| 2024-04-19 18:47:06 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) |
| 2024-04-19 18:46:13 +0200 | cawfee | (~root@2406:3003:2077:1c50::babe) (Quit: WeeChat 4.2.2) |
| 2024-04-19 18:45:07 +0200 | vpan | (~vpan@212.117.1.172) (Quit: Leaving.) |
| 2024-04-19 18:38:28 +0200 | mcksp | (~mcksp@host2.98.gci-net.pl) (Quit: Client closed) |
| 2024-04-19 18:37:33 +0200 | <EvanR> | refl : a = a |
| 2024-04-19 18:37:04 +0200 | <EvanR> | the equality type from martin lof type theory is for proving terms to be equal, before you interpret anything |
| 2024-04-19 18:36:29 +0200 | <masaeedu> | tomsmeding: i interpret the =s in typeclass laws as propositional equality. in Haskell, i prove the propositions only on paper |
| 2024-04-19 18:35:38 +0200 | <EvanR> | sounds like you're using a specific interpretation |
| 2024-04-19 18:35:05 +0200 | <EvanR> | masaeedu, skipping everything from the last 30 minues because I was away, I wasn't talking about proving procedures equal |
| 2024-04-19 18:34:55 +0200 | billchenchina | (~billchenc@103.118.42.229) (Remote host closed the connection) |