| 2025-04-28 00:00:24 +0200 | j0lol | (~j0lol@132.145.17.236) (Ping timeout: 276 seconds) |
| 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:01:46 +0200 | <davean> | since it sorta drags providence along with it. |
| 2025-04-28 00:02:17 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 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:04:20 +0200 | j1n37- | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 00:05:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Ping timeout: 260 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:22:00 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds) |
| 2025-04-28 00:22:51 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 00:25:20 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 272 seconds) |
| 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:35:05 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) |
| 2025-04-28 00:44:31 +0200 | j1n37- | (~j1n37@user/j1n37) (Ping timeout: 276 seconds) |
| 2025-04-28 00:47:07 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 00:49:49 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 00:50:58 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 00:59:06 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds) |
| 2025-04-28 01:02:21 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 01:03:14 +0200 | koz | (~koz@121.99.240.58) (Ping timeout: 244 seconds) |
| 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:12:49 +0200 | typedfern_ | (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) typedfern |
| 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: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:45 +0200 | j0lol | (~j0lol@132.145.17.236) j0lol |
| 2025-04-28 01:18:01 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 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:19:41 +0200 | <EvanR> | just discard the argument |
| 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:24:43 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) |
| 2025-04-28 01:25:24 +0200 | sprotte24 | (~sprotte24@p200300d16f174f00e11b2faf6af92897.dip0.t-ipconnect.de) (Quit: Leaving) |
| 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:32:13 +0200 | <EvanR> | ... not sure |
| 2025-04-28 01:32:36 +0200 | <monochrom> | Err, ∀r. (Πx:A. B(x) -> r) -> r |
| 2025-04-28 01:34:14 +0200 | <EvanR> | ok yes |
| 2025-04-28 01:34:21 +0200 | <monochrom> | :) |
| 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:35:56 +0200 | <EvanR> | if that's in the machine code then it only bothers somebody trying to disassemnle it |
| 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:36:08 +0200 | <EvanR> | typing with pinkies is hard |
| 2025-04-28 01:36:36 +0200 | fantom | (~fantom@2.219.56.221) (Ping timeout: 244 seconds) |
| 2025-04-28 01:37:20 +0200 | <EvanR> | erasing types or proofs shouldn't change the "observable" behavior |
| 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:38:33 +0200 | <haskellbridge> | <loonycyborg> which probably will have different implementations at runtime and compile time |
| 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:39:22 +0200 | <EvanR> | because this isn't java |
| 2025-04-28 01:39:24 +0200 | mange | (~user@user/mange) mange |
| 2025-04-28 01:39:32 +0200 | <EvanR> | (but I heard java erases it's types also) |
| 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:40:30 +0200 | <EvanR> | well then that's not purely at the type level definitely |
| 2025-04-28 01:41:46 +0200 | <EvanR> | accept keyboard input and append to an ongoing list of Types that you can then ask for a listing of, because they have nice Show instances |
| 2025-04-28 01:41:55 +0200 | <EvanR> | isn't a type level thing |
| 2025-04-28 01:42:33 +0200 | <haskellbridge> | <loonycyborg> to me type erasure seems like technical decision asserting that "compile type == type level; runtime == term level" |
| 2025-04-28 01:43:01 +0200 | <EvanR> | well that's not true is it |
| 2025-04-28 01:43:19 +0200 | <EvanR> | because e.g. constant folding at compile time etc |
| 2025-04-28 01:43:48 +0200 | <haskellbridge> | <loonycyborg> so to get proper dependent types in a compiled language would have to drop type erasure, perhaps replacing it by something else |
| 2025-04-28 01:44:54 +0200 | <EvanR> | once you get to a phase where the types aren't doing anything, then keeping them around can only waste resources |
| 2025-04-28 01:46:03 +0200 | <haskellbridge> | <loonycyborg> But still there is the case of reading of arbitrary type from stdin :P |
| 2025-04-28 01:46:18 +0200 | <EvanR> | you can remove them like a compiler is expected to remove terms that aren't doing anything |
| 2025-04-28 01:46:26 +0200 | <haskellbridge> | <loonycyborg> if you explicitly don't support it then it's unlikely that it's a localized case |
| 2025-04-28 01:46:28 +0200 | <mange> | Idris 2 lets you be precise about which types you expect to be erased from the program, using multiplicities: https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html#erasure |
| 2025-04-28 01:46:41 +0200 | <haskellbridge> | <loonycyborg> like need to explicitly figure out what is supported and what isn't |
| 2025-04-28 01:47:01 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:8240:4eb8:4326:3de4) (Ping timeout: 248 seconds) |
| 2025-04-28 01:47:33 +0200 | <EvanR> | I don't see how you would even erase a type that is generated at runtime |
| 2025-04-28 01:47:37 +0200 | <EvanR> | or why you would want to |
| 2025-04-28 01:50:39 +0200 | fantom | (~fantom@2.219.56.221) |
| 2025-04-28 01:51:13 +0200 | <haskellbridge> | <loonycyborg> What I'm really wondering about are things like: if we read something from stdin and make a type level Nat from it then can we make arbitrary compile time arithmetic on it? |
| 2025-04-28 01:51:33 +0200 | <haskellbridge> | <loonycyborg> And if we can then how it works :P |
| 2025-04-28 01:52:54 +0200 | <EvanR> | if this is mainstreet dependent types you wouldn't have a separate type level Nat |
| 2025-04-28 01:53:17 +0200 | <EvanR> | and compile time arithmetic at runtime sounds like a contradiction |
| 2025-04-28 01:54:02 +0200 | <EvanR> | the Nat used at type level can be the same Nat used at value level |
| 2025-04-28 01:54:13 +0200 | <EvanR> | not a DataKind |
| 2025-04-28 01:55:26 +0200 | <EvanR> | -- oh, compile time arithmetic at runtime, that would be JIT |
| 2025-04-28 01:56:53 +0200 | <mange> | I've also seen https://dl.acm.org/doi/10.1145/3341692, which is kind of about deferring type checking until runtime. It's not exactly what you're looking for, but it feels in the same ballpark. |
| 2025-04-28 01:59:07 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2025-04-28 01:59:21 +0200 | <haskellbridge> | <loonycyborg> EvanR: ye I actually meant dependent type arithmetic :P |
| 2025-04-28 02:01:21 +0200 | <EvanR> | the conflation between arithmetic on literal types is a haskell thing because it's weird type level hacks |
| 2025-04-28 02:01:35 +0200 | <EvanR> | you don't want to do this |
| 2025-04-28 02:01:47 +0200 | <EvanR> | outside haskell |
| 2025-04-28 02:04:17 +0200 | <haskellbridge> | <loonycyborg> Yes, but if it's made fully dependent typed then potentially could read any sort of types from stdin, even those that aren't haskell specific hacks |
| 2025-04-28 02:04:58 +0200 | jespada_ | (~jespada@r186-49-245-168.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds) |
| 2025-04-28 02:05:30 +0200 | <EvanR> | you can read chars or Word8 from stdin I would believe that |
| 2025-04-28 02:06:15 +0200 | <haskellbridge> | <loonycyborg> So I'm thinking that going fully dependent typing would either result in some weird inconsistencies or push the language into becoming fully dynamic like python |
| 2025-04-28 02:06:25 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds) |
| 2025-04-28 02:06:41 +0200 | <haskellbridge> | <loonycyborg> * typed |
| 2025-04-28 02:06:48 +0200 | <EvanR> | python's dynamic types cause the program to crash if a type check fails |
| 2025-04-28 02:06:55 +0200 | <EvanR> | that wouldn't happen |
| 2025-04-28 02:07:16 +0200 | <EvanR> | the program itself can be well typed while still juggling types at runtime |
| 2025-04-28 02:07:26 +0200 | <EvanR> | (for whatever reason) |
| 2025-04-28 02:10:17 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2025-04-28 02:13:56 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 02:17:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 02:18:20 +0200 | <monochrom> | Yeah "type-level 0::Nat as opposed to term-level 0::Nat" is a GHC invention, proving that GHC does not have dependent typing. In dependent typing there is just one 0::Nat; you can use it anywhere you want, in a term or in a type, but it's the same 0::Nat used in both sites, not two different versions. |
| 2025-04-28 02:18:37 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 2025-04-28 02:19:34 +0200 | OftenFaded | (~OftenFade@user/tisktisk) OftenFaded |
| 2025-04-28 02:23:38 +0200 | <haskellbridge> | <loonycyborg> Practical case would be serialization: can you construct your data entirely based on something you de-serialize with dependent types? |
| 2025-04-28 02:24:06 +0200 | <haskellbridge> | <loonycyborg> Probably if your program operates on such types then it wouldn't be too optimized |
| 2025-04-28 02:24:22 +0200 | <haskellbridge> | <loonycyborg> because compiler doesn't know anything about actual data that will be read |
| 2025-04-28 02:24:26 +0200 | <haskellbridge> | <loonycyborg> unless it'sJIT |
| 2025-04-28 02:24:47 +0200 | <monochrom> | If you have n::Nat coming from user input, for example the user inputs n booleans and you store them in an index-safe vector, i.e., the vector type includes the length n, i.e., Vec n Bool, then generically speaking you now have a sigma type: v :: Σn::Nat. Vec n Bool. You can call that dynamic; it's a sigma, it's OOP now. |
| 2025-04-28 02:27:28 +0200 | <monochrom> | Or you can do an implicit church encoding like I described. You don't construct a pair for the sigma type, you pass n and v "separately" to a function foo :: (n::Nat) -> Vec n Bool -> IO (). |
| 2025-04-28 02:30:10 +0200 | <monochrom> | s/pass n and v/pass n and the vector/ |
| 2025-04-28 02:34:01 +0200 | <monochrom> | You are reminding me of that joke (or true story) about C++ back then. |
| 2025-04-28 02:34:57 +0200 | <monochrom> | Someone wrote a prime factorization algorithm in C++ that takes O(1) time. How: The factorization happened at compile time, the generated code just needs to print the answer. |
| 2025-04-28 02:35:31 +0200 | <geekosaur> | true story and done multiple times by multiple people |
| 2025-04-28 02:36:03 +0200 | <geekosaur> | (one of whom was a CS postgrad at C-MU who replicated it after hearing about the original) |
| 2025-04-28 02:36:55 +0200 | <monochrom> | If you require the number in question to be obtained during runtime-only from some user or entity, then the factorization must happen at run time. Do you call that unoptimized, just because the "O(1)-time static solution" exists? |
| 2025-04-28 02:37:59 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a) |
| 2025-04-28 02:38:13 +0200 | sim590 | (~simon@209-15-185-101.resi.cgocable.ca) |
| 2025-04-28 02:40:38 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@152.37.68.178) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-28 02:41:31 +0200 | otto_s | (~user@p5de2f428.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-28 02:44:56 +0200 | <monochrom> | I guess I can cheat too. I can take it down to linear time. The program is a huge binary search tree that stores the answer for every input for a sufficiently large range. The exe will not fit in any storage in existence today, nay, any data centre, but we can talk hypothetically about how nice it would be. >:) |