IRCBrowse

2025/04/28

2025-04-28 00:00:24 +0200j0lol(~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 +0200gmg(~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 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-28 00:05:40 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 260 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:22:00 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-04-28 00:22:51 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
2025-04-28 00:25:20 +0200acidjnk_new(~acidjnk@p200300d6e71c4f291c3f5884f0a5aebe.dip0.t-ipconnect.de) (Ping timeout: 272 seconds)
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:35:05 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 00:44:31 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 276 seconds)
2025-04-28 00:47:07 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 00:49:49 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-28 00:50:58 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 00:59:06 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-04-28 01:02:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 01:03:14 +0200koz(~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 +0200typedfern_(~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) typedfern
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: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 +0200j0lol(~j0lol@132.145.17.236) j0lol
2025-04-28 01:18:01 +0200peterbecich(~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 +0200acidjnk_new(~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de)
2025-04-28 01:25:24 +0200sprotte24(~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 +0200fantom(~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 +0200mange(~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 +0200xff0x(~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 +0200fantom(~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 +0200Tuplanolla(~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 +0200jespada_(~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 +0200merijn(~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 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds)
2025-04-28 02:13:56 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
2025-04-28 02:17:44 +0200merijn(~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 +0200OftenFaded(~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 +0200xff0x(~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a)
2025-04-28 02:38:13 +0200sim590(~simon@209-15-185-101.resi.cgocable.ca)
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:41:22 +0200haritz(~hrtz@152.37.68.178)
2025-04-28 02:41:22 +0200haritz(~hrtz@152.37.68.178) (Changing host)
2025-04-28 02:41:22 +0200haritz(~hrtz@user/haritz) haritz
2025-04-28 02:41:31 +0200otto_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. >:)
2025-04-28 02:50:48 +0200otto_s(~user@p4ff27ad7.dip0.t-ipconnect.de)
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:54:12 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 02:55:26 +0200__jmcantrell__(~weechat@user/jmcantrell) (Ping timeout: 272 seconds)
2025-04-28 02:57:40 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 02:59:48 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds)
2025-04-28 03:00:51 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 03:02:41 +0200acidjnk_new(~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-04-28 03:03:32 +0200 <mauke> #include "/dev/tty" // please type the correct code
2025-04-28 03:05:52 +0200 <int-e> Ah yeah the good old 1988 IOCCC entry.
2025-04-28 03:07:04 +0200weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-04-28 03:07:21 +0200weary-traveler(~user@user/user363627) user363627
2025-04-28 03:13:51 +0200OftenFaded9(~OftenFade@user/tisktisk) OftenFaded
2025-04-28 03:14:54 +0200OftenFaded(~OftenFade@user/tisktisk) (Ping timeout: 240 seconds)
2025-04-28 03:15:19 +0200bitmapper(uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2025-04-28 03:15:30 +0200OftenFaded9(~OftenFade@user/tisktisk) (Client Quit)
2025-04-28 03:18:07 +0200 <monochrom> Oh hahaha
2025-04-28 03:21:14 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds)
2025-04-28 03:22:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-28 03:28:53 +0200snoopy1(~Thunderbi@199.115.144.130)
2025-04-28 03:33:06 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-28 03:33:24 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 03:33:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 03:34:35 +0200hgolden(~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) (Remote host closed the connection)
2025-04-28 03:37:01 +0200hgolden(~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) hgolden
2025-04-28 03:42:10 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-04-28 03:42:31 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 03:44:24 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-28 03:44:54 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 03:48:48 +0200notdabs(~Owner@2600:1700:69cf:9000:c531:a8cf:57a8:ee6f) (Quit: Leaving)
2025-04-28 03:55:03 +0200xff0x(~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a) (Ping timeout: 276 seconds)
2025-04-28 03:55:24 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2025-04-28 04:19:59 +0200Guest85(~Guest85@83.234.227.67)
2025-04-28 04:20:37 +0200td_(~td@i5387092A.versanet.de) (Ping timeout: 248 seconds)
2025-04-28 04:21:32 +0200Guest85(~Guest85@83.234.227.67) (Client Quit)
2025-04-28 04:22:13 +0200td_(~td@i53870908.versanet.de)
2025-04-28 04:29:46 +0200snoopy1(~Thunderbi@199.115.144.130) (Quit: snoopy1)
2025-04-28 04:30:04 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds)
2025-04-28 04:30:24 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
2025-04-28 04:37:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-28 04:45:25 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-28 04:48:47 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-28 04:49:05 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 04:49:47 +0200Square(~Square@user/square) (Ping timeout: 265 seconds)
2025-04-28 04:50:05 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 04:50:18 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-04-28 04:51:08 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 04:56:45 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2025-04-28 05:01:43 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-04-28 05:03:40 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 05:03:56 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 05:12:21 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 05:12:38 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 05:30:21 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-28 05:31:45 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 05:32:37 +0200koz(~koz@121.99.240.58)
2025-04-28 05:35:16 +0200cbs(df2953d28a@2a03:6000:1812:100::1451) cbs
2025-04-28 05:36:08 +0200cbs(df2953d28a@2a03:6000:1812:100::1451) ()
2025-04-28 05:38:38 +0200 <haskellbridge> <Bowuigi> loonycyborg if your pi type acts as a forall, you can erase it safely. There's more conditions but that's the most intuitive one
2025-04-28 05:41:32 +0200 <haskellbridge> <Bowuigi> EvanR type erasure is part of standard optimization in any functional lang. Dependently typed langs get a "cut-down" version of it that requires complex algorithms to work properly (not sure if it's actually decidable). It's a problem on dependently typed langs, but a given on the rest
2025-04-28 05:41:51 +0200 <haskellbridge> <Bowuigi> Also that's partly why dependent haskell takes so much effort
2025-04-28 05:42:37 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 05:43:53 +0200weary-traveler(~user@user/user363627) (Remote host closed the connection)
2025-04-28 05:45:42 +0200 <haskellbridge> <Bowuigi> Another big reason was hinted at here too: Dependent types + unrestricted effects = magic. You can get something with a random type or with a type you read from stdin. Dependent types in Haskell aren't just about the proofs, it's about making a stupidly powerful language for everyone
2025-04-28 05:50:57 +0200 <haskellbridge> <Bowuigi> Also, opening the door to dependent types means allowing the "I want to prove more and more" philosophy. First one adds the base constructs because deriving the eta laws for the rest of things is harder with just pi types (unless you use a novel trick from a random thesis I read and forgot about), then dependent ADTs, then slightly more complex equality, then HITs, then IRTs, then IITs, then cubical stuff, then...
2025-04-28 05:51:02 +0200 <haskellbridge> ... extension types, then you take a Higher Observational detour aaaand you've reached current research and are stuck with a very complex system that's too hard to verify properly.
2025-04-28 05:52:23 +0200 <haskellbridge> <Bowuigi> Suddenly to get a chance of using the newest features you need a PhD because progress is not quite there yet
2025-04-28 05:52:25 +0200 <ames> seems very strange to assume that this is a common thing to do when there's exactly one language that's done that
2025-04-28 05:54:01 +0200 <ames> also erasing types is very easy. code generators for languages that aren't Idris2 simply do not include a way to generate code for types
2025-04-28 05:54:36 +0200 <ames> it's erasing the things that *aren't* types e.g. lengths of vectors that's complicated
2025-04-28 05:54:58 +0200 <haskellbridge> <Bowuigi> I see
2025-04-28 05:55:42 +0200 <haskellbridge> <Bowuigi> As for the "I want to prove more" thing, Agda is the prime example, but Coq and the Red* family (tho that's many languages, so not that big of an issue) are following suit. The rest are kinda on the same path, but moving more slowly
2025-04-28 05:57:59 +0200 <haskellbridge> <Bowuigi> It isn't that big of a problem for theorem provers because well, they exist to prove theorems, but Haskell is not a theorem prover
2025-04-28 05:58:05 +0200 <ames> coq does not have anything approaching a cubical mode and jon's proof assistants are basically proofs-of-concept
2025-04-28 05:58:54 +0200 <ames> "make three to throw away" and all that
2025-04-28 05:59:56 +0200 <haskellbridge> <Bowuigi> The previous steps (inductive-inductive and inductive-recursive stuff) were added / are in progress because of user demand in Coq AFAIU
2025-04-28 06:00:37 +0200 <ames> "previous steps" - those are completely orthogonal features.
2025-04-28 06:03:40 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Quit: Client closed)
2025-04-28 06:05:30 +0200 <haskellbridge> <Bowuigi> Yeah that's the idea
2025-04-28 06:06:13 +0200 <haskellbridge> <Bowuigi> Can't find the IIT/IRT stuff on the Coq issues but I remember some talk about supporting them exists lol
2025-04-28 06:06:25 +0200 <haskellbridge> <Bowuigi> I should take more notes
2025-04-28 06:10:18 +0200 <ames> but you're talking about these things as if there's a "universal dependently-typed language" that everyone's converging to. this is nonsense. idris people are not interested in "more complex equality" or "cubical stuff" and lean people are outright hostile towards these things
2025-04-28 06:11:35 +0200 <haskellbridge> <Bowuigi> Ah, sorry, that's not what I meant. I mean that one should resist the temptation to add a lot of shiny new features, as with any software project
2025-04-28 06:16:01 +0200 <haskellbridge> <Liamzee> huh, that's interesting, and probably extremely degenerate
2025-04-28 06:16:16 +0200 <haskellbridge> <Liamzee> you know how emojis are actually part of the haskell operator namespace?
2025-04-28 06:16:56 +0200 <haskellbridge> <Liamzee> if you want an operator version of go, emojis actually suffice since they have no collisions and are single characters. They also brighten up your day. :)
2025-04-28 06:18:55 +0200 <ames> i think some emoji should be uppercase so we can use them as constructors
2025-04-28 06:27:36 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2025-04-28 06:27:48 +0200gorignak(~gorignak@user/gorignak) gorignak
2025-04-28 06:29:30 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 06:34:48 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 06:37:40 +0200polykernel(~polykerne@user/polykernel) (Remote host closed the connection)
2025-04-28 06:38:49 +0200polykernel(~polykerne@user/polykernel) polykernel
2025-04-28 06:40:04 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 06:40:39 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Quit: Client closed)
2025-04-28 06:43:49 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 06:44:12 +0200michalz(~michalz@185.246.207.218)
2025-04-28 06:44:13 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 06:44:44 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Write error: Broken pipe)
2025-04-28 06:47:13 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-28 06:47:58 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 06:49:38 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 06:51:32 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 06:52:52 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 06:56:03 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 06:58:02 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 06:58:37 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 07:00:51 +0200jacopovalanzano(~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Quit: Client closed)
2025-04-28 07:01:40 +0200 <EvanR> or lowercase so we can use them as variables
2025-04-28 07:02:54 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 07:03:57 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 07:07:05 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 07:09:38 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 07:14:08 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 07:17:15 +0200takuan(~takuan@d8D86B601.access.telenet.be)
2025-04-28 07:26:44 +0200harveypwca(~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c)
2025-04-28 07:30:45 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 07:33:14 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 07:36:52 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-04-28 07:37:38 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
2025-04-28 07:39:00 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 07:42:03 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 07:42:53 +0200haritz(~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
2025-04-28 07:47:07 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 07:53:36 +0200j1n37(~j1n37@user/j1n37) (Read error: Connection reset by peer)
2025-04-28 07:56:38 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 07:59:04 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 07:59:19 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 08:05:01 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2025-04-28 08:11:06 +0200jco(~jco@78-70-217-44-no600.tbcn.telia.com) jco
2025-04-28 08:12:32 +0200 <jco> Hey, anyone got any recommendations on libraries that can be used for writing (binary) file formats? I.e. something like the inverse of parsing...?
2025-04-28 08:13:12 +0200 <geekosaur> @hackage binary
2025-04-28 08:13:12 +0200 <lambdabot> https://hackage.haskell.org/package/binary
2025-04-28 08:13:16 +0200 <geekosaur> @hackage cereal
2025-04-28 08:13:16 +0200 <lambdabot> https://hackage.haskell.org/package/cereal
2025-04-28 08:14:25 +0200 <jco> geekosaur: Thanks a lot.
2025-04-28 08:15:01 +0200haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection)
2025-04-28 08:18:13 +0200pabs3(~pabs3@user/pabs3) (Ping timeout: 276 seconds)
2025-04-28 08:20:40 +0200 <Axman6> I kind of wish there were better options these days, I'm sure there must be. There was some really cool work that went into the cborg and serialise packages to make it fast but it's specific to CBOR
2025-04-28 08:22:35 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) CiaoSen
2025-04-28 08:22:48 +0200chele(~chele@user/chele) chele
2025-04-28 08:24:34 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
2025-04-28 08:24:51 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 08:27:18 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
2025-04-28 08:29:55 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds)
2025-04-28 08:34:23 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 08:44:24 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-28 08:48:18 +0200halloy3041(~halloy304@2001:569:76fd:b00:ada3:3d53:48e5:4f37)
2025-04-28 08:50:29 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
2025-04-28 08:51:39 +0200ft(~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving)
2025-04-28 08:55:41 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-28 08:55:47 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk
2025-04-28 08:57:59 +0200__monty__(~toonn@user/toonn) toonn
2025-04-28 09:00:03 +0200caconym7(~caconym@user/caconym) (Quit: bye)
2025-04-28 09:00:42 +0200caconym7(~caconym@user/caconym) caconym
2025-04-28 09:03:03 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-28 09:03:36 +0200haskellbridge(~hackager@syn-024-093-192-219.res.spectrum.com) hackager
2025-04-28 09:03:36 +0200 <haskellbridge> <hellwolf> "less mainstream logics"
2025-04-28 09:03:36 +0200 <haskellbridge> <Bowuigi> Oh, mainstream here means popular, in a sense
2025-04-28 09:03:36 +0200 <haskellbridge> <Bowuigi> As to which logics specifically, it actually depends on the features the type system has. Haven't read much on categorical logic yet but AFAIU you can use toposes to model dependently typed systems
2025-04-28 09:03:36 +0200ChanServ+v haskellbridge
2025-04-28 09:03:45 +0200 <haskellbridge> <hellwolf> I actually don't have a clue what qualifies aslogic in the first place... I guess, something to do with formal way of describing"equality"?
2025-04-28 09:03:47 +0200 <haskellbridge> <hellwolf> anyhow, not going to far,
2025-04-28 09:03:49 +0200 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/crunkvuyNAgcnoaGKHVPavQw/HhaisemMfmk (5 lines)
2025-04-28 09:03:50 +0200 <haskellbridge> <Bowuigi> If a proof is too trivial for you, it's probably also trivial on code. Some exceptions exist depending on what you consider trivial
2025-04-28 09:03:52 +0200 <haskellbridge> <Bowuigi> Proofs about type systems are the proofs I read the most, I like how easy it is to do those in Twelf
2025-04-28 09:03:54 +0200 <haskellbridge> <Bowuigi> Other logics can be embedded on top by using the actual implementation as a framework, but it's not a full replacement yeah
2025-04-28 09:03:56 +0200 <haskellbridge> <Bowuigi> (Those are independent replies from 1 to 3, in order)
2025-04-28 09:03:57 +0200 <haskellbridge> <hellwolf> understand. i am the consumer of type systems, i try to use it for something. by too trivial proofs, i meant judging from the value where it is used
2025-04-28 09:03:59 +0200 <haskellbridge> <hellwolf> "less run time error" is probably the "KPI"
2025-04-28 09:04:01 +0200 <haskellbridge> <hellwolf> interesting dependent types thread...
2025-04-28 09:04:02 +0200 <haskellbridge> What's the healthy level of proofs that you would put in Haskell?
2025-04-28 09:04:04 +0200 <haskellbridge> <Bowuigi> Up to and including the base constructs seems good enough I guess
2025-04-28 09:04:05 +0200 <haskellbridge> <hellwolf> - propositional logic <-> static types (?)
2025-04-28 09:04:07 +0200 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/UEPByodBGyiSVOqodXeCtYPh/LKR6AzyTcQ4 (3 lines)
2025-04-28 09:04:08 +0200 <haskellbridge> <Bowuigi> Actually dependency in user-defined ADTs is good. With base constructs I mean pi and sigma types
2025-04-28 09:04:10 +0200 <haskellbridge> <hellwolf> From logic's perspective, is dependent type to make the quantifiers more rigour vs. in Haskell usually you hand wave it or slap a quickcheck to it for the day?
2025-04-28 09:04:12 +0200 <haskellbridge> <Bowuigi> Yeah that's the main idea, but formalizing/verifying stuff is optional, you can use a dependently typed lang without making use of any dependent types
2025-04-28 09:04:14 +0200 <haskellbridge> <Bowuigi> Also dependent types don't correspond to propositional logic, but rather to less mainstream logics that have more power in some places but less in others
2025-04-28 09:04:16 +0200 <haskellbridge> <hellwolf> what is that?
2025-04-28 09:04:18 +0200 <haskellbridge> <Bowuigi> "Everyone's bad at code" and "I like having a good mental health" are probably why we still have PL research lol
2025-04-28 09:04:21 +0200geekosaurwonders how long those were queued
2025-04-28 09:05:40 +0200 <haskellbridge> <hellwolf> Heh, yea, selling DT is hard because people are lazy and handwave the proofs a way by doing it on paper or simply yolo
2025-04-28 09:07:29 +0200akegalj(~akegalj@83-131-242-128.adsl.net.t-com.hr) akegalj
2025-04-28 09:07:33 +0200 <haskellbridge> <geekosaur> oh, they weren't, you were just catching up while the bot was down (system upgrade)
2025-04-28 09:07:34 +0200 <haskellbridge> <hellwolf> But rust also shows that some technique of better managing runtime system behaviour can be appreciated. Do you consider DT and LinearTypes are orthogonal to each other as researches?
2025-04-28 09:07:59 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-28 09:09:07 +0200 <haskellbridge> <hellwolf> Also, I think length-indexed vector is the most practical everyday stuff DT should sell hard. Like selling ADT and pattern matching to mainstream languages.
2025-04-28 09:11:51 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
2025-04-28 09:17:29 +0200prdak(~Thunderbi@user/prdak) (Ping timeout: 245 seconds)
2025-04-28 09:19:10 +0200 <c_wraith> length-indexed vectors are very easy to understand, but actually quite awkward to use. Like... filter can have a ton of different types, and it turns out all of them are a pain to work with.
2025-04-28 09:21:42 +0200Lord_of_Life_(~Lord@user/lord-of-life/x-2819915) Lord_of_Life
2025-04-28 09:21:51 +0200euleritian(~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-28 09:22:08 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 09:22:34 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds)
2025-04-28 09:22:43 +0200harveypwca(~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving)
2025-04-28 09:23:05 +0200Lord_of_Life_Lord_of_Life
2025-04-28 09:23:12 +0200akegalj(~akegalj@83-131-242-128.adsl.net.t-com.hr) (Ping timeout: 252 seconds)
2025-04-28 09:28:55 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 09:31:45 +0200img(~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
2025-04-28 09:32:53 +0200akegalj(~akegalj@144-188.dsl.iskon.hr)
2025-04-28 09:33:05 +0200img(~img@user/img) img
2025-04-28 09:34:53 +0200prdak(~Thunderbi@user/prdak) (Quit: prdak)
2025-04-28 09:34:57 +0200 <haskellbridge> <hellwolf> https://hackage.haskell.org/package/vec-0.5.1/docs/Data-Vec-Lazy.html#g:5
2025-04-28 09:34:57 +0200 <haskellbridge> I am checking this... which one is painful? I am asking unironically.
2025-04-28 09:35:12 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 09:36:47 +0200 <haskellbridge> <hellwolf> > dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n
2025-04-28 09:36:47 +0200 <haskellbridge> beautiful interface :p
2025-04-28 09:37:12 +0200emmanuelux_(~emmanuelu@user/emmanuelux) (Quit: au revoir)
2025-04-28 09:37:32 +0200 <haskellbridge> <hellwolf> but I can see the problem of filtering.
2025-04-28 09:37:53 +0200xelxebar(~xelxebar@wilsonb.com) (Ping timeout: 248 seconds)
2025-04-28 09:39:32 +0200 <haskellbridge> <hellwolf> though, I could think " filter" differently, it is a fold that adding a boolean to the original vector
2025-04-28 09:39:34 +0200 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/nUqJifIEojXapRsqcNyBxQyG/SZSeSOaoePA (3 lines)
2025-04-28 09:39:50 +0200 <haskellbridge> <hellwolf> something like that, depending the use case
2025-04-28 09:43:41 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 09:43:58 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 09:44:36 +0200emmanuelux(~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
2025-04-28 09:45:33 +0200xelxebar(~xelxebar@wilsonb.com) xelxebar
2025-04-28 09:46:19 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2025-04-28 09:46:45 +0200 <Leary> Cute fact about that `dfoldr`: just like with regular `foldr` on lists, you can rearrange it to get the church encoding `Vec n a` ~ `forall f. (forall m. a -> f m -> f (S m)) -> f Z -> f n`. Rare to see these for GADTs.
2025-04-28 09:52:53 +0200prdak(~Thunderbi@user/prdak) (Ping timeout: 252 seconds)
2025-04-28 09:53:35 +0200merijn(~merijn@77.242.116.146) merijn
2025-04-28 09:53:35 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) machinedgod
2025-04-28 09:54:24 +0200 <haskellbridge> <hellwolf> amazing.
2025-04-28 09:54:24 +0200 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/ZXmHzkdBFkCbuBgjCCIfldSk/hI24ncMuDu0 (3 lines)
2025-04-28 09:59:15 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 09:59:30 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 10:06:46 +0200gmg(~user@user/gehmehgeh) gehmehgeh
2025-04-28 10:16:13 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-28 10:29:58 +0200lxsameer(~lxsameer@Serene/lxsameer) lxsameer
2025-04-28 10:39:26 +0200pabs3(~pabs3@user/pabs3) pabs3
2025-04-28 10:43:14 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
2025-04-28 10:44:31 +0200comerijn(~merijn@77.242.116.146) merijn
2025-04-28 10:44:47 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 10:47:28 +0200merijn(~merijn@77.242.116.146) (Ping timeout: 252 seconds)
2025-04-28 10:50:23 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 10:54:05 +0200xff0x(~xff0x@2409:251:9040:2c00:c640:4db6:d630:f639)
2025-04-28 11:00:01 +0200prdak(~Thunderbi@user/prdak) (Ping timeout: 248 seconds)
2025-04-28 11:01:29 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2025-04-28 11:01:56 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-28 11:02:41 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 248 seconds)
2025-04-28 11:02:42 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-04-28 11:03:02 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 11:03:43 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2025-04-28 11:05:12 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-04-28 11:05:22 +0200starburst(~starburst@2601:602:680:2280:dd8c:92ac:a129:aaa9)
2025-04-28 11:05:45 +0200 <starburst> hello h
2025-04-28 11:07:20 +0200 <starburst> is anyone ther? (anyone ther.. anythr,,, (echoes))
2025-04-28 11:07:29 +0200Digit(~user@user/digit) (Ping timeout: 245 seconds)
2025-04-28 11:09:03 +0200 <jco> hi hi
2025-04-28 11:10:17 +0200FragByte(~christian@user/fragbyte) (Quit: Quit)
2025-04-28 11:12:08 +0200 <lxsameer> b
2025-04-28 11:12:13 +0200FragByte(~christian@user/fragbyte) FragByte
2025-04-28 11:13:54 +0200 <starburst> hii
2025-04-28 11:14:09 +0200xff0x(~xff0x@2409:251:9040:2c00:c640:4db6:d630:f639) (Ping timeout: 245 seconds)
2025-04-28 11:14:33 +0200starburst(~starburst@2601:602:680:2280:dd8c:92ac:a129:aaa9) (Quit: Client closed)
2025-04-28 11:16:12 +0200werneta(~werneta@syn-071-083-160-242.res.spectrum.com) (Read error: Connection reset by peer)
2025-04-28 11:17:20 +0200 <prdak> hiiii
2025-04-28 11:19:34 +0200werneta(~werneta@syn-071-083-160-242.res.spectrum.com) werneta
2025-04-28 11:21:26 +0200 <haskellbridge> <hellwolf> h <> repeat 'i'
2025-04-28 11:27:30 +0200fp(~Thunderbi@2001:708:20:1406::10c5) fp
2025-04-28 11:30:56 +0200L29Ah(~L29Ah@wikipedia/L29Ah) ()
2025-04-28 11:31:38 +0200L29Ah(~L29Ah@wikipedia/L29Ah) L29Ah
2025-04-28 11:31:40 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2025-04-28 11:35:14 +0200hellwolf(~user@df56-1a33-0fb6-67d2-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 268 seconds)
2025-04-28 11:37:46 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk
2025-04-28 11:38:03 +0200hellwolf(~user@0f4e-6074-8c9d-a17c-0f00-4d40-07d0-2001.sta.estpak.ee) hellwolf
2025-04-28 11:39:46 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
2025-04-28 11:42:11 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2025-04-28 11:42:55 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 11:46:44 +0200prdak(~Thunderbi@user/prdak) (Read error: Connection reset by peer)
2025-04-28 11:48:21 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 11:54:34 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-28 11:55:27 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 12:05:37 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-28 12:05:37 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-28 12:11:11 +0200mari-estel(~mari-este@user/mari-estel) mari-estel
2025-04-28 12:11:52 +0200poscat(~poscat@user/poscat) poscat
2025-04-28 12:12:03 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-04-28 12:12:51 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Max SendQ exceeded)
2025-04-28 12:13:35 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-04-28 12:14:45 +0200poscat0x04(~poscat@user/poscat) (Ping timeout: 248 seconds)
2025-04-28 12:15:28 +0200jco(~jco@78-70-217-44-no600.tbcn.telia.com) (Quit: leaving)
2025-04-28 12:19:17 +0200tromp(~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Read error: Connection reset by peer)
2025-04-28 12:21:17 +0200dhil(~dhil@5.151.29.138) dhil
2025-04-28 12:28:08 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
2025-04-28 12:28:24 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 12:28:31 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
2025-04-28 12:28:49 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 12:30:28 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
2025-04-28 12:30:46 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 12:31:42 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2025-04-28 12:37:00 +0200__monty__(~toonn@user/toonn) (Ping timeout: 260 seconds)
2025-04-28 12:37:04 +0200s3(~s3@user/bn) (Ping timeout: 245 seconds)
2025-04-28 12:37:12 +0200JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-04-28 12:37:24 +0200qaotsap(~paotsaq@2001:818:ea0e:8300:6733:50c0:6d2:30c2) (Ping timeout: 260 seconds)
2025-04-28 12:37:59 +0200mceresa(~mceresa@user/mceresa) (Ping timeout: 260 seconds)
2025-04-28 12:38:01 +0200yin(~z@user/zero) (Ping timeout: 252 seconds)
2025-04-28 12:43:18 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-28 12:44:24 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 260 seconds)
2025-04-28 12:48:37 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2025-04-28 12:49:22 +0200down200(~down200@shell.lug.mtu.edu) down200
2025-04-28 12:51:52 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de)
2025-04-28 13:02:01 +0200jespada(~jespada@r186-49-240-45.dialup.adsl.anteldata.net.uy) jespada
2025-04-28 13:04:20 +0200AlexZenon(~alzenon@178.34.151.238) (Quit: ;-)
2025-04-28 13:08:20 +0200AlexNoo(~AlexNoo@178.34.151.238) (Read error: Connection reset by peer)
2025-04-28 13:09:59 +0200Digit(~user@user/digit) Digit
2025-04-28 13:11:41 +0200JuanDaughertyColinRobinson
2025-04-28 13:15:28 +0200typedfern_(~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Remote host closed the connection)
2025-04-28 13:21:04 +0200AlexNoo(~AlexNoo@178.34.151.238)
2025-04-28 13:21:55 +0200AlexZenon(~alzenon@178.34.151.238)
2025-04-28 13:23:07 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
2025-04-28 13:23:24 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 13:23:56 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
2025-04-28 13:24:14 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) alexherbo2
2025-04-28 13:26:06 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 13:27:24 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
2025-04-28 13:30:13 +0200mari-estel(~mari-este@user/mari-estel) (Ping timeout: 276 seconds)
2025-04-28 13:34:55 +0200 <kqr> I find that toRational @Double 2.3 yields something close to 2.299999999 rather than 23 % 10 as I would expect. This seems strange to me because as far as I can tell, 2.3 is perfectly representable as a double-precision value.
2025-04-28 13:35:02 +0200 <kqr> Is this known/expected only I've missed something?
2025-04-28 13:35:47 +0200ColinRobinson(~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
2025-04-28 13:40:03 +0200mari-estel(~mari-este@user/mari-estel) mari-estel
2025-04-28 13:42:37 +0200prdak(~Thunderbi@user/prdak) (Read error: Connection reset by peer)
2025-04-28 13:43:36 +0200 <opqdonut> it's not perfectly representable, though
2025-04-28 13:43:40 +0200 <opqdonut> see eg. https://float.exposed/0x40133333
2025-04-28 13:46:15 +0200 <kqr> Oh. I wonder where I went wrong in my calculations!
2025-04-28 13:47:24 +0200 <kqr> No, wait, that's for a single-precision float.
2025-04-28 13:47:29 +0200 <opqdonut> yeah but it's the same
2025-04-28 13:47:36 +0200 <kqr> If you click the double tab it shows that 2.3 is representable with double precision
2025-04-28 13:47:39 +0200 <opqdonut> 1/10 is not representable as float anyway
2025-04-28 13:47:41 +0200 <kqr> Or no, it's not
2025-04-28 13:48:02 +0200 <kqr> You're right. I was working with too little precision to detect the difference. Thanks
2025-04-28 13:48:27 +0200 <kqr> I'm guessing the toRational implementation truncates the value instead of rounding it.
2025-04-28 13:49:08 +0200 <kqr> Wow, more numbers than I thought are irrepresentable – only double-handling functions tend to round them off so I never notice.
2025-04-28 13:50:53 +0200 <opqdonut> yeah, they're interested in something like reproducability
2025-04-28 13:55:35 +0200 <opqdonut> 2.3 gets converted to float as 2.29999995231628417969, which then gets printed as 2.3 because we can know that this is the closest float to 2.3, so there can be no confusion
2025-04-28 13:56:59 +0200 <opqdonut> but there's a lot of design choices to make here, and quite a bit of old research papers written as well
2025-04-28 13:59:15 +0200 <kqr> In my case I have a bunch of old code that uses Doubles but accidentally ran into these errors in calculations, so I'm working my way through the code to convert them to fixed-precision numbers. However, in the meantime I need a way to convert back and forth between doubles and fixed precision numbers. The primitive way I tried first was fromRational . toRational but that didn't have the intended
2025-04-28 13:59:18 +0200 <kqr> effect due to the above!
2025-04-28 14:01:32 +0200 <kqr> But I think I can work around it by rounding myself at some appropriate precision.
2025-04-28 14:04:21 +0200 <tomsmeding> kqr: anything that has something in the denominator that is not a power of 2 is not representable exactly.
2025-04-28 14:05:37 +0200akegalj(~akegalj@144-188.dsl.iskon.hr) (Ping timeout: 248 seconds)
2025-04-28 14:05:46 +0200 <haskellbridge> <Liamzee> did haddock ever fix the reusable named chunk problem?
2025-04-28 14:08:14 +0200 <tomsmeding> kqr: toRational for Double simply takes the "exponent * fraction" representation that the IEEE float literally encodes, and gives you that as a Rational
2025-04-28 14:08:37 +0200 <tomsmeding> which means that the denominator of toRational on a Float or Double will always be a power of 2
2025-04-28 14:08:43 +0200 <tomsmeding> https://hackage.haskell.org/package/base-4.19.0.0/docs/src/GHC.Float.html#line-585
2025-04-28 14:23:21 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 14:27:11 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Client Quit)
2025-04-28 14:28:17 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 14:29:29 +0200TheCoffeMaker_(~TheCoffeM@186.136.173.186) (Quit: So long and thanks for all the fish)
2025-04-28 14:30:55 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Client Quit)
2025-04-28 14:31:35 +0200TheCoffeMaker(~TheCoffeM@user/thecoffemaker) TheCoffeMaker
2025-04-28 14:33:20 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 14:36:31 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 14:42:19 +0200AlexZenon(~alzenon@178.34.151.238) (Quit: ;-)
2025-04-28 14:43:07 +0200ystael(~ystael@user/ystael) ystael
2025-04-28 14:43:14 +0200akegalj(~akegalj@93-139-181-11.adsl.net.t-com.hr)
2025-04-28 14:43:30 +0200AlexNoo(~AlexNoo@178.34.151.238) (Quit: Leaving)
2025-04-28 14:45:43 +0200mari35028(~mari-este@user/mari-estel) mari-estel
2025-04-28 14:47:09 +0200tolgo(~Thunderbi@199.115.144.130)
2025-04-28 14:47:41 +0200mari-estel(~mari-este@user/mari-estel) (Read error: Connection reset by peer)
2025-04-28 14:47:44 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 14:48:00 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 14:49:07 +0200weary-traveler(~user@user/user363627) user363627
2025-04-28 14:49:56 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2025-04-28 14:52:04 +0200CiaoSen(~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds)
2025-04-28 14:52:54 +0200jespada_(~jespada@r179-25-42-1.dialup.adsl.anteldata.net.uy) jespada
2025-04-28 14:55:15 +0200jespada(~jespada@r186-49-240-45.dialup.adsl.anteldata.net.uy) (Ping timeout: 260 seconds)
2025-04-28 14:56:11 +0200visilii(~visilii@85.172.76.90) (Ping timeout: 272 seconds)
2025-04-28 14:57:55 +0200weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-04-28 14:58:20 +0200weary-traveler(~user@user/user363627) user363627
2025-04-28 14:59:26 +0200mari35028(~mari-este@user/mari-estel) (Ping timeout: 252 seconds)
2025-04-28 15:02:43 +0200mange(~user@user/mange) (Remote host closed the connection)
2025-04-28 15:04:56 +0200tolgo(~Thunderbi@199.115.144.130) (Ping timeout: 252 seconds)
2025-04-28 15:16:21 +0200chiselfuse(~chiselfus@user/chiselfuse) (Remote host closed the connection)
2025-04-28 15:16:57 +0200chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-04-28 15:22:13 +0200Square2(~Square4@user/square) Square
2025-04-28 15:25:26 +0200haritz(~hrtz@2a01:4b00:bc2e:7000::2)
2025-04-28 15:25:26 +0200haritz(~hrtz@2a01:4b00:bc2e:7000::2) (Changing host)
2025-04-28 15:25:26 +0200haritz(~hrtz@user/haritz) haritz
2025-04-28 15:26:19 +0200AlexNoo(~AlexNoo@178.34.151.238)
2025-04-28 15:29:28 +0200AlexZenon(~alzenon@178.34.151.238)
2025-04-28 15:30:15 +0200bionade24(~quassel@2a03:4000:33:45b::1) (Ping timeout: 260 seconds)
2025-04-28 15:30:23 +0200bionade24(~quassel@2a03:4000:33:45b::1) bionade24
2025-04-28 15:33:54 +0200prdak(~Thunderbi@user/prdak) (Read error: Connection reset by peer)
2025-04-28 15:36:41 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 15:39:10 +0200Teacup(~teacup@user/teacup) (Quit: No Ping reply in 180 seconds.)
2025-04-28 15:40:46 +0200Teacup(~teacup@user/teacup) Teacup
2025-04-28 15:42:31 +0200fp(~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 268 seconds)
2025-04-28 15:43:08 +0200Goodbye_Vincent1(cyvahl@freakshells.net) (Read error: Connection reset by peer)
2025-04-28 15:43:17 +0200prdak(~Thunderbi@user/prdak) (Ping timeout: 248 seconds)
2025-04-28 15:51:37 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 15:51:51 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 15:56:11 +0200Axman6(~Axman6@user/axman6) (*.net *.split)
2025-04-28 15:56:11 +0200superbil(~superbil@114-32-231-70.hinet-ip.hinet.net) (*.net *.split)
2025-04-28 15:56:11 +0200duckworld(~duckworld@user/duckworld) (*.net *.split)
2025-04-28 15:57:09 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Quit: Client closed)
2025-04-28 16:04:54 +0200fp(~Thunderbi@2001:708:20:1406::10c5) fp
2025-04-28 16:06:23 +0200notdabs(~Owner@2600:1700:69cf:9000:79ef:6a68:163c:c553)
2025-04-28 16:07:57 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 16:11:16 +0200tolgo(~Thunderbi@199.115.144.130)
2025-04-28 16:11:28 +0200tolgo(~Thunderbi@199.115.144.130) (Client Quit)
2025-04-28 16:12:34 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds)
2025-04-28 16:14:22 +0200euleritian(~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de)
2025-04-28 16:21:35 +0200 <EvanR> 2.29999995231628417969 is also not the exact decimal value, which would bit a bit longer but still finite
2025-04-28 16:23:35 +0200 <EvanR> unfortunately lambdabot doesn't have scientific to make the expansion easy
2025-04-28 16:24:53 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 248 seconds)
2025-04-28 16:27:58 +0200 <EvanR> 2.29999999999999982236431605997495353221893310546875 🤯
2025-04-28 16:28:24 +0200 <EvanR> still doesn't seem right
2025-04-28 16:30:33 +0200 <EvanR> ok
2025-04-28 16:31:45 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-04-28 16:34:26 +0200 <EvanR> 0.1000000000000000055511151231257827021181583404541015625 gotta love the "...6875" and "...5625" at the end proclaiming the arrival of a dyadic fraction
2025-04-28 16:42:31 +0200 <int-e> > truncate $ toRational 2.3 * 10^53
2025-04-28 16:42:32 +0200 <lambdabot> 229999999999999982236431605997495353221893310546875000
2025-04-28 16:42:33 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) son0p
2025-04-28 16:44:38 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk
2025-04-28 16:44:57 +0200 <EvanR> I wonder where 2.29999995231628417969 comes fro
2025-04-28 16:45:21 +0200 <EvanR> with that length
2025-04-28 16:47:04 +0200loonycyborg(loonycybor@wesnoth/developer/loonycyborg) (Read error: Connection reset by peer)
2025-04-28 16:47:22 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2025-04-28 16:50:08 +0200loonycyborg(loonycybor@wesnoth/developer/loonycyborg) loonycyborg
2025-04-28 16:50:08 +0200 <ski> "if we read something from stdin and make a type level Nat from it then can we make arbitrary compile time arithmetic on it?" -- you could read two vectors of non-empty lines, terminated by empty lines, then concatenate those two vectors, have the (statically) unknown length of the resulting vector be known to be the sum of the (statically) unknown lengths of the first two vectors
2025-04-28 16:52:29 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 245 seconds)
2025-04-28 16:52:53 +0200euphores(~SASL_euph@user/euphores) euphores
2025-04-28 16:53:04 +0200 <ski> hm, also with indexed types (similar to GADTs in Haskell), you can recover some (statically) unknown information, by matching on data constructors, this giving you information about the shape of the indices, "reflecting info from run-time back to compile-time by the `case'". this would also work if the value of the indexed data type is generated at run-time (and the indices are erased, perhaps expressed
2025-04-28 16:53:10 +0200 <ski> using existential, or the CPS encoding or data type encoding of that)
2025-04-28 16:54:37 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) son0p
2025-04-28 16:54:55 +0200 <glguy> > Data.Number.CReal.showCReal 50 (realToFrac 2.3)
2025-04-28 16:54:57 +0200 <lambdabot> "2.29999999999999982236431605997495353221893310546875"
2025-04-28 16:55:10 +0200 <int-e> EvanR: this.max_digits = 21 in FloatConfig() in Float.js (doesn't count the decimal point)
2025-04-28 16:55:27 +0200 <int-e> > length "2.29999995231628417969"
2025-04-28 16:55:28 +0200 <lambdabot> 22
2025-04-28 16:55:59 +0200 <int-e> (doesn't count leading zeros either)
2025-04-28 16:56:38 +0200 <int-e> EvanR: so it's due to how that float.exposed website works
2025-04-28 16:57:07 +0200 <EvanR> oh
2025-04-28 16:58:49 +0200 <EvanR> that's decidedly larger than DBL_DECIMAL_DIG on my computer (17)
2025-04-28 16:59:38 +0200 <EvanR> ... but it is equal to LDBL_DECIMAL_DIG
2025-04-28 17:00:32 +0200 <EvanR> javascript assuming extended precision? 😱
2025-04-28 17:01:09 +0200MironZ38(~MironZ@nat-infra.ehlab.uk)
2025-04-28 17:02:06 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 17:03:05 +0200 <EvanR> > Data.Number.CReal.showCReal 50 (realToFrac 0.1)
2025-04-28 17:03:07 +0200 <lambdabot> "0.1000000000000000055511151231257827021181583404541"
2025-04-28 17:03:13 +0200MironZ3(~MironZ@nat-infra.ehlab.uk) (Ping timeout: 248 seconds)
2025-04-28 17:03:14 +0200MironZ38MironZ3
2025-04-28 17:03:18 +0200 <EvanR> so you have to "already know" the 50 to make that work
2025-04-28 17:03:27 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) Unicorn_Princess
2025-04-28 17:03:59 +0200 <EvanR> > Data.Number.CReal.showCReal 55 (realToFrac 0.1)
2025-04-28 17:04:00 +0200 <lambdabot> "0.1000000000000000055511151231257827021181583404541015625"
2025-04-28 17:06:29 +0200kuribas(~user@ptr-17d51emz2h3kcoowrgl.18120a2.ip6.access.telenet.be) kuribas
2025-04-28 17:08:02 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2025-04-28 17:10:32 +0200 <tomsmeding> > Data.Number.CReal.showCReal 60 (realToFrac 0.1)
2025-04-28 17:10:33 +0200 <lambdabot> "0.1000000000000000055511151231257827021181583404541015625"
2025-04-28 17:11:04 +0200 <tomsmeding> turns out the correct answer was 55?
2025-04-28 17:11:17 +0200 <tomsmeding> wait why does '55' give 6 more digits than '50'
2025-04-28 17:12:01 +0200 <EvanR> > Data.Number.CReal.showCReal 54 (realToFrac 0.1)
2025-04-28 17:12:03 +0200 <lambdabot> "0.100000000000000005551115123125782702118158340454101563"
2025-04-28 17:12:22 +0200 <int-e> > Data.Number.CReal.showCReal 56 (realToFrac 0.10000000000000002)
2025-04-28 17:12:23 +0200 <EvanR> maybe 50 ends in a zero
2025-04-28 17:12:24 +0200 <lambdabot> "0.10000000000000001942890293094023945741355419158935546875"
2025-04-28 17:12:34 +0200 <tomsmeding> that makes sense
2025-04-28 17:13:19 +0200 <int-e> (56 is the safe value to use for numbers between 0.0625 and 0.125; turns out the final mantissa digit for 0.1 is 0)
2025-04-28 17:13:42 +0200 <EvanR> I just noticed earlier that the expansion for 0.1 had 5 more digits than 2.3 so I "already knew" the 55
2025-04-28 17:13:48 +0200 <tomsmeding> not the final one, right? Just the 50th
2025-04-28 17:14:27 +0200 <tomsmeding> > [length (Data.Number.CReal.showCReal n (realToFrac 0.1)) | n <- [48 .. 58]]
2025-04-28 17:14:28 +0200 <lambdabot> [50,51,51,53,54,55,56,57,57,57,57]
2025-04-28 17:15:02 +0200 <int-e> > [length (Data.Number.CReal.showCReal n (realToFrac
2025-04-28 17:15:04 +0200 <lambdabot> <hint>:1:52: error:
2025-04-28 17:15:04 +0200 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
2025-04-28 17:15:06 +0200 <int-e> 0.1)) | n <- [48 .. 58]]
2025-04-28 17:15:09 +0200 <int-e> meh
2025-04-28 17:15:11 +0200 <tomsmeding> :)
2025-04-28 17:15:57 +0200 <int-e> > [length (Data.Number.CReal.showCReal n (realToFrac 0.10000000000000002)) | n <- [48 .. 58]]
2025-04-28 17:15:58 +0200 <lambdabot> [50,51,52,53,54,55,56,57,58,58,58]
2025-04-28 17:16:18 +0200 <tomsmeding> ah, so the 50th _and_ the 56th
2025-04-28 17:16:57 +0200 <tomsmeding> EvanR: your 50 confused everyone, it's your fault
2025-04-28 17:17:08 +0200 <EvanR> that was glguy
2025-04-28 17:17:10 +0200 <tomsmeding> (everyone = me)
2025-04-28 17:17:13 +0200 <tomsmeding> oh
2025-04-28 17:17:31 +0200 <int-e> it didn't confuse me because I didn't even think about were that 50 came from :-P
2025-04-28 17:17:37 +0200 <int-e> where
2025-04-28 17:18:13 +0200 <EvanR> enough magic numbers, I will now see about computing this with like 5 APL symbols
2025-04-28 17:19:36 +0200 <int-e> 53 is the magic number here, from 52 mantissa bits, plus 1 for the mostly fixed leading 1. The rest is just keeping track of the floating point exponent.
2025-04-28 17:20:11 +0200 <EvanR> that's base 2
2025-04-28 17:20:16 +0200 <tomsmeding> yes
2025-04-28 17:20:28 +0200 <tomsmeding> the number of decimal digits of 1/2^n is n
2025-04-28 17:20:37 +0200 <tomsmeding> behind the decimal points, that is
2025-04-28 17:20:42 +0200 <tomsmeding> decimal decimal digits?
2025-04-28 17:20:56 +0200 <tomsmeding> 0.5 0.25 0.125 0.0625
2025-04-28 17:21:06 +0200 <EvanR> yes so it doesn't let you predict the length of the above strings exactly
2025-04-28 17:21:28 +0200 <tomsmeding> apart from a possible trailing 0, it does
2025-04-28 17:21:28 +0200 <int-e> EvanR: 10 = 5*2, so each factor 10 cancels out a factor of 2 from a fraction whose denominator is a power of 2
2025-04-28 17:21:30 +0200 <EvanR> > Data.Number.CReal.showCReal 61 (realToFrac 0.00001)
2025-04-28 17:21:31 +0200 <lambdabot> "0.0000100000000000000008180305391403130954586231382563710212708"
2025-04-28 17:21:59 +0200 <int-e> EvanR: so keeping track of that power of 2 tells you how many decimal digits you need
2025-04-28 17:22:09 +0200 <EvanR> the number of binary digits of 1/2^n is n, what were you talking about
2025-04-28 17:22:15 +0200 <tomsmeding> yes
2025-04-28 17:22:16 +0200 <int-e> > logBase 0.5 0.00001
2025-04-28 17:22:17 +0200 <lambdabot> 16.609640474436812
2025-04-28 17:22:20 +0200 <tomsmeding> and the number of _decimal_ digits is, too
2025-04-28 17:22:20 +0200 <EvanR> you said decimal
2025-04-28 17:22:24 +0200 <EvanR> o_O
2025-04-28 17:22:33 +0200 <int-e> > Data.Number.CReal.showCReal (53 + 16) (realToFrac 0.00001)
2025-04-28 17:22:34 +0200 <lambdabot> "0.000010000000000000000818030539140313095458623138256371021270751953125"
2025-04-28 17:23:18 +0200 <tomsmeding> Claim: if n >= 1 then the last digit is always 5. Claim: length of decimal expansion is n. Both admit a simple proof by induction :)
2025-04-28 17:23:39 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2025-04-28 17:23:39 +0200 <int-e> (It worked, but I should be using 17.)
2025-04-28 17:24:15 +0200 <int-e> it's almost as if 1/2^n = 5^n/10^n
2025-04-28 17:24:24 +0200 <int-e> call me crazy, but I think that's actually true
2025-04-28 17:24:26 +0200 <int-e> ;-)
2025-04-28 17:24:29 +0200 <EvanR> each time you multiply by 1/10 you get a nother power of two
2025-04-28 17:24:35 +0200 <EvanR> but also a power of 5
2025-04-28 17:24:49 +0200 <EvanR> not obvious to me
2025-04-28 17:25:29 +0200 <int-e> once you understand it it will be obvious ;)
2025-04-28 17:25:33 +0200 <tomsmeding> > 5 ^ 20
2025-04-28 17:25:34 +0200 <lambdabot> 95367431640625
2025-04-28 17:25:39 +0200 <EvanR> tautology 37
2025-04-28 17:25:49 +0200 <tomsmeding> > Data.Number.CReal.showCReal (53 + 16) (1 % 2^20)
2025-04-28 17:25:51 +0200 <lambdabot> error:
2025-04-28 17:25:51 +0200 <lambdabot> • Couldn't match expected type ‘CReal’ with actual type ‘Ratio a0’
2025-04-28 17:25:51 +0200 <lambdabot> • In the second argument of ‘showCReal’, namely ‘(1 % 2 ^ 20)’
2025-04-28 17:25:58 +0200 <EvanR> k powers of 5 end in 5
2025-04-28 17:25:59 +0200 <tomsmeding> > Data.Number.CReal.showCReal (53 + 16) (realToFrac (1 % 2^20))
2025-04-28 17:26:00 +0200 <lambdabot> "0.00000095367431640625"
2025-04-28 17:26:02 +0200 <EvanR> in decimal
2025-04-28 17:26:13 +0200 <tomsmeding> these two numbers are alike
2025-04-28 17:26:35 +0200 <int-e> EvanR: Right. I mean it's not *quite* tautological... you may understand a complicated thing and it still won't be obvious. But this particular factoid isn't complicated.
2025-04-28 17:27:35 +0200 <EvanR> I mean "if you understand it it's obvious"
2025-04-28 17:27:44 +0200 <int-e> Same here.
2025-04-28 17:28:22 +0200 <tomsmeding> > and [Data.Number.CReal.showCReal 80 (realToFrac (1 % 2^n)) == "0." ++ (let s = show (5^n) in replicate (n - length s) '0' ++ s) | n <- [1..50]]
2025-04-28 17:28:23 +0200 <lambdabot> True
2025-04-28 17:28:36 +0200[exa]reminded of that "zeros at the end of factorial" exercise
2025-04-28 17:29:19 +0200 <tomsmeding> "dividing by powers of 2 is easy. Just exponentiate 5 and add some zeros"
2025-04-28 17:29:23 +0200 <EvanR> :t showCReal -- now with more unqualified
2025-04-28 17:29:24 +0200 <lambdabot> Int -> CReal -> String
2025-04-28 17:30:23 +0200 <EvanR> fine I'll use paper
2025-04-28 17:30:25 +0200 <tomsmeding> anyway this checks the claim for 1 <= n <= 50 :p
2025-04-28 17:30:42 +0200 <int-e> [exa]: do you know the variant for binomial coefficients, https://en.wikipedia.org/wiki/Lucas%27s_theorem ?
2025-04-28 17:31:02 +0200 <EvanR> check it for n up to 10^900 and I'll start to be convinced (just kidding)
2025-04-28 17:31:14 +0200prdak(~Thunderbi@user/prdak) (Read error: Connection reset by peer)
2025-04-28 17:31:18 +0200 <tomsmeding> it does show where int-e's powers of 5 end up
2025-04-28 17:32:23 +0200 <tomsmeding> EvanR: 1/2^n is an integer multiple of 1/10^n: the multiple is 5^n, because 5^n * 1/10^n = (1/2)^n = 1/2^n
2025-04-28 17:32:55 +0200 <tomsmeding> furthermore, that multiplier (5^n) is not divisible by 10 ever because it has no factors of 2, so 1/2^n is not an integer multiple of 1/10^(n-1)
2025-04-28 17:33:09 +0200 <tomsmeding> so you need n decimal decimal digits to represent 1/2^n
2025-04-28 17:34:12 +0200 <int-e> . o O ( for n > 0 we have 5^n = 1^n = 1 (mod 2) and 5^n = 0 (mod 5), so by the Chinese Remainder Theorem, 5^n = 5 (mod 10) -- scnr )
2025-04-28 17:34:19 +0200 <EvanR> "decimal decimal" ??
2025-04-28 17:34:29 +0200 <tomsmeding> decimal digits behind the decimal point
2025-04-28 17:34:35 +0200 <EvanR> oh
2025-04-28 17:35:25 +0200 <int-e> > [0..] >>= last . show . (5^)
2025-04-28 17:35:26 +0200 <lambdabot> error:
2025-04-28 17:35:26 +0200 <lambdabot> • Couldn't match type ‘Char’ with ‘[b]’
2025-04-28 17:35:26 +0200 <lambdabot> Expected type: b0 -> [b]
2025-04-28 17:35:45 +0200 <tomsmeding> too free
2025-04-28 17:36:11 +0200 <tomsmeding> > [0..] >>= pure . last . show . (5^)
2025-04-28 17:36:12 +0200 <lambdabot> "155555555555555555555555555555555555555555555555555555555555555555555555555...
2025-04-28 17:36:26 +0200 <EvanR> proof by exhaustion
2025-04-28 17:36:27 +0200 <tomsmeding> > last . show . (5^) <$> [0..]
2025-04-28 17:36:29 +0200 <lambdabot> "155555555555555555555555555555555555555555555555555555555555555555555555555...
2025-04-28 17:46:04 +0200byte(~mu@user/byte) (Read error: Connection reset by peer)
2025-04-28 17:48:48 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Quit: Client closed)
2025-04-28 17:49:32 +0200 <EvanR> I was down a rabbit hole on the wrong question, how to divide by dyadic fraction by 5 and get back a dyadic fraction
2025-04-28 17:49:48 +0200 <EvanR> which is impossible
2025-04-28 17:49:54 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) tzh
2025-04-28 17:50:05 +0200 <EvanR> and nobody was doing it anyway!
2025-04-28 17:50:10 +0200 <EvanR> smh
2025-04-28 17:55:29 +0200akegalj(~akegalj@93-139-181-11.adsl.net.t-com.hr) (Quit: leaving)
2025-04-28 18:03:40 +0200CalimeroTeknik(~calimero@ctkarch.org) (Changing host)
2025-04-28 18:03:40 +0200CalimeroTeknik(~calimero@user/calimeroteknik) CalimeroTeknik
2025-04-28 18:06:42 +0200 <EvanR> every float has a decimal form: assuming n/2^k where 2^k <= n < 2^(k+1), multiply by 5^k/5^k to get 5^k n / 10^k where 10^k <= 5^k n < 2 * 10^k
2025-04-28 18:06:56 +0200 <EvanR> though it might need to be adjusted to be a proper decimal float
2025-04-28 18:07:17 +0200 <EvanR> changing the number of digits a few
2025-04-28 18:08:41 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 18:08:58 +0200 <EvanR> shoot if k is negative that fails
2025-04-28 18:09:16 +0200euleritian(~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-28 18:09:34 +0200euleritian(~euleritia@77.23.248.47)
2025-04-28 18:13:32 +0200 <EvanR> if k is negative those are integer equations nvm
2025-04-28 18:15:42 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
2025-04-28 18:16:41 +0200chele(~chele@user/chele) (Remote host closed the connection)
2025-04-28 18:18:19 +0200acarrico(~acarrico@pppoe-209-99-221-107.greenmountainaccess.net)
2025-04-28 18:20:01 +0200comerijn(~merijn@77.242.116.146) (Ping timeout: 248 seconds)
2025-04-28 18:20:21 +0200 <EvanR> I"m wrong < 2*10^k < 10^(k+1) so it's even a proper decimal float
2025-04-28 18:21:45 +0200 <tomsmeding> it is
2025-04-28 18:22:09 +0200 <tomsmeding> in my formulation, 1/2^n = 5^n * 1/10^n, and 5^n does not end in a zero for any n >= 0
2025-04-28 18:22:26 +0200 <tomsmeding> oh my n is your k
2025-04-28 18:22:50 +0200euleritian(~euleritia@77.23.248.47) (Read error: Connection reset by peer)
2025-04-28 18:23:38 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 18:24:06 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2025-04-28 18:28:04 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-04-28 18:28:26 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 18:28:55 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 18:35:45 +0200 <EvanR> so all floats end up between "ten and twenty" before the power of ten jumps
2025-04-28 18:36:14 +0200 <EvanR> you won't see the decimal form starting with 3
2025-04-28 18:36:45 +0200 <EvanR> k that can't be right
2025-04-28 18:37:03 +0200 <int-e> > 2^^(-5)
2025-04-28 18:37:04 +0200 <lambdabot> 3.125e-2
2025-04-28 18:37:14 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
2025-04-28 18:37:22 +0200euleritian(~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de)
2025-04-28 18:39:51 +0200 <EvanR> that's not between 10^k and 2*10^k ...
2025-04-28 18:40:13 +0200euleritian(~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
2025-04-28 18:40:30 +0200euleritian(~euleritia@77.23.248.47)
2025-04-28 18:44:04 +0200 <EvanR> I forgot to handle the exponent
2025-04-28 18:44:18 +0200 <EvanR> but
2025-04-28 18:47:08 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
2025-04-28 18:47:23 +0200Googulator47(~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
2025-04-28 18:51:01 +0200euleritian(~euleritia@77.23.248.47) (Ping timeout: 248 seconds)
2025-04-28 18:51:50 +0200fp(~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 268 seconds)
2025-04-28 18:53:12 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
2025-04-28 19:00:52 +0200econo_(uid147250@id-147250.tinside.irccloud.com)
2025-04-28 19:03:54 +0200Buliarous(~gypsydang@46.232.210.139) (Remote host closed the connection)
2025-04-28 19:04:23 +0200Buliarous(~gypsydang@46.232.210.139) Buliarous
2025-04-28 19:06:29 +0200wootehfoot(~wootehfoo@user/wootehfoot) wootehfoot
2025-04-28 19:10:32 +0200 <EvanR> ok yeah adding in the exponential factor leads to a decimal form but not necessarily normalized
2025-04-28 19:13:38 +0200jco(~jco@78-70-217-44-no600.tbcn.telia.com) jco
2025-04-28 19:15:16 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de)
2025-04-28 19:18:39 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net) alexherbo2
2025-04-28 19:21:19 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-28 19:25:47 +0200ft(~ft@p4fc2a6e6.dip0.t-ipconnect.de) ft
2025-04-28 19:28:29 +0200_d0t(~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 265 seconds)
2025-04-28 19:30:54 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
2025-04-28 19:31:34 +0200 <tomsmeding> EvanR: all floats end up between 10 and 100 in binary, yes
2025-04-28 19:31:51 +0200 <tomsmeding> after multiplying by a power of 2
2025-04-28 19:32:00 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
2025-04-28 19:32:09 +0200 <tomsmeding> which could have been on https://www.vex.net/~trebla/humour/tautologies.html
2025-04-28 19:32:26 +0200_d0t(~{-d0t-}@user/-d0t-/x-7915216) {-d0t-}
2025-04-28 19:36:39 +0200_d0t(~{-d0t-}@user/-d0t-/x-7915216) (Remote host closed the connection)
2025-04-28 19:37:29 +0200_d0t(~{-d0t-}@user/-d0t-/x-7915216) {-d0t-}
2025-04-28 19:48:45 +0200justsomeguy(~justsomeg@user/justsomeguy) justsomeguy
2025-04-28 19:51:46 +0200TMA(tma@twin.jikos.cz) (Ping timeout: 276 seconds)
2025-04-28 19:55:42 +0200mistivia_(~mistivia@user/mistivia) (Ping timeout: 252 seconds)
2025-04-28 19:55:43 +0200mistivia(~mistivia@user/mistivia) mistivia
2025-04-28 19:59:15 +0200wootehfoot(~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
2025-04-28 20:01:10 +0200ljdarj(~Thunderbi@user/ljdarj) ljdarj
2025-04-28 20:02:00 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 20:02:02 +0200fp(~Thunderbi@87-94-239-173.bb.dnainternet.fi) fp
2025-04-28 20:04:35 +0200mceresa(~mceresa@user/mceresa) mceresa
2025-04-28 20:17:06 +0200superbil(~superbil@114-32-231-70.hinet-ip.hinet.net) superbil
2025-04-28 20:17:06 +0200duckworld(~duckworld@user/duckworld) duckworld
2025-04-28 20:17:06 +0200Axman6(~Axman6@user/axman6) Axman6
2025-04-28 20:19:04 +0200fp(~Thunderbi@87-94-239-173.bb.dnainternet.fi) (Ping timeout: 276 seconds)
2025-04-28 20:20:07 +0200jco(~jco@78-70-217-44-no600.tbcn.telia.com) (Quit: leaving)
2025-04-28 20:20:39 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net) (Remote host closed the connection)
2025-04-28 20:20:48 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net) alexherbo2
2025-04-28 20:21:15 +0200JuanDaugherty(~juan@user/JuanDaugherty) JuanDaugherty
2025-04-28 20:23:46 +0200alexherbo2(~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net) (Remote host closed the connection)