2025/04/28

Newest at the top

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 +0200acidjnk_new(~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-04-28 03:00:51 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 02:59:48 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds)
2025-04-28 02:57:40 +0200j1n37(~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 +0200peterbecich(~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 +0200otto_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 +0200otto_s(~user@p5de2f428.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
2025-04-28 02:41:22 +0200haritz(~hrtz@user/haritz) haritz
2025-04-28 02:41:22 +0200haritz(~hrtz@152.37.68.178) (Changing host)
2025-04-28 02:41:22 +0200haritz(~hrtz@152.37.68.178)
2025-04-28 02:40:38 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection)
2025-04-28 02:38:13 +0200sim590(~simon@209-15-185-101.resi.cgocable.ca)
2025-04-28 02:37:59 +0200xff0x(~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 +0200OftenFaded(~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 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 02:13:56 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
2025-04-28 02:10:17 +0200euleritian(~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 +0200merijn(~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 +0200jespada_(~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
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 01:59:21 +0200 <haskellbridge> <loonycyborg> EvanR: ye I actually meant dependent type arithmetic :P