2025/04/28

Newest at the top

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:14 +0200MironZ38MironZ3
2025-04-28 17:03:13 +0200MironZ3(~MironZ@nat-infra.ehlab.uk) (Ping timeout: 248 seconds)
2025-04-28 17:03:07 +0200 <lambdabot> "0.1000000000000000055511151231257827021181583404541"
2025-04-28 17:03:05 +0200 <EvanR> > Data.Number.CReal.showCReal 50 (realToFrac 0.1)
2025-04-28 17:02:06 +0200prdak(~Thunderbi@user/prdak) prdak
2025-04-28 17:01:09 +0200MironZ38(~MironZ@nat-infra.ehlab.uk)
2025-04-28 17:00:32 +0200 <EvanR> javascript assuming extended precision? 😱
2025-04-28 16:59:38 +0200 <EvanR> ... but it is equal to LDBL_DECIMAL_DIG
2025-04-28 16:58:49 +0200 <EvanR> that's decidedly larger than DBL_DECIMAL_DIG on my computer (17)
2025-04-28 16:57:07 +0200 <EvanR> oh
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:55:59 +0200 <int-e> (doesn't count leading zeros either)
2025-04-28 16:55:28 +0200 <lambdabot> 22
2025-04-28 16:55:27 +0200 <int-e> > length "2.29999995231628417969"
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:54:57 +0200 <lambdabot> "2.29999999999999982236431605997495353221893310546875"
2025-04-28 16:54:55 +0200 <glguy> > Data.Number.CReal.showCReal 50 (realToFrac 2.3)
2025-04-28 16:54:37 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) son0p
2025-04-28 16:53:10 +0200 <ski> using existential, or the CPS encoding or data type encoding of that)
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:52:53 +0200euphores(~SASL_euph@user/euphores) euphores
2025-04-28 16:52:29 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 245 seconds)
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:50:08 +0200loonycyborg(loonycybor@wesnoth/developer/loonycyborg) loonycyborg
2025-04-28 16:47:22 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2025-04-28 16:47:04 +0200loonycyborg(loonycybor@wesnoth/developer/loonycyborg) (Read error: Connection reset by peer)
2025-04-28 16:45:21 +0200 <EvanR> with that length
2025-04-28 16:44:57 +0200 <EvanR> I wonder where 2.29999995231628417969 comes fro
2025-04-28 16:44:38 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) acidjnk
2025-04-28 16:42:33 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) son0p
2025-04-28 16:42:32 +0200 <lambdabot> 229999999999999982236431605997495353221893310546875000
2025-04-28 16:42:31 +0200 <int-e> > truncate $ toRational 2.3 * 10^53
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:31:45 +0200acidjnk_new(~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-04-28 16:30:33 +0200 <EvanR> ok
2025-04-28 16:28:24 +0200 <EvanR> still doesn't seem right
2025-04-28 16:27:58 +0200 <EvanR> 2.29999999999999982236431605997495353221893310546875 🤯
2025-04-28 16:24:53 +0200son0p(~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 248 seconds)
2025-04-28 16:23:35 +0200 <EvanR> unfortunately lambdabot doesn't have scientific to make the expansion easy
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:14:22 +0200euleritian(~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de)
2025-04-28 16:12:34 +0200euleritian(~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds)
2025-04-28 16:11:28 +0200tolgo(~Thunderbi@199.115.144.130) (Client Quit)
2025-04-28 16:11:16 +0200tolgo(~Thunderbi@199.115.144.130)
2025-04-28 16:07:57 +0200LainIwakura(~LainIwaku@user/LainIwakura) LainIwakura
2025-04-28 16:06:23 +0200notdabs(~Owner@2600:1700:69cf:9000:79ef:6a68:163c:c553)
2025-04-28 16:04:54 +0200fp(~Thunderbi@2001:708:20:1406::10c5) fp
2025-04-28 15:57:09 +0200LainIwakura(~LainIwaku@user/LainIwakura) (Quit: Client closed)
2025-04-28 15:56:11 +0200duckworld(~duckworld@user/duckworld) (*.net *.split)