Newest at the top
2025-04-28 01:40:30 +0200 | <EvanR> | well then that's not purely at the type level definitely |
2025-04-28 01:39:50 +0200 | <haskellbridge> | <loonycyborg> I'm not so sure because of types that could be specified entirely at runtime |
2025-04-28 01:39:32 +0200 | <EvanR> | (but I heard java erases it's types also) |
2025-04-28 01:39:24 +0200 | mange | (~user@user/mange) mange |
2025-04-28 01:39:22 +0200 | <EvanR> | because this isn't java |
2025-04-28 01:38:54 +0200 | <EvanR> | if it's purely at the type level then it wouldn't need to exist at runtime |
2025-04-28 01:38:33 +0200 | <haskellbridge> | <loonycyborg> which probably will have different implementations at runtime and compile time |
2025-04-28 01:38:16 +0200 | <haskellbridge> | <loonycyborg> still it requires operating on type level things that can't be erased |
2025-04-28 01:37:20 +0200 | <EvanR> | erasing types or proofs shouldn't change the "observable" behavior |
2025-04-28 01:36:36 +0200 | fantom | (~fantom@2.219.56.221) (Ping timeout: 244 seconds) |
2025-04-28 01:36:08 +0200 | <EvanR> | typing with pinkies is hard |
2025-04-28 01:36:02 +0200 | <monochrom> | Maybe the programmer doesn't use that encoding, but the compiler does the translation. |
2025-04-28 01:35:56 +0200 | <EvanR> | if that's in the machine code then it only bothers somebody trying to disassemnle it |
2025-04-28 01:35:01 +0200 | <haskellbridge> | <loonycyborg> Even if you technically make this work not sure it would be a good language design. Like most types that aren't passed around are erased but some have to remain which kinda feels inconsistent. |
2025-04-28 01:34:21 +0200 | <monochrom> | :) |
2025-04-28 01:34:14 +0200 | <EvanR> | ok yes |
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) |