Newest at the top
| 2025-04-28 01:32:36 +0200 | <monochrom> | Err, ∀r. (Πx:A. B(x) -> r) -> r |
| 2025-04-28 01:32:13 +0200 | <EvanR> | ... not sure |
| 2025-04-28 01:29:14 +0200 | <monochrom> | Do you accept: Encode Σx:A. B(x) as ∀r. Πx:A. B(x) -> r so it is just pi types all over again? :) |
| 2025-04-28 01:25:24 +0200 | sprotte24 | (~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de) (Quit: Leaving) |
| 2025-04-28 01:24:43 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) |
| 2025-04-28 01:21:18 +0200 | <EvanR> | sigma type is a bit more mysterious to me, how do you know someone won't want to use the 2nd component |
| 2025-04-28 01:19:41 +0200 | <EvanR> | just discard the argument |
| 2025-04-28 01:19:29 +0200 | <EvanR> | any call site would need to be adjusted to stop trying to call it like a function |
| 2025-04-28 01:18:01 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 01:16:45 +0200 | j0lol | (~j0lol@132.145.17.236) j0lol |
| 2025-04-28 01:16:37 +0200 | <EvanR> | if the code doesn't use the argument, be it a type or a value, then the body is effectively a constant |
| 2025-04-28 01:16:04 +0200 | Typedfern | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 260 seconds) |
| 2025-04-28 01:12:49 +0200 | typedfern_ | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) typedfern |
| 2025-04-28 01:10:25 +0200 | <haskellbridge> | <loonycyborg> I still have no idea how can you have both pi types and type erasure in the same language. |
| 2025-04-28 01:03:14 +0200 | koz | (~koz@121.99.240.58) (Ping timeout: 244 seconds) |
| 2025-04-28 01:02:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 00:59:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-28 00:50:58 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 00:49:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 00:47:07 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 00:44:31 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-28 00:35:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 00:34:46 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-04-28 00:25:20 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 2025-04-28 00:22:51 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 00:22:00 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-28 00:07:43 +0200 | tromp | (~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2025-04-28 00:05:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 seconds) |
| 2025-04-28 00:04:20 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 00:02:47 +0200 | <davean> | I have no idea if anyone has done serious work on dragging that information along though ... |
| 2025-04-28 00:02:17 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2025-04-28 00:01:46 +0200 | <davean> | since it sorta drags providence along with it. |
| 2025-04-28 00:00:57 +0200 | <davean> | I think the dependent version lets you use information a bit further away than Haskell does. |
| 2025-04-28 00:00:24 +0200 | j0lol | (~j0lol@132.145.17.236) (Ping timeout: 276 seconds) |
| 2025-04-27 23:58:12 +0200 | <davean> | We get it in Haskell beyond just what is in the type because of conditionals use for other purposes that overlap, etc. |
| 2025-04-27 23:57:46 +0200 | <davean> | Which is to say the benefits of this very much is associated with specialization and inlining. |
| 2025-04-27 23:56:18 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-27 23:54:18 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 244 seconds) |
| 2025-04-27 23:54:12 +0200 | <davean> | Those simplications usually show up in the code because the fact we used them is how we ended up with the type in the first place. That said, when we start inlining more abstract functions, etc we get to simplify under these new constraints. This is part of the code of how to optimize in Haskell too. |
| 2025-04-27 23:51:42 +0200 | <EvanR> | like in a context where an integer is known to be in a small range or is small in magnitude |
| 2025-04-27 23:47:27 +0200 | <EvanR> | though you might imagine there is more there that can be exploited beyond the obvious |
| 2025-04-27 23:46:48 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) |
| 2025-04-27 23:45:44 +0200 | <davean> | What you're erasing is why the code only does the things it does, not the other things it might have to do. |
| 2025-04-27 23:44:48 +0200 | <EvanR> | ok that's good |
| 2025-04-27 23:44:35 +0200 | <davean> | And which cases can't occur drop which conditions you need to check, etc. |
| 2025-04-27 23:44:12 +0200 | <EvanR> | or the two steps forward that the dependent types added the two steps back for you earlier |
| 2025-04-27 23:43:47 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-27 23:43:40 +0200 | <EvanR> | ok |
| 2025-04-27 23:43:18 +0200 | sabathan2 | (~sabathan@amarseille-159-1-12-107.w86-203.abo.wanadoo.fr) (Read error: Connection reset by peer) |
| 2025-04-27 23:43:14 +0200 | <ncf> | what do you mean? erasure is a form of optimisation |