2025/04/27

Newest at the top

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 +0200sprotte24(~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de) (Quit: Leaving)
2025-04-28 01:24:43 +0200acidjnk_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 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 01:16:45 +0200j0lol(~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 +0200Typedfern(~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Ping timeout: 260 seconds)
2025-04-28 01:12:49 +0200typedfern_(~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 +0200koz(~koz@121.99.240.58) (Ping timeout: 244 seconds)
2025-04-28 01:02:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 00:59:06 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-04-28 00:50:58 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 00:49:49 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-28 00:47:07 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 00:44:31 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-04-28 00:35:05 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 00:34:46 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-28 00:25:20 +0200acidjnk_new(~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
2025-04-28 00:22:51 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
2025-04-28 00:22:00 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-04-28 00:07:43 +0200tromp(~textual@2001:1c00:3487:1b00:ac80:9bb1:e5dc:c7d3) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-28 00:05:40 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 260 seconds)
2025-04-28 00:04:20 +0200j1n37-(~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 +0200gmg(~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 +0200j0lol(~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 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-27 23:54:18 +0200j1n37(~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 +0200sabathan2(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-27 23:43:40 +0200 <EvanR> ok
2025-04-27 23:43:18 +0200sabathan2(~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
2025-04-27 23:40:27 +0200 <EvanR> but is there a way to use that information for optimization instead, instead of just "do no harm"
2025-04-27 23:39:33 +0200 <EvanR> in dependent types world you sometimes hear about erasable types which helps compiled code not be as slowed down carrying proofs around that aren't actually used