Newest at the top
| 2025-04-28 03:07:21 +0200 | weary-traveler | (~user@user/user363627) user363627 |
| 2025-04-28 03:07:04 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2025-04-28 03:05:52 +0200 | <int-e> | Ah yeah the good old 1988 IOCCC entry. |
| 2025-04-28 03:03:32 +0200 | <mauke> | #include "/dev/tty" // please type the correct code |
| 2025-04-28 03:02:41 +0200 | acidjnk_new | (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2025-04-28 03:00:51 +0200 | j1n37 | (~j1n37@user/j1n37) j1n37 |
| 2025-04-28 02:59:48 +0200 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds) |
| 2025-04-28 02:57:40 +0200 | j1n37 | (~j1n37@user/j1n37) (Read error: Connection reset by peer) |
| 2025-04-28 02:55:26 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) (Ping timeout: 272 seconds) |
| 2025-04-28 02:54:12 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-04-28 02:51:55 +0200 | <ames> | if you don't have typecase at runtime you can just erase all the types in addition to things that are otherwise marked erased. agda does this, pretty sure coq does too |
| 2025-04-28 02:50:48 +0200 | otto_s | (~user@p4ff27ad7.dip0.t-ipconnect.de) |
| 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. >:) |
| 2025-04-28 02:41:31 +0200 | otto_s | (~user@p5de2f428.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@user/haritz) haritz |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@152.37.68.178) (Changing host) |
| 2025-04-28 02:41:22 +0200 | haritz | (~hrtz@152.37.68.178) |
| 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:38:13 +0200 | sim590 | (~simon@209-15-185-101.resi.cgocable.ca) |
| 2025-04-28 02:37:59 +0200 | xff0x | (~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a) |
| 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: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:35:31 +0200 | <geekosaur> | true story and done multiple times by multiple people |
| 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:34:01 +0200 | <monochrom> | You are reminding me of that joke (or true story) about C++ back then. |
| 2025-04-28 02:30:10 +0200 | <monochrom> | s/pass n and v/pass n and the vector/ |
| 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: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:24:26 +0200 | <haskellbridge> | <loonycyborg> unless it'sJIT |
| 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:06 +0200 | <haskellbridge> | <loonycyborg> Probably if your program operates on such types then it wouldn't be too optimized |
| 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:19:34 +0200 | OftenFaded | (~OftenFade@user/tisktisk) OftenFaded |
| 2025-04-28 02:18:37 +0200 | __jmcantrell__ | (~weechat@user/jmcantrell) jmcantrell |
| 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:17:44 +0200 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-04-28 02:13:56 +0200 | euleritian | (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) |
| 2025-04-28 02:10:17 +0200 | euleritian | (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2025-04-28 02:07:26 +0200 | <EvanR> | (for whatever reason) |
| 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:06:55 +0200 | <EvanR> | that wouldn't happen |
| 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:41 +0200 | <haskellbridge> | <loonycyborg> * typed |
| 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: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:05:30 +0200 | <EvanR> | you can read chars or Word8 from stdin I would believe that |
| 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: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:01:47 +0200 | <EvanR> | outside haskell |
| 2025-04-28 02:01:35 +0200 | <EvanR> | you don't want to do this |