Newest at the top
| 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) |
| 2024-04-19 18:32:06 +0200 | <probie> | masaeedu: Just so we're on the same page, are you claiming that it can't be proven that `map (*2) [1..]` is equal to `[2,4..]`? |
| 2024-04-19 18:30:46 +0200 | <raehik> | it should also keep the intermediate type leaner (probably...) |
| 2024-04-19 18:30:16 +0200 | <raehik> | tomsmeding: thanks. I'm doing type level string stuff, and I think UnconsSymbol-ing earlier lets me pack more into a single equation |
| 2024-04-19 18:30:08 +0200 | <masaeedu> | there's a lot of talking about decidable equality above, about which i've said nothing |
| 2024-04-19 18:30:08 +0200 | <tomsmeding> | masaeedu: what's your interpretation of the '=' sign in type class laws? |
| 2024-04-19 18:29:46 +0200 | <dolio> | But that's no reason to enshrine a bad version of reasoning about coinductive types. |
| 2024-04-19 18:29:35 +0200 | <masaeedu> | it isn't |
| 2024-04-19 18:29:30 +0200 | <tomsmeding> | they do, but that's mostly tangential to the point |
| 2024-04-19 18:29:27 +0200 | <masaeedu> | yes |
| 2024-04-19 18:29:20 +0200 | <dolio> | At least if you have eta rules. |
| 2024-04-19 18:29:04 +0200 | <dolio> | The monad laws for functions actually hold judgmentally. |
| 2024-04-19 18:26:43 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:53fc:42ca:b6e5:7849) (Remote host closed the connection) |
| 2024-04-19 18:26:25 +0200 | <tomsmeding> | that's more likely to be large intermediate types |
| 2024-04-19 18:26:08 +0200 | <tomsmeding> | though I think checking the equations is not the bottleneck |
| 2024-04-19 18:25:56 +0200 | <tomsmeding> | raehik: top-to-bottom: yes; not sure how inlining reduces the number of equations, but if you can reduce the number of equations, then probably yes |
| 2024-04-19 18:25:48 +0200 | billchenchina- | (~billchenc@2408:8453:6420:23d9:e5d8:b8f7:4bdc:c818) (Ping timeout: 260 seconds) |
| 2024-04-19 18:25:09 +0200 | <tomsmeding> | and if you don't think this counter-argument is convincing: if you reject monad laws on streams, then you must also reject the monad laws for the reader monad -- because apart from performance, Stream and ((->) Natural) are equivalent |
| 2024-04-19 18:25:05 +0200 | <raehik> | Closed type families are evaluated top-to-bottom, right? So if I can "inline" calls to other type families (e.g. UnconsSymbol) and reduce the number of equations, will that make GHC evaluate faster? |
| 2024-04-19 18:24:13 +0200 | billchenchina | (~billchenc@103.118.42.229) |
| 2024-04-19 18:23:23 +0200 | <tomsmeding> | if you can't, then, well, you haven't proved that you have a lawful monad instance :) |
| 2024-04-19 18:23:05 +0200 | <tomsmeding> | if you say that your monad instance is valid because the streams are equal even if the generating functions are different, fine -- if you can show that the streams that those functions generate are equal, then you're all set |
| 2024-04-19 18:22:28 +0200 | <tomsmeding> | but that's not surprising |
| 2024-04-19 18:22:26 +0200 | <tomsmeding> | you will need to write this proof on paper or in a proof assistant, and you will not be able to exhaustively check that the laws hold at runtime |
| 2024-04-19 18:22:02 +0200 | <tomsmeding> | if you write a Monad instance for Stream, it is up to you to write a proof that the laws hold, i.e. that a bunch of streams are indeed equal |
| 2024-04-19 18:22:02 +0200 | <masaeedu> | you can certainly show that the generating equation for certain streams are equal, but this is too restrictive to model anything approaching equality |
| 2024-04-19 18:21:46 +0200 | <masaeedu> | let me paste the first sentence again |
| 2024-04-19 18:21:31 +0200 | <dolio> | Stream equality isn't equality of their generating functions. |
| 2024-04-19 18:21:27 +0200 | <tomsmeding> | that is not a problem |
| 2024-04-19 18:21:21 +0200 | <tomsmeding> | sure |
| 2024-04-19 18:21:15 +0200 | <masaeedu> | many streams that we would expect to be "equal" intuitively have distinct generating functions |
| 2024-04-19 18:20:58 +0200 | <masaeedu> | tomsmeding: i don't think you're quite thinking through what the restriction means |
| 2024-04-19 18:20:31 +0200 | billchenchina | (~billchenc@58.20.40.49) (Ping timeout: 246 seconds) |