Home liberachat/#haskell: Logs Calendar

Logs on 2025-04-28 (liberachat/#haskell)

00:01:21 <EvanR> the conflation between arithmetic on literal types is a haskell thing because it's weird type level hacks
00:01:35 <EvanR> you don't want to do this
00:01:47 <EvanR> outside haskell
00:04:17 <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
00:04:58 × jespada_ quits (~jespada@r186-49-245-168.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds)
00:05:30 <EvanR> you can read chars or Word8 from stdin I would believe that
00:06:15 <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
00:06:25 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
00:06:41 <haskellbridge> <loonycyborg> * typed
00:06:48 <EvanR> python's dynamic types cause the program to crash if a type check fails
00:06:55 <EvanR> that wouldn't happen
00:07:16 <EvanR> the program itself can be well typed while still juggling types at runtime
00:07:26 <EvanR> (for whatever reason)
00:10:17 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds)
00:13:56 → euleritian joins (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
00:17:44 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
00:18:20 <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.
00:18:37 → __jmcantrell__ joins (~weechat@user/jmcantrell)
00:19:34 → OftenFaded joins (~OftenFade@user/tisktisk)
00:23:38 <haskellbridge> <loonycyborg> Practical case would be serialization: can you construct your data entirely based on something you de-serialize with dependent types?
00:24:06 <haskellbridge> <loonycyborg> Probably if your program operates on such types then it wouldn't be too optimized
00:24:22 <haskellbridge> <loonycyborg> because compiler doesn't know anything about actual data that will be read
00:24:26 <haskellbridge> <loonycyborg> unless it'sJIT
00:24:47 <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.
00:27:28 <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 ().
00:30:10 <monochrom> s/pass n and v/pass n and the vector/
00:34:01 <monochrom> You are reminding me of that joke (or true story) about C++ back then.
00:34:57 <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.
00:35:31 <geekosaur> true story and done multiple times by multiple people
00:36:03 <geekosaur> (one of whom was a CS postgrad at C-MU who replicated it after hearing about the original)
00:36:55 <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?
00:37:59 → xff0x joins (~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a)
00:38:13 → sim590 joins (~simon@209-15-185-101.resi.cgocable.ca)
00:40:38 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Remote host closed the connection)
00:41:22 → haritz joins (~hrtz@152.37.68.178)
00:41:22 × haritz quits (~hrtz@152.37.68.178) (Changing host)
00:41:22 → haritz joins (~hrtz@user/haritz)
00:41:31 × otto_s quits (~user@p5de2f428.dip0.t-ipconnect.de) (Ping timeout: 276 seconds)
00:44:56 <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. >:)
00:50:48 → otto_s joins (~user@p4ff27ad7.dip0.t-ipconnect.de)
00:51:55 <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
00:54:12 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
00:55:26 × __jmcantrell__ quits (~weechat@user/jmcantrell) (Ping timeout: 272 seconds)
00:57:40 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
00:59:48 × machinedgod quits (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 276 seconds)
01:00:51 → j1n37 joins (~j1n37@user/j1n37)
01:02:41 × acidjnk_new quits (~acidjnk@p200300d6e71c4f29a1deb7f42d1df083.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
01:03:32 <mauke> #include "/dev/tty" // please type the correct code
01:05:52 <int-e> Ah yeah the good old 1988 IOCCC entry.
01:07:04 × weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!)
01:07:21 → weary-traveler joins (~user@user/user363627)
01:13:51 → OftenFaded9 joins (~OftenFade@user/tisktisk)
01:14:54 × OftenFaded quits (~OftenFade@user/tisktisk) (Ping timeout: 240 seconds)
01:15:19 × bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity)
01:15:30 × OftenFaded9 quits (~OftenFade@user/tisktisk) (Client Quit)
01:18:07 <monochrom> Oh hahaha
01:21:14 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds)
01:22:28 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
01:28:53 → snoopy1 joins (~Thunderbi@199.115.144.130)
01:33:06 × euleritian quits (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
01:33:24 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
01:33:39 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
01:34:35 × hgolden quits (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e) (Remote host closed the connection)
01:37:01 → hgolden joins (~hgolden@2603:8000:9d00:3ed1:88e0:76ff:fe9c:b21e)
01:42:10 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
01:42:31 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
01:44:24 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds)
01:44:54 → j1n37 joins (~j1n37@user/j1n37)
01:48:48 × notdabs quits (~Owner@2600:1700:69cf:9000:c531:a8cf:57a8:ee6f) (Quit: Leaving)
01:55:03 × xff0x quits (~xff0x@2409:251:9040:2c00:aeeb:2fa9:beb7:eb2a) (Ping timeout: 276 seconds)
01:55:24 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
02:19:59 → Guest85 joins (~Guest85@83.234.227.67)
02:20:37 × td_ quits (~td@i5387092A.versanet.de) (Ping timeout: 248 seconds)
02:21:32 × Guest85 quits (~Guest85@83.234.227.67) (Client Quit)
02:22:13 → td_ joins (~td@i53870908.versanet.de)
02:29:46 × snoopy1 quits (~Thunderbi@199.115.144.130) (Quit: snoopy1)
02:30:04 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 276 seconds)
02:30:24 → euleritian joins (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
02:37:52 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
02:45:25 → bitdex joins (~bitdex@gateway/tor-sasl/bitdex)
02:48:47 × euleritian quits (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
02:49:05 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
02:49:47 × Square quits (~Square@user/square) (Ping timeout: 265 seconds)
02:50:05 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
02:50:18 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
02:51:08 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
02:56:45 × Unicorn_Princess quits (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
03:01:43 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
03:03:40 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
03:03:56 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
03:12:21 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
03:12:38 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
03:30:21 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
03:31:45 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
03:32:37 → koz joins (~koz@121.99.240.58)
03:35:16 → cbs joins (df2953d28a@2a03:6000:1812:100::1451)
03:36:08 ← cbs parts (df2953d28a@2a03:6000:1812:100::1451) ()
03:38:38 <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
03:41:32 <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
03:41:51 <haskellbridge> <Bowuigi> Also that's partly why dependent haskell takes so much effort
03:42:37 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
03:43:53 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
03:45:42 <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
03:50:57 <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...
03:51:02 <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.
03:52:23 <haskellbridge> <Bowuigi> Suddenly to get a chance of using the newest features you need a PhD because progress is not quite there yet
03:52:25 <ames> seems very strange to assume that this is a common thing to do when there's exactly one language that's done that
03:54:01 <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
03:54:36 <ames> it's erasing the things that *aren't* types e.g. lengths of vectors that's complicated
03:54:58 <haskellbridge> <Bowuigi> I see
03:55:42 <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
03:57:59 <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
03:58:05 <ames> coq does not have anything approaching a cubical mode and jon's proof assistants are basically proofs-of-concept
03:58:54 <ames> "make three to throw away" and all that
03:59:56 <haskellbridge> <Bowuigi> The previous steps (inductive-inductive and inductive-recursive stuff) were added / are in progress because of user demand in Coq AFAIU
04:00:37 <ames> "previous steps" - those are completely orthogonal features.
04:03:40 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Quit: Client closed)
04:05:30 <haskellbridge> <Bowuigi> Yeah that's the idea
04:06:13 <haskellbridge> <Bowuigi> Can't find the IIT/IRT stuff on the Coq issues but I remember some talk about supporting them exists lol
04:06:25 <haskellbridge> <Bowuigi> I should take more notes
04:10:18 <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
04:11:35 <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
04:16:01 <haskellbridge> <Liamzee> huh, that's interesting, and probably extremely degenerate
04:16:16 <haskellbridge> <Liamzee> you know how emojis are actually part of the haskell operator namespace?
04:16:56 <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. :)
04:18:55 <ames> i think some emoji should be uppercase so we can use them as constructors
04:27:36 × gorignak quits (~gorignak@user/gorignak) (Quit: quit)
04:27:48 → gorignak joins (~gorignak@user/gorignak)
04:29:30 → LainIwakura joins (~LainIwaku@user/LainIwakura)
04:34:48 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:37:40 × polykernel quits (~polykerne@user/polykernel) (Remote host closed the connection)
04:38:49 → polykernel joins (~polykerne@user/polykernel)
04:40:04 → j1n37 joins (~j1n37@user/j1n37)
04:40:39 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Quit: Client closed)
04:43:49 → LainIwakura joins (~LainIwaku@user/LainIwakura)
04:44:12 → michalz joins (~michalz@185.246.207.218)
04:44:13 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:44:44 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Write error: Broken pipe)
04:47:13 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
04:47:58 → j1n37 joins (~j1n37@user/j1n37)
04:49:38 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:51:32 → j1n37 joins (~j1n37@user/j1n37)
04:52:52 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
04:56:03 → j1n37 joins (~j1n37@user/j1n37)
04:58:02 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
04:58:37 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
05:00:51 × jacopovalanzano quits (~jacopoval@cpc151911-cove17-2-0-cust105.3-1.cable.virginm.net) (Quit: Client closed)
05:01:40 <EvanR> or lowercase so we can use them as variables
05:02:54 → j1n37 joins (~j1n37@user/j1n37)
05:03:57 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
05:07:05 → j1n37 joins (~j1n37@user/j1n37)
05:09:38 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
05:14:08 → prdak joins (~Thunderbi@user/prdak)
05:17:15 → takuan joins (~takuan@d8D86B601.access.telenet.be)
05:26:44 → harveypwca joins (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c)
05:30:45 → j1n37 joins (~j1n37@user/j1n37)
05:33:14 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
05:36:52 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
05:37:38 → euleritian joins (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de)
05:39:00 → j1n37 joins (~j1n37@user/j1n37)
05:42:03 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
05:42:53 × haritz quits (~hrtz@user/haritz) (Quit: ZNC 1.8.2+deb3.1+deb12u1 - https://znc.in)
05:47:07 → j1n37 joins (~j1n37@user/j1n37)
05:53:36 × j1n37 quits (~j1n37@user/j1n37) (Read error: Connection reset by peer)
05:56:38 → j1n37 joins (~j1n37@user/j1n37)
05:59:04 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
05:59:19 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
06:05:01 × Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer)
06:11:06 → jco joins (~jco@78-70-217-44-no600.tbcn.telia.com)
06:12:32 <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...?
06:13:12 <geekosaur> @hackage binary
06:13:12 <lambdabot> https://hackage.haskell.org/package/binary
06:13:16 <geekosaur> @hackage cereal
06:13:16 <lambdabot> https://hackage.haskell.org/package/cereal
06:14:25 <jco> geekosaur: Thanks a lot.
06:15:01 × haskellbridge quits (~hackager@syn-024-093-192-219.res.spectrum.com) (Remote host closed the connection)
06:18:13 × pabs3 quits (~pabs3@user/pabs3) (Ping timeout: 276 seconds)
06:20:40 <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
06:22:35 → CiaoSen joins (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db)
06:22:48 → chele joins (~chele@user/chele)
06:24:34 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Quit: peterbecich)
06:24:51 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
06:27:18 → tromp joins (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
06:29:55 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 276 seconds)
06:34:23 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
06:44:24 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
06:48:18 → halloy3041 joins (~halloy304@2001:569:76fd:b00:ada3:3d53:48e5:4f37)
06:50:29 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
06:51:39 × ft quits (~ft@p4fc2a6e6.dip0.t-ipconnect.de) (Quit: leaving)
06:55:41 × tromp quits (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…)
06:55:47 → acidjnk_new joins (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de)
06:57:59 → __monty__ joins (~toonn@user/toonn)
07:00:03 × caconym7 quits (~caconym@user/caconym) (Quit: bye)
07:00:42 → caconym7 joins (~caconym@user/caconym)
07:03:03 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
07:03:36 → haskellbridge joins (~hackager@syn-024-093-192-219.res.spectrum.com)
07:03:36 <haskellbridge> <hellwolf> "less mainstream logics"
07:03:36 <haskellbridge> <Bowuigi> Oh, mainstream here means popular, in a sense
07:03:36 <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
07:03:36 ChanServ sets mode +v haskellbridge
07:03:45 <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"?
07:03:47 <haskellbridge> <hellwolf> anyhow, not going to far,
07:03:49 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/crunkvuyNAgcnoaGKHVPavQw/HhaisemMfmk (5 lines)
07:03:50 <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
07:03:52 <haskellbridge> <Bowuigi> Proofs about type systems are the proofs I read the most, I like how easy it is to do those in Twelf
07:03:54 <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
07:03:56 <haskellbridge> <Bowuigi> (Those are independent replies from 1 to 3, in order)
07:03:57 <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
07:03:59 <haskellbridge> <hellwolf> "less run time error" is probably the "KPI"
07:04:01 <haskellbridge> <hellwolf> interesting dependent types thread...
07:04:02 <haskellbridge> What's the healthy level of proofs that you would put in Haskell?
07:04:04 <haskellbridge> <Bowuigi> Up to and including the base constructs seems good enough I guess
07:04:05 <haskellbridge> <hellwolf> - propositional logic <-> static types (?)
07:04:07 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/UEPByodBGyiSVOqodXeCtYPh/LKR6AzyTcQ4 (3 lines)
07:04:08 <haskellbridge> <Bowuigi> Actually dependency in user-defined ADTs is good. With base constructs I mean pi and sigma types
07:04:10 <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?
07:04:12 <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
07:04:14 <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
07:04:16 <haskellbridge> <hellwolf> what is that?
07:04:18 <haskellbridge> <Bowuigi> "Everyone's bad at code" and "I like having a good mental health" are probably why we still have PL research lol
07:04:21 geekosaur wonders how long those were queued
07:05:40 <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
07:07:29 → akegalj joins (~akegalj@83-131-242-128.adsl.net.t-com.hr)
07:07:33 <haskellbridge> <geekosaur> oh, they weren't, you were just catching up while the bot was down (system upgrade)
07:07:34 <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?
07:07:59 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
07:09:07 <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.
07:11:51 → tromp joins (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
07:17:29 × prdak quits (~Thunderbi@user/prdak) (Ping timeout: 245 seconds)
07:19:10 <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.
07:21:42 → Lord_of_Life_ joins (~Lord@user/lord-of-life/x-2819915)
07:21:51 × euleritian quits (~euleritia@dynamic-176-006-133-101.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
07:22:08 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
07:22:34 × Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 260 seconds)
07:22:43 × harveypwca quits (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving)
07:23:05 Lord_of_Life_ is now known as Lord_of_Life
07:23:12 × akegalj quits (~akegalj@83-131-242-128.adsl.net.t-com.hr) (Ping timeout: 252 seconds)
07:28:55 → prdak joins (~Thunderbi@user/prdak)
07:31:45 × img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
07:32:53 → akegalj joins (~akegalj@144-188.dsl.iskon.hr)
07:33:05 → img joins (~img@user/img)
07:34:53 × prdak quits (~Thunderbi@user/prdak) (Quit: prdak)
07:34:57 <haskellbridge> <hellwolf> https://hackage.haskell.org/package/vec-0.5.1/docs/Data-Vec-Lazy.html#g:5
07:34:57 <haskellbridge> I am checking this... which one is painful? I am asking unironically.
07:35:12 → prdak joins (~Thunderbi@user/prdak)
07:36:47 <haskellbridge> <hellwolf> > dfoldr :: forall n a f. (forall m. a -> f m -> f ('S m)) -> f 'Z -> Vec n a -> f n
07:36:47 <haskellbridge> beautiful interface :p
07:37:12 × emmanuelux_ quits (~emmanuelu@user/emmanuelux) (Quit: au revoir)
07:37:32 <haskellbridge> <hellwolf> but I can see the problem of filtering.
07:37:53 × xelxebar quits (~xelxebar@wilsonb.com) (Ping timeout: 248 seconds)
07:39:32 <haskellbridge> <hellwolf> though, I could think " filter" differently, it is a fold that adding a boolean to the original vector
07:39:34 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/nUqJifIEojXapRsqcNyBxQyG/SZSeSOaoePA (3 lines)
07:39:50 <haskellbridge> <hellwolf> something like that, depending the use case
07:43:41 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
07:43:58 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
07:44:36 × emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer)
07:45:33 → xelxebar joins (~xelxebar@wilsonb.com)
07:46:19 × tzh quits (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
07:46:45 <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.
07:52:53 × prdak quits (~Thunderbi@user/prdak) (Ping timeout: 252 seconds)
07:53:35 → merijn joins (~merijn@77.242.116.146)
07:53:35 → machinedgod joins (~machinedg@d108-173-18-100.abhsia.telus.net)
07:54:24 <haskellbridge> <hellwolf> amazing.
07:54:24 <haskellbridge> ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/ZXmHzkdBFkCbuBgjCCIfldSk/hI24ncMuDu0 (3 lines)
07:59:15 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
07:59:30 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
08:06:46 → gmg joins (~user@user/gehmehgeh)
08:16:13 × tromp quits (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…)
08:29:58 → lxsameer joins (~lxsameer@Serene/lxsameer)
08:39:26 → pabs3 joins (~pabs3@user/pabs3)
08:43:14 → tromp joins (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
08:44:31 → comerijn joins (~merijn@77.242.116.146)
08:44:47 → prdak joins (~Thunderbi@user/prdak)
08:47:28 × merijn quits (~merijn@77.242.116.146) (Ping timeout: 252 seconds)
08:50:23 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net)
08:54:05 → xff0x joins (~xff0x@2409:251:9040:2c00:c640:4db6:d630:f639)
09:00:01 × prdak quits (~Thunderbi@user/prdak) (Ping timeout: 248 seconds)
09:01:29 ← L29Ah parts (~L29Ah@wikipedia/L29Ah) ()
09:01:56 → j1n37- joins (~j1n37@user/j1n37)
09:02:41 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 248 seconds)
09:02:42 → L29Ah joins (~L29Ah@wikipedia/L29Ah)
09:03:02 → prdak joins (~Thunderbi@user/prdak)
09:03:43 ← L29Ah parts (~L29Ah@wikipedia/L29Ah) ()
09:05:12 → L29Ah joins (~L29Ah@wikipedia/L29Ah)
09:05:22 → starburst joins (~starburst@2601:602:680:2280:dd8c:92ac:a129:aaa9)
09:05:45 <starburst> hello h
09:07:20 <starburst> is anyone ther? (anyone ther.. anythr,,, (echoes))
09:07:29 × Digit quits (~user@user/digit) (Ping timeout: 245 seconds)
09:09:03 <jco> hi hi
09:10:17 × FragByte quits (~christian@user/fragbyte) (Quit: Quit)
09:12:08 <lxsameer> b
09:12:13 → FragByte joins (~christian@user/fragbyte)
09:13:54 <starburst> hii
09:14:09 × xff0x quits (~xff0x@2409:251:9040:2c00:c640:4db6:d630:f639) (Ping timeout: 245 seconds)
09:14:33 × starburst quits (~starburst@2601:602:680:2280:dd8c:92ac:a129:aaa9) (Quit: Client closed)
09:16:12 × werneta quits (~werneta@syn-071-083-160-242.res.spectrum.com) (Read error: Connection reset by peer)
09:17:20 <prdak> hiiii
09:19:34 → werneta joins (~werneta@syn-071-083-160-242.res.spectrum.com)
09:21:26 <haskellbridge> <hellwolf> h <> repeat 'i'
09:27:30 → fp joins (~Thunderbi@2001:708:20:1406::10c5)
09:30:56 ← L29Ah parts (~L29Ah@wikipedia/L29Ah) ()
09:31:38 → L29Ah joins (~L29Ah@wikipedia/L29Ah)
09:31:40 × acidjnk_new quits (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
09:35:14 × hellwolf quits (~user@df56-1a33-0fb6-67d2-0f00-4d40-07d0-2001.sta.estpak.ee) (Ping timeout: 268 seconds)
09:37:46 → acidjnk_new joins (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de)
09:38:03 → hellwolf joins (~user@0f4e-6074-8c9d-a17c-0f00-4d40-07d0-2001.sta.estpak.ee)
09:39:46 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
09:42:11 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
09:42:55 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
09:46:44 × prdak quits (~Thunderbi@user/prdak) (Read error: Connection reset by peer)
09:48:21 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net)
09:54:34 × j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds)
09:55:27 → j1n37 joins (~j1n37@user/j1n37)
10:05:37 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds)
10:05:37 → j1n37- joins (~j1n37@user/j1n37)
10:11:11 → mari-estel joins (~mari-este@user/mari-estel)
10:11:52 → poscat joins (~poscat@user/poscat)
10:12:03 → wootehfoot joins (~wootehfoo@user/wootehfoot)
10:12:51 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Max SendQ exceeded)
10:13:35 → wootehfoot joins (~wootehfoo@user/wootehfoot)
10:14:45 × poscat0x04 quits (~poscat@user/poscat) (Ping timeout: 248 seconds)
10:15:28 × jco quits (~jco@78-70-217-44-no600.tbcn.telia.com) (Quit: leaving)
10:19:17 × tromp quits (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Read error: Connection reset by peer)
10:21:17 → dhil joins (~dhil@5.151.29.138)
10:28:08 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
10:28:24 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net)
10:28:31 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
10:28:49 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net)
10:30:28 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
10:30:46 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net)
10:31:42 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
10:37:00 × __monty__ quits (~toonn@user/toonn) (Ping timeout: 260 seconds)
10:37:04 × s3 quits (~s3@user/bn) (Ping timeout: 245 seconds)
10:37:12 → JuanDaugherty joins (~juan@user/JuanDaugherty)
10:37:24 × qaotsap quits (~paotsaq@2001:818:ea0e:8300:6733:50c0:6d2:30c2) (Ping timeout: 260 seconds)
10:37:59 × mceresa quits (~mceresa@user/mceresa) (Ping timeout: 260 seconds)
10:38:01 × yin quits (~z@user/zero) (Ping timeout: 252 seconds)
10:43:18 → j1n37 joins (~j1n37@user/j1n37)
10:44:24 × j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds)
10:48:37 × acidjnk_new quits (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
10:49:22 → down200 joins (~down200@shell.lug.mtu.edu)
10:51:52 → acidjnk_new joins (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de)
11:02:01 → jespada joins (~jespada@r186-49-240-45.dialup.adsl.anteldata.net.uy)
11:04:20 × AlexZenon quits (~alzenon@178.34.151.238) (Quit: ;-)
11:08:20 × AlexNoo quits (~AlexNoo@178.34.151.238) (Read error: Connection reset by peer)
11:09:59 → Digit joins (~user@user/digit)
11:11:41 JuanDaugherty is now known as ColinRobinson
11:15:28 × typedfern_ quits (~Typedfern@242.red-83-37-36.dynamicip.rima-tde.net) (Remote host closed the connection)
11:21:04 → AlexNoo joins (~AlexNoo@178.34.151.238)
11:21:55 → AlexZenon joins (~alzenon@178.34.151.238)
11:23:07 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
11:23:24 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net)
11:23:56 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
11:24:14 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net)
11:26:06 → prdak joins (~Thunderbi@user/prdak)
11:27:24 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-7850-9e9f-0d14-2cca.rev.sfr.net) (Remote host closed the connection)
11:30:13 × mari-estel quits (~mari-este@user/mari-estel) (Ping timeout: 276 seconds)
11:34:55 <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.
11:35:02 <kqr> Is this known/expected only I've missed something?
11:35:47 × ColinRobinson quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
11:40:03 → mari-estel joins (~mari-este@user/mari-estel)
11:42:37 × prdak quits (~Thunderbi@user/prdak) (Read error: Connection reset by peer)
11:43:36 <opqdonut> it's not perfectly representable, though
11:43:40 <opqdonut> see eg. https://float.exposed/0x40133333
11:46:15 <kqr> Oh. I wonder where I went wrong in my calculations!
11:47:24 <kqr> No, wait, that's for a single-precision float.
11:47:29 <opqdonut> yeah but it's the same
11:47:36 <kqr> If you click the double tab it shows that 2.3 is representable with double precision
11:47:39 <opqdonut> 1/10 is not representable as float anyway
11:47:41 <kqr> Or no, it's not
11:48:02 <kqr> You're right. I was working with too little precision to detect the difference. Thanks
11:48:27 <kqr> I'm guessing the toRational implementation truncates the value instead of rounding it.
11:49:08 <kqr> Wow, more numbers than I thought are irrepresentable – only double-handling functions tend to round them off so I never notice.
11:50:53 <opqdonut> yeah, they're interested in something like reproducability
11:55:35 <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
11:56:59 <opqdonut> but there's a lot of design choices to make here, and quite a bit of old research papers written as well
11:59:15 <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
11:59:18 <kqr> effect due to the above!
12:01:32 <kqr> But I think I can work around it by rounding myself at some appropriate precision.
12:04:21 <tomsmeding> kqr: anything that has something in the denominator that is not a power of 2 is not representable exactly.
12:05:37 × akegalj quits (~akegalj@144-188.dsl.iskon.hr) (Ping timeout: 248 seconds)
12:05:46 <haskellbridge> <Liamzee> did haddock ever fix the reusable named chunk problem?
12:08:14 <tomsmeding> kqr: toRational for Double simply takes the "exponent * fraction" representation that the IEEE float literally encodes, and gives you that as a Rational
12:08:37 <tomsmeding> which means that the denominator of toRational on a Float or Double will always be a power of 2
12:08:43 <tomsmeding> https://hackage.haskell.org/package/base-4.19.0.0/docs/src/GHC.Float.html#line-585
12:23:21 → LainIwakura joins (~LainIwaku@user/LainIwakura)
12:27:11 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Client Quit)
12:28:17 → LainIwakura joins (~LainIwaku@user/LainIwakura)
12:29:29 × TheCoffeMaker_ quits (~TheCoffeM@186.136.173.186) (Quit: So long and thanks for all the fish)
12:30:55 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Client Quit)
12:31:35 → TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker)
12:33:20 → LainIwakura joins (~LainIwaku@user/LainIwakura)
12:36:31 → prdak joins (~Thunderbi@user/prdak)
12:42:19 × AlexZenon quits (~alzenon@178.34.151.238) (Quit: ;-)
12:43:07 → ystael joins (~ystael@user/ystael)
12:43:14 → akegalj joins (~akegalj@93-139-181-11.adsl.net.t-com.hr)
12:43:30 × AlexNoo quits (~AlexNoo@178.34.151.238) (Quit: Leaving)
12:45:43 → mari35028 joins (~mari-este@user/mari-estel)
12:47:09 → tolgo joins (~Thunderbi@199.115.144.130)
12:47:41 × mari-estel quits (~mari-este@user/mari-estel) (Read error: Connection reset by peer)
12:47:44 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
12:48:00 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
12:49:07 → weary-traveler joins (~user@user/user363627)
12:49:56 × bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
12:52:04 × CiaoSen quits (~Jura@2a02:8071:64e1:da0:5a47:caff:fe78:33db) (Ping timeout: 245 seconds)
12:52:54 → jespada_ joins (~jespada@r179-25-42-1.dialup.adsl.anteldata.net.uy)
12:55:15 × jespada quits (~jespada@r186-49-240-45.dialup.adsl.anteldata.net.uy) (Ping timeout: 260 seconds)
12:56:11 × visilii quits (~visilii@85.172.76.90) (Ping timeout: 272 seconds)
12:57:55 × weary-traveler quits (~user@user/user363627) (Quit: Konversation terminated!)
12:58:20 → weary-traveler joins (~user@user/user363627)
12:59:26 × mari35028 quits (~mari-este@user/mari-estel) (Ping timeout: 252 seconds)
13:02:43 × mange quits (~user@user/mange) (Remote host closed the connection)
13:04:56 × tolgo quits (~Thunderbi@199.115.144.130) (Ping timeout: 252 seconds)
13:16:21 × chiselfuse quits (~chiselfus@user/chiselfuse) (Remote host closed the connection)
13:16:57 → chiselfuse joins (~chiselfus@user/chiselfuse)
13:22:13 → Square2 joins (~Square4@user/square)
13:25:26 → haritz joins (~hrtz@2a01:4b00:bc2e:7000::2)
13:25:26 × haritz quits (~hrtz@2a01:4b00:bc2e:7000::2) (Changing host)
13:25:26 → haritz joins (~hrtz@user/haritz)
13:26:19 → AlexNoo joins (~AlexNoo@178.34.151.238)
13:29:28 → AlexZenon joins (~alzenon@178.34.151.238)
13:30:15 × bionade24 quits (~quassel@2a03:4000:33:45b::1) (Ping timeout: 260 seconds)
13:30:23 → bionade24 joins (~quassel@2a03:4000:33:45b::1)
13:33:54 × prdak quits (~Thunderbi@user/prdak) (Read error: Connection reset by peer)
13:36:41 → prdak joins (~Thunderbi@user/prdak)
13:39:10 × Teacup quits (~teacup@user/teacup) (Quit: No Ping reply in 180 seconds.)
13:40:46 → Teacup joins (~teacup@user/teacup)
13:42:31 × fp quits (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 268 seconds)
13:43:08 × Goodbye_Vincent1 quits (cyvahl@freakshells.net) (Read error: Connection reset by peer)
13:43:17 × prdak quits (~Thunderbi@user/prdak) (Ping timeout: 248 seconds)
13:51:37 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
13:51:51 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
13:56:11 × Axman6 quits (~Axman6@user/axman6) (*.net *.split)
13:56:11 × superbil quits (~superbil@114-32-231-70.hinet-ip.hinet.net) (*.net *.split)
13:56:11 × duckworld quits (~duckworld@user/duckworld) (*.net *.split)
13:57:09 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Quit: Client closed)
14:04:54 → fp joins (~Thunderbi@2001:708:20:1406::10c5)
14:06:23 → notdabs joins (~Owner@2600:1700:69cf:9000:79ef:6a68:163c:c553)
14:07:57 → LainIwakura joins (~LainIwaku@user/LainIwakura)
14:11:16 → tolgo joins (~Thunderbi@199.115.144.130)
14:11:28 × tolgo quits (~Thunderbi@199.115.144.130) (Client Quit)
14:12:34 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 244 seconds)
14:14:22 → euleritian joins (~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de)
14:21:35 <EvanR> 2.29999995231628417969 is also not the exact decimal value, which would bit a bit longer but still finite
14:23:35 <EvanR> unfortunately lambdabot doesn't have scientific to make the expansion easy
14:24:53 × son0p quits (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 248 seconds)
14:27:58 <EvanR> 2.29999999999999982236431605997495353221893310546875 🤯
14:28:24 <EvanR> still doesn't seem right
14:30:33 <EvanR> ok
14:31:45 × acidjnk_new quits (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
14:34:26 <EvanR> 0.1000000000000000055511151231257827021181583404541015625 gotta love the "...6875" and "...5625" at the end proclaiming the arrival of a dyadic fraction
14:42:31 <int-e> > truncate $ toRational 2.3 * 10^53
14:42:32 <lambdabot> 229999999999999982236431605997495353221893310546875000
14:42:33 → son0p joins (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d)
14:44:38 → acidjnk_new joins (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de)
14:44:57 <EvanR> I wonder where 2.29999995231628417969 comes fro
14:45:21 <EvanR> with that length
14:47:04 × loonycyborg quits (loonycybor@wesnoth/developer/loonycyborg) (Read error: Connection reset by peer)
14:47:22 × euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.)
14:50:08 → loonycyborg joins (loonycybor@wesnoth/developer/loonycyborg)
14:50:08 <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
14:52:29 × son0p quits (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d) (Ping timeout: 245 seconds)
14:52:53 → euphores joins (~SASL_euph@user/euphores)
14:53:04 <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
14:53:10 <ski> using existential, or the CPS encoding or data type encoding of that)
14:54:37 → son0p joins (~ff@2800:e6:4001:f995:7f79:d961:a77:e30d)
14:54:55 <glguy> > Data.Number.CReal.showCReal 50 (realToFrac 2.3)
14:54:57 <lambdabot> "2.29999999999999982236431605997495353221893310546875"
14:55:10 <int-e> EvanR: this.max_digits = 21 in FloatConfig() in Float.js (doesn't count the decimal point)
14:55:27 <int-e> > length "2.29999995231628417969"
14:55:28 <lambdabot> 22
14:55:59 <int-e> (doesn't count leading zeros either)
14:56:38 <int-e> EvanR: so it's due to how that float.exposed website works
14:57:07 <EvanR> oh
14:58:49 <EvanR> that's decidedly larger than DBL_DECIMAL_DIG on my computer (17)
14:59:38 <EvanR> ... but it is equal to LDBL_DECIMAL_DIG
15:00:32 <EvanR> javascript assuming extended precision? 😱
15:01:09 → MironZ38 joins (~MironZ@nat-infra.ehlab.uk)
15:02:06 → prdak joins (~Thunderbi@user/prdak)
15:03:05 <EvanR> > Data.Number.CReal.showCReal 50 (realToFrac 0.1)
15:03:07 <lambdabot> "0.1000000000000000055511151231257827021181583404541"
15:03:13 × MironZ3 quits (~MironZ@nat-infra.ehlab.uk) (Ping timeout: 248 seconds)
15:03:14 MironZ38 is now known as MironZ3
15:03:18 <EvanR> so you have to "already know" the 50 to make that work
15:03:27 → Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542)
15:03:59 <EvanR> > Data.Number.CReal.showCReal 55 (realToFrac 0.1)
15:04:00 <lambdabot> "0.1000000000000000055511151231257827021181583404541015625"
15:06:29 → kuribas joins (~user@ptr-17d51emz2h3kcoowrgl.18120a2.ip6.access.telenet.be)
15:08:02 × pavonia quits (~user@user/siracusa) (Quit: Bye!)
15:10:32 <tomsmeding> > Data.Number.CReal.showCReal 60 (realToFrac 0.1)
15:10:33 <lambdabot> "0.1000000000000000055511151231257827021181583404541015625"
15:11:04 <tomsmeding> turns out the correct answer was 55?
15:11:17 <tomsmeding> wait why does '55' give 6 more digits than '50'
15:12:01 <EvanR> > Data.Number.CReal.showCReal 54 (realToFrac 0.1)
15:12:03 <lambdabot> "0.100000000000000005551115123125782702118158340454101563"
15:12:22 <int-e> > Data.Number.CReal.showCReal 56 (realToFrac 0.10000000000000002)
15:12:23 <EvanR> maybe 50 ends in a zero
15:12:24 <lambdabot> "0.10000000000000001942890293094023945741355419158935546875"
15:12:34 <tomsmeding> that makes sense
15:13:19 <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)
15:13:42 <EvanR> I just noticed earlier that the expansion for 0.1 had 5 more digits than 2.3 so I "already knew" the 55
15:13:48 <tomsmeding> not the final one, right? Just the 50th
15:14:27 <tomsmeding> > [length (Data.Number.CReal.showCReal n (realToFrac 0.1)) | n <- [48 .. 58]]
15:14:28 <lambdabot> [50,51,51,53,54,55,56,57,57,57,57]
15:15:02 <int-e> > [length (Data.Number.CReal.showCReal n (realToFrac
15:15:04 <lambdabot> <hint>:1:52: error:
15:15:04 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
15:15:06 <int-e> 0.1)) | n <- [48 .. 58]]
15:15:09 <int-e> meh
15:15:11 <tomsmeding> :)
15:15:57 <int-e> > [length (Data.Number.CReal.showCReal n (realToFrac 0.10000000000000002)) | n <- [48 .. 58]]
15:15:58 <lambdabot> [50,51,52,53,54,55,56,57,58,58,58]
15:16:18 <tomsmeding> ah, so the 50th _and_ the 56th
15:16:57 <tomsmeding> EvanR: your 50 confused everyone, it's your fault
15:17:08 <EvanR> that was glguy
15:17:10 <tomsmeding> (everyone = me)
15:17:13 <tomsmeding> oh
15:17:31 <int-e> it didn't confuse me because I didn't even think about were that 50 came from :-P
15:17:37 <int-e> where
15:18:13 <EvanR> enough magic numbers, I will now see about computing this with like 5 APL symbols
15:19:36 <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.
15:20:11 <EvanR> that's base 2
15:20:16 <tomsmeding> yes
15:20:28 <tomsmeding> the number of decimal digits of 1/2^n is n
15:20:37 <tomsmeding> behind the decimal points, that is
15:20:42 <tomsmeding> decimal decimal digits?
15:20:56 <tomsmeding> 0.5 0.25 0.125 0.0625
15:21:06 <EvanR> yes so it doesn't let you predict the length of the above strings exactly
15:21:28 <tomsmeding> apart from a possible trailing 0, it does
15:21:28 <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
15:21:30 <EvanR> > Data.Number.CReal.showCReal 61 (realToFrac 0.00001)
15:21:31 <lambdabot> "0.0000100000000000000008180305391403130954586231382563710212708"
15:21:59 <int-e> EvanR: so keeping track of that power of 2 tells you how many decimal digits you need
15:22:09 <EvanR> the number of binary digits of 1/2^n is n, what were you talking about
15:22:15 <tomsmeding> yes
15:22:16 <int-e> > logBase 0.5 0.00001
15:22:17 <lambdabot> 16.609640474436812
15:22:20 <tomsmeding> and the number of _decimal_ digits is, too
15:22:20 <EvanR> you said decimal
15:22:24 <EvanR> o_O
15:22:33 <int-e> > Data.Number.CReal.showCReal (53 + 16) (realToFrac 0.00001)
15:22:34 <lambdabot> "0.000010000000000000000818030539140313095458623138256371021270751953125"
15:23:18 <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 :)
15:23:39 × acidjnk_new quits (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
15:23:39 <int-e> (It worked, but I should be using 17.)
15:24:15 <int-e> it's almost as if 1/2^n = 5^n/10^n
15:24:24 <int-e> call me crazy, but I think that's actually true
15:24:26 <int-e> ;-)
15:24:29 <EvanR> each time you multiply by 1/10 you get a nother power of two
15:24:35 <EvanR> but also a power of 5
15:24:49 <EvanR> not obvious to me
15:25:29 <int-e> once you understand it it will be obvious ;)
15:25:33 <tomsmeding> > 5 ^ 20
15:25:34 <lambdabot> 95367431640625
15:25:39 <EvanR> tautology 37
15:25:49 <tomsmeding> > Data.Number.CReal.showCReal (53 + 16) (1 % 2^20)
15:25:51 <lambdabot> error:
15:25:51 <lambdabot> • Couldn't match expected type ‘CReal’ with actual type ‘Ratio a0’
15:25:51 <lambdabot> • In the second argument of ‘showCReal’, namely ‘(1 % 2 ^ 20)’
15:25:58 <EvanR> k powers of 5 end in 5
15:25:59 <tomsmeding> > Data.Number.CReal.showCReal (53 + 16) (realToFrac (1 % 2^20))
15:26:00 <lambdabot> "0.00000095367431640625"
15:26:02 <EvanR> in decimal
15:26:13 <tomsmeding> these two numbers are alike
15:26:35 <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.
15:27:35 <EvanR> I mean "if you understand it it's obvious"
15:27:44 <int-e> Same here.
15:28:22 <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]]
15:28:23 <lambdabot> True
15:28:36 [exa] reminded of that "zeros at the end of factorial" exercise
15:29:19 <tomsmeding> "dividing by powers of 2 is easy. Just exponentiate 5 and add some zeros"
15:29:23 <EvanR> :t showCReal -- now with more unqualified
15:29:24 <lambdabot> Int -> CReal -> String
15:30:23 <EvanR> fine I'll use paper
15:30:25 <tomsmeding> anyway this checks the claim for 1 <= n <= 50 :p
15:30:42 <int-e> [exa]: do you know the variant for binomial coefficients, https://en.wikipedia.org/wiki/Lucas%27s_theorem ?
15:31:02 <EvanR> check it for n up to 10^900 and I'll start to be convinced (just kidding)
15:31:14 × prdak quits (~Thunderbi@user/prdak) (Read error: Connection reset by peer)
15:31:18 <tomsmeding> it does show where int-e's powers of 5 end up
15:32:23 <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
15:32:55 <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)
15:33:09 <tomsmeding> so you need n decimal decimal digits to represent 1/2^n
15:34:12 <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 )
15:34:19 <EvanR> "decimal decimal" ??
15:34:29 <tomsmeding> decimal digits behind the decimal point
15:34:35 <EvanR> oh
15:35:25 <int-e> > [0..] >>= last . show . (5^)
15:35:26 <lambdabot> error:
15:35:26 <lambdabot> • Couldn't match type ‘Char’ with ‘[b]’
15:35:26 <lambdabot> Expected type: b0 -> [b]
15:35:45 <tomsmeding> too free
15:36:11 <tomsmeding> > [0..] >>= pure . last . show . (5^)
15:36:12 <lambdabot> "155555555555555555555555555555555555555555555555555555555555555555555555555...
15:36:26 <EvanR> proof by exhaustion
15:36:27 <tomsmeding> > last . show . (5^) <$> [0..]
15:36:29 <lambdabot> "155555555555555555555555555555555555555555555555555555555555555555555555555...
15:46:04 × byte quits (~mu@user/byte) (Read error: Connection reset by peer)
15:48:48 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Quit: Client closed)
15:49:32 <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
15:49:48 <EvanR> which is impossible
15:49:54 → tzh joins (~tzh@c-76-115-131-146.hsd1.or.comcast.net)
15:50:05 <EvanR> and nobody was doing it anyway!
15:50:10 <EvanR> smh
15:55:29 × akegalj quits (~akegalj@93-139-181-11.adsl.net.t-com.hr) (Quit: leaving)
16:03:40 × CalimeroTeknik quits (~calimero@ctkarch.org) (Changing host)
16:03:40 → CalimeroTeknik joins (~calimero@user/calimeroteknik)
16:06:42 <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
16:06:56 <EvanR> though it might need to be adjusted to be a proper decimal float
16:07:17 <EvanR> changing the number of digits a few
16:08:41 → LainIwakura joins (~LainIwaku@user/LainIwakura)
16:08:58 <EvanR> shoot if k is negative that fails
16:09:16 × euleritian quits (~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
16:09:34 → euleritian joins (~euleritia@77.23.248.47)
16:13:32 <EvanR> if k is negative those are integer equations nvm
16:15:42 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
16:16:41 × chele quits (~chele@user/chele) (Remote host closed the connection)
16:18:19 → acarrico joins (~acarrico@pppoe-209-99-221-107.greenmountainaccess.net)
16:20:01 × comerijn quits (~merijn@77.242.116.146) (Ping timeout: 248 seconds)
16:20:21 <EvanR> I"m wrong < 2*10^k < 10^(k+1) so it's even a proper decimal float
16:21:45 <tomsmeding> it is
16:22:09 <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
16:22:26 <tomsmeding> oh my n is your k
16:22:50 × euleritian quits (~euleritia@77.23.248.47) (Read error: Connection reset by peer)
16:23:38 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
16:24:06 × gorignak quits (~gorignak@user/gorignak) (Quit: quit)
16:28:04 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
16:28:26 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
16:28:55 → LainIwakura joins (~LainIwaku@user/LainIwakura)
16:35:45 <EvanR> so all floats end up between "ten and twenty" before the power of ten jumps
16:36:14 <EvanR> you won't see the decimal form starting with 3
16:36:45 <EvanR> k that can't be right
16:37:03 <int-e> > 2^^(-5)
16:37:04 <lambdabot> 3.125e-2
16:37:14 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
16:37:22 → euleritian joins (~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de)
16:39:51 <EvanR> that's not between 10^k and 2*10^k ...
16:40:13 × euleritian quits (~euleritia@dynamic-176-006-132-060.176.6.pool.telefonica.de) (Read error: Connection reset by peer)
16:40:30 → euleritian joins (~euleritia@77.23.248.47)
16:44:04 <EvanR> I forgot to handle the exponent
16:44:18 <EvanR> but
16:47:08 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
16:47:23 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
16:51:01 × euleritian quits (~euleritia@77.23.248.47) (Ping timeout: 248 seconds)
16:51:50 × fp quits (~Thunderbi@2001:708:20:1406::10c5) (Ping timeout: 268 seconds)
16:53:12 → euleritian joins (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de)
17:00:52 → econo_ joins (uid147250@id-147250.tinside.irccloud.com)
17:03:54 × Buliarous quits (~gypsydang@46.232.210.139) (Remote host closed the connection)
17:04:23 → Buliarous joins (~gypsydang@46.232.210.139)
17:06:29 → wootehfoot joins (~wootehfoo@user/wootehfoot)
17:10:32 <EvanR> ok yeah adding in the exponential factor leads to a decimal form but not necessarily normalized
17:13:38 → jco joins (~jco@78-70-217-44-no600.tbcn.telia.com)
17:15:16 → acidjnk_new joins (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de)
17:18:39 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net)
17:21:19 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
17:25:47 → ft joins (~ft@p4fc2a6e6.dip0.t-ipconnect.de)
17:28:29 × _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (Ping timeout: 265 seconds)
17:30:54 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
17:31:34 <tomsmeding> EvanR: all floats end up between 10 and 100 in binary, yes
17:31:51 <tomsmeding> after multiplying by a power of 2
17:32:00 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
17:32:09 <tomsmeding> which could have been on https://www.vex.net/~trebla/humour/tautologies.html
17:32:26 → _d0t joins (~{-d0t-}@user/-d0t-/x-7915216)
17:36:39 × _d0t quits (~{-d0t-}@user/-d0t-/x-7915216) (Remote host closed the connection)
17:37:29 → _d0t joins (~{-d0t-}@user/-d0t-/x-7915216)
17:48:45 → justsomeguy joins (~justsomeg@user/justsomeguy)
17:51:46 × TMA quits (tma@twin.jikos.cz) (Ping timeout: 276 seconds)
17:55:42 × mistivia_ quits (~mistivia@user/mistivia) (Ping timeout: 252 seconds)
17:55:43 → mistivia joins (~mistivia@user/mistivia)
17:59:15 × wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer)
18:01:10 → ljdarj joins (~Thunderbi@user/ljdarj)
18:02:00 → LainIwakura joins (~LainIwaku@user/LainIwakura)
18:02:02 → fp joins (~Thunderbi@87-94-239-173.bb.dnainternet.fi)
18:04:35 → mceresa joins (~mceresa@user/mceresa)
18:17:06 → superbil joins (~superbil@114-32-231-70.hinet-ip.hinet.net)
18:17:06 → duckworld joins (~duckworld@user/duckworld)
18:17:06 → Axman6 joins (~Axman6@user/axman6)
18:19:04 × fp quits (~Thunderbi@87-94-239-173.bb.dnainternet.fi) (Ping timeout: 276 seconds)
18:20:07 × jco quits (~jco@78-70-217-44-no600.tbcn.telia.com) (Quit: leaving)
18:20:39 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net) (Remote host closed the connection)
18:20:48 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net)
18:21:15 → JuanDaugherty joins (~juan@user/JuanDaugherty)
18:23:46 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-956d-23d3-b043-d827.rev.sfr.net) (Remote host closed the connection)
18:26:22 → alexherbo2 joins (~alexherbo@2a02-8440-250b-b0ac-9124-7afb-e1b3-b7a1.rev.sfr.net)
18:29:13 → gorignak joins (~gorignak@user/gorignak)
18:30:10 × lxsameer quits (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds)
18:39:16 → prdak joins (~Thunderbi@user/prdak)
18:40:01 → DirkU joins (~DirkU@i5C74E2AB.versanet.de)
18:40:59 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
18:42:55 ← DirkU parts (~DirkU@i5C74E2AB.versanet.de) ()
18:44:25 × prdak quits (~Thunderbi@user/prdak) (Ping timeout: 276 seconds)
18:46:25 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
18:46:50 → sprotte24 joins (~sprotte24@p200300d16f1e9b00643a7ed1094ff735.dip0.t-ipconnect.de)
18:47:15 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
18:47:48 → visilii joins (~visilii@85.94.26.146)
18:48:31 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
18:48:46 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
18:49:04 × weary-traveler quits (~user@user/user363627) (Remote host closed the connection)
18:56:47 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:00:02 × caconym7 quits (~caconym@user/caconym) (Quit: bye)
19:00:46 → caconym7 joins (~caconym@user/caconym)
19:01:25 × gorignak quits (~gorignak@user/gorignak) (Quit: quit)
19:01:46 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
19:06:04 → gorignak joins (~gorignak@user/gorignak)
19:12:34 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:17:05 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
19:17:54 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:18:13 <JuanDaugherty> google makes funny with "Wanteds with rewriters haskell"
19:19:08 → rvalue- joins (~rvalue@user/rvalue)
19:20:02 × rvalue quits (~rvalue@user/rvalue) (Ping timeout: 252 seconds)
19:21:32 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 244 seconds)
19:23:25 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
19:26:38 × gorignak quits (~gorignak@user/gorignak) (Ping timeout: 252 seconds)
19:26:54 → gorignak joins (~gorignak@user/gorignak)
19:27:51 rvalue- is now known as rvalue
19:32:00 × gorignak quits (~gorignak@user/gorignak) (Quit: quit)
19:32:29 → gorignak joins (~gorignak@user/gorignak)
19:33:48 → j1n37- joins (~j1n37@user/j1n37)
19:34:24 → tromp joins (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
19:34:28 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 276 seconds)
19:35:19 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:35:39 <monochrom> I am dumb. I knew there must be a correspondence between 0.5, 0.25, 0.125, 0.0625, ... with 5, 25, 125, 625, ... I never thought of simply 1/2 = 5/10.
19:39:00 <EvanR> famously not every decimal float has a binary form e.g. 1/10. Assume 1/10 = N/2^k for some k >= 0. Then 2^k = 2 * 5 * N
19:39:16 <EvanR> a power of two contains a prime factor of 5 contradiction
19:40:17 <davean> EvanR: Which is why one uses decimal floating point.
19:40:29 <davean> There is a reason its part of the IEEE 754 standard
19:40:41 <EvanR> there is one person who uses decimal floating point?
19:40:47 <davean> There are many
19:40:49 <EvanR> citation needed
19:41:05 <davean> Hell, a lot of systems have dedicated BCD hardware units
19:41:25 <EvanR> oh yeah BCD forgot about those xD
19:41:34 <EvanR> I keep confusing it with EBCDIC
19:41:41 <davean> financial institutions SERIOUSLY care about this
19:41:59 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
19:42:09 × gorignak quits (~gorignak@user/gorignak) (Quit: quit)
19:42:13 <davean> its a major selling point of a lot of IBM hardware for example
19:42:34 <davean> Both z/Arch and POWER have it standard
19:42:39 → gorignak joins (~gorignak@user/gorignak)
19:42:42 <EvanR> smh shoulda just switched to binary money
19:43:08 <davean> x86 has SOME support but it sucks
19:44:12 <davean> https://www.ibm.com/docs/en/zos/2.4.0?topic=functions-decimal-floating-point-built-in
19:44:36 <davean> You'll find a bunch of databases and such which support decimal32/64 for example, because people DO care
19:44:44 <davean> people have legal problems if they get it wrong :-p
19:45:29 <davean> There is a haskell lib that does emulation of it because banks ...
19:45:31 <EvanR> sounds like we need more laws like that
19:45:37 <davean> ask me how I know
19:45:52 <EvanR> this is haskell we like laws
19:47:36 <JuanDaugherty> EBCDIC basically means IBM coded
19:47:42 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
19:47:44 <tomsmeding> monochrom: it's okay, I also only figured this out as part of the preceding conversation
19:48:24 <JuanDaugherty> others like burroughs accomodated cause in that time computers were called "ibm machines"
19:49:09 → Guest24 joins (~Guest24@189.7.87.242)
19:50:16 <davean> EvanR: You can actually find some complaints in the Haskell mailing list about the lack of decimal64 support ...
19:50:33 × Guest24 quits (~Guest24@189.7.87.242) (Client Quit)
19:52:06 × ii8 quits (~ii8@45.63.97.131) (Quit: ii8)
19:52:25 <davean> https://hackage.haskell.org/package/Decimal ah I think thats what people use
19:53:22 → pavonia joins (~user@user/siracusa)
19:53:22 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
19:53:53 <EvanR> Scientific?
19:58:13 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
19:59:47 <davean> EvanR: For money? No
20:00:16 × tromp quits (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…)
20:00:43 <davean> EvanR: people want fixed precision, not arbitrary
20:01:07 <EvanR> like Data.Fixed?
20:01:22 <davean> Yes, thats closer
20:02:07 × alexherbo2 quits (~alexherbo@2a02-8440-250b-b0ac-9124-7afb-e1b3-b7a1.rev.sfr.net) (Remote host closed the connection)
20:02:24 → tromp joins (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad)
20:06:20 <EvanR> eitherFromRational :: Integral i => Rational -> Either String (DecimalRaw i)
20:06:24 <EvanR> Try to convert Rational to Decimal with absolute precision return string with fail description if not converted
20:06:30 <EvanR> what is absolute precision
20:06:57 <JuanDaugherty> not float
20:06:58 <davean> A specific accuracy, without reference to a relative point.
20:07:11 <davean> like Data.Fixed, thats absolute precision
20:07:21 <davean> it says exactly what precision it always is
20:08:04 × euleritian quits (~euleritia@ip4d17f82f.dynamic.kabel-deutschland.de) (Ping timeout: 252 seconds)
20:08:33 → LainIwakura joins (~LainIwaku@user/LainIwakura)
20:08:41 → euleritian joins (~euleritia@dynamic-176-006-135-001.176.6.pool.telefonica.de)
20:09:10 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:11:15 × gorignak quits (~gorignak@user/gorignak) (Quit: quit)
20:11:35 → gorignak joins (~gorignak@user/gorignak)
20:12:47 <EvanR> Try to convert Rational to Decimal with absolute precision return string with fail description if not converted
20:12:53 <EvanR> bad paste
20:12:58 <EvanR> Allocate a DecimalRaw value proportionately with the values in a list. The allocated portions are guaranteed to add up to the original value.
20:13:13 <EvanR> bold guarantee, do we have some proof
20:13:28 <davean> Thats not very bold
20:13:33 <davean> there is a trivial solution
20:14:05 <davean> When you get to the last value, just subtract the preceding results from the distributed amount, and allocate that to the last value
20:14:07 <davean> quite trivial
20:14:09 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
20:14:48 <EvanR> I know there's an algorithm for it
20:15:16 <EvanR> but how do you know the code in this library implements it correctly
20:15:34 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 244 seconds)
20:18:08 × michalz quits (~michalz@185.246.207.218) (Remote host closed the connection)
20:18:53 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:19:23 → justsomeguy joins (~justsomeg@user/justsomeguy)
20:21:16 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
20:22:12 → TMA joins (tma@twin.jikos.cz)
20:23:50 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
20:34:43 × kuribas quits (~user@ptr-17d51emz2h3kcoowrgl.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
20:36:42 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:39:41 × takuan quits (~takuan@d8D86B601.access.telenet.be) (Remote host closed the connection)
20:41:25 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
20:42:07 <c_wraith> I learned something about USD recently that I found amusing and relevant to doing money math. Legally, the minimal increment of USD is 1/1000th of a dollar. That is, a tenth of a cent. So instead of doing calculations in the number of cents, you should do your calculations in the number of tenths of cents.
20:42:25 × gorignak quits (~gorignak@user/gorignak) (Ping timeout: 248 seconds)
20:42:28 <c_wraith> (or, you know. Data.Fixed with 3 decimals of precision)
20:43:01 → droideqa joins (uid499291@user/droideqa)
20:46:59 <EvanR> I have the distinct feeling they are using more decimals
20:47:07 <EvanR> in those trade platforms
20:48:08 <EvanR> but 3 is consistent with gas station prices
20:51:00 × peterbecich quits (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
20:51:10 <c_wraith> honestly, that's not really true, as most systems don't allow transfers of less than a cent. So really if you're doing financial computations, you should put your methodology in the contract.
20:52:06 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
20:52:37 → Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
20:53:35 <haskellbridge> <Liamzee> c_wraith: is there a legal rounding function, or is it floor?
20:53:57 <EvanR> "banker's rounding"
20:54:08 <haskellbridge> <Liamzee> "lawyer's rounding"
20:54:11 <EvanR> would be funny if banks didn't use this
20:54:23 <c_wraith> No, the legal status is just for amounts. How you calculate those amounts is a matter for all parties to agree on. Or sue each other if they can't.
20:54:51 <EvanR> *I'm sure no one will miss 1/10 of a cent here and there*
20:55:04 <c_wraith> It's the office space/superman plot!
20:55:06 <haskellbridge> <Liamzee> yeah, i was more wondering about 1/100th of a cent
20:55:16 <haskellbridge> <Liamzee> "legally, I embezzled nothing"
20:55:40 <haskellbridge> <Liamzee> at least 1/25th of a cent should be safe under any common rounding scheme
20:56:28 <EvanR> cents make no sense
20:56:49 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
20:57:48 <darkling> $former_work set up a "credits" system for customers. We stored the values in units of 1/1000 credit. I argues for 1/840 of a credit (2^3*3*5*7), but I got overruled. :(
20:58:09 <c_wraith> yes. small factors!
20:58:18 <c_wraith> decimal kind of sucks.
20:58:34 <c_wraith> the babylonians made a lot more sense with their base-60 system
20:59:45 <darkling> I think at some point, someone wanted to use a fraction that didn't work in the 1/1000th units, but would have worked in 1/840ths...
21:00:00 <EvanR> store their credits in cyclotomic
21:00:01 <haskellbridge> <Liamzee> 7 is just a weird number, I just don't see it come up very often
21:00:18 <EvanR> don't hang out in the casino much?
21:01:02 <EvanR> when your HP in FF7 became 7777 you'd get 7777 fever and do tons of attacks or something
21:01:16 <Square2> I doubt what I'm trying to do is doable, but I'll ask anyway. Say I have 'f :: a -> b -> Bool'. Is there a way to implement that so it return true if a == b?
21:01:36 <c_wraith> Square2: not without adding some constraints to that type
21:01:48 <EvanR> needs more type signature
21:01:50 <haskellbridge> <sm> Decimal lib is what hledger users, it's great (up to 255 decimal places)
21:01:52 <Square2> gotcha. That won't work
21:01:57 <c_wraith> Square2: like, you could do it if you add (Typeable a, Typeable b)
21:02:26 <Square2> Oh yeah. That could possibly work
21:02:39 <EvanR> or if they were coercible to a common type
21:02:43 <EvanR> that has an Eq instance
21:03:17 <c_wraith> EvanR: I read the question as being about "if the types are the same", not "if the values are the same"
21:03:19 × j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 260 seconds)
21:03:25 <haskellbridge> <Liamzee> you don't actually need an Eq instance if they're... oh wait, that's manual implementation of Eq
21:03:31 → j1n37 joins (~j1n37@user/j1n37)
21:03:42 <Square2> ah ok. I feel I'm out in the hack suburb, may need to rethink stuff.
21:03:42 <EvanR> er
21:04:10 × dhil quits (~dhil@5.151.29.138) (Ping timeout: 252 seconds)
21:04:24 <EvanR> if you aren't comparing the values then it doesn't need to be a function
21:04:42 <c_wraith> Yeah, in general seeing Typeable should make you go "is there a better way?"
21:04:43 <EvanR> but a multiparameter type class
21:05:06 <c_wraith> EvanR: That class already exists and is named (~)
21:05:12 <EvanR> there you go
21:05:24 <c_wraith> But it isn't quite the same thing as giving you a *value*
21:05:38 × m5zs7k quits (aquares@web10.mydevil.net) (Ping timeout: 252 seconds)
21:05:49 <EvanR> there's that type equality test class
21:06:01 <c_wraith> :t \x y -> typeOf x == typeOf y -- this just isn't the same thing as a MPTC
21:06:02 <lambdabot> (Typeable a1, Typeable a2) => a1 -> a2 -> Bool
21:06:16 <EvanR> gross
21:06:51 <c_wraith> In generaly, you'd probably want (:~:) so you could actually write code that knows the types are the same by matching on Refl
21:07:33 <c_wraith> But yeah, the whole thing is... Really hoping there's a better way.
21:07:53 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:08:01 → tolgo joins (~Thunderbi@199.115.144.130)
21:08:08 → m5zs7k joins (aquares@web10.mydevil.net)
21:08:28 → shapr joins (~user@2600:4040:5c49:5600:dfc0:98d5:78c7:1853)
21:08:53 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 265 seconds)
21:10:38 → ljdarj1 joins (~Thunderbi@user/ljdarj)
21:12:58 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
21:13:44 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 245 seconds)
21:14:06 → ljdarj joins (~Thunderbi@user/ljdarj)
21:15:10 × ljdarj1 quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
21:15:13 × tolgo quits (~Thunderbi@199.115.144.130) (Ping timeout: 276 seconds)
21:16:45 <Square2> c_wraith, EvanR thanks. You convinced me I should just try avoid this situation =D
21:17:28 <c_wraith> good. that's the best lesson here. :)
21:18:48 <EvanR> inline python it is
21:20:24 <haskellbridge> <Liamzee> https://hackage-content.haskell.org/package/inline-python-0.1.1.1
21:21:53 <monochrom> The financial sector uses base 10 for fractions, and it is written is the law and too late to change. (You need to go back to say the 17th century to change it.) However, for all other purposes, Knuth proved that rounding errors are less bad iff the base is smaller, therefore base 2 is the least bad.
21:22:08 <monochrom> s/written is/written into/
21:23:21 <monochrom> (I don't mean the law were written in the 17th century. But the law just codifies a long tradition that began back then.)
21:23:40 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:25:25 → justsomeguy joins (~justsomeg@user/justsomeguy)
21:25:28 × tromp quits (~textual@2001:1c00:3487:1b00:b5bd:9efd:97f5:64ad) (Quit: My iMac has gone to sleep. ZZZzzz…)
21:26:11 <c_wraith> I suppose given that context, USD uses 1000ths of a dollar in order to make a ha'penny an actual value they can issue.
21:27:02 <davean> monochrom: wouldn't unary be better?
21:27:53 <monochrom> I don't know. But I start with: How do I express one half in unary?
21:30:56 <darkling> For extra fun, consider pre-decimalisation British coinage (240 pence / pound; fractions down to 1/4p, so 960 farthings to the pound)... and then the transition to decimalised currency. :)
21:31:07 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
21:31:43 <EvanR> use unary floating point
21:31:43 <darkling> (There's an entire plot thread in a couple of Trollope's books about that, 120 years before they actually did it).
21:32:25 <monochrom> A lot of people must have complaint that their rightful wealth were literally decimated. >:)
21:32:51 <EvanR> ooooooo
21:33:49 <monochrom> I say that because a lot of students are complaining that I am depriving them of their rightful marks because my exam required thinking.
21:34:57 <darkling> The pund remained the same. The shilling (12 old pence, 5 new) and two shilling coins were kept. Everything under a shilling was dropped, and a new coin (50p) minted for the 10 shilling point.
21:35:54 <darkling> I remember using "5p" and "10p" coins that were marked "1 shilling" and "2 shillings".
21:36:29 <darkling> (They changed it all two years before I was born, but the coins were still in circulation).
21:38:22 → gorignak joins (~gorignak@user/gorignak)
21:38:40 <davean> monochrom: How does one complain they were deprived by an exam requiring thinking?
21:39:07 <davean> It would seem one based on memorization one might have an argument on because one could just look up facts.
21:39:15 <int-e> davean: it's easy if you don't think about it? :)
21:40:27 <monochrom> "Every question requires thinking. There are very little free marks. This is unfair."
21:41:02 <davean> Those are statements, where is the logic though?
21:41:08 <monochrom> I don't know. I guess if one has an entitlement attitude then one understands how this is unfair.
21:41:11 <davean> They're not even given connectives
21:41:44 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:41:49 <darkling> "I showed up! I should get marks for that!"
21:42:09 <davean> My favorit exams where "Here are three things, you have a week to prove them"
21:42:17 <darkling> or, slightly less offensive, but still missing the point, "I spent a lot of time on it!"
21:43:17 <darkling> davean: We'd get problem sheets like that from our lecturers. One of the questions, once, was, literally, "prove the Riemann Hypothesis". Lecturer taking a hopeful punt... :)
21:44:01 <davean> darkling: eh there is partial credit for coming up with interesting intermediate results
21:44:16 → prdak joins (~Thunderbi@user/prdak)
21:44:32 <davean> wouldn't be rthe first time a long standing math problem was solved by dint of being put on a college exam
21:44:50 <darkling> They weren't even marked, let alone credit-worthy. But several of that lecturer's questions qould lead to the follow-on question, "would you like a PhD?"
21:44:57 <davean> There have been several cases of long standing math problems solved because undergrads thought they were supposed to be ab le to sovle it
21:45:18 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Ping timeout: 240 seconds)
21:45:22 <EvanR> didn't know the question was supposed to be hard
21:45:24 <EvanR> strategy
21:45:27 <darkling> Yeah. The Riemann Hypothesis hasn't been one of those yet, though. :)
21:45:52 <int-e> yet
21:46:02 <davean> darkling: Or it was and the prof just assumed it was wrong ;)
21:46:28 <darkling> Hehe. I hope not.
21:46:43 <davean> I once had a list of "Hard problems solved by accident people someone thought it should be easy"
21:46:46 <davean> I should dig that up
21:46:48 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
21:46:57 <davean> It wasn't actually a short list
21:48:00 <darkling> I always liked the history of Fermat's Last Problem. Was thought to be solved for 20 years, back in the 19th century, before someone spotted the mistake.
21:48:43 <EvanR> smh 19th century
21:48:53 <EvanR> they didn't even have set theory
21:49:00 × prdak quits (~Thunderbi@user/prdak) (Ping timeout: 252 seconds)
21:49:02 <EvanR> how could you possibly know if the proof was right or wrong!
21:49:14 <davean> I prefer my theories dynamic, not set.
21:49:24 <EvanR> lol
21:50:13 → tolgo joins (~Thunderbi@199.115.144.130)
21:51:06 <darkling> Yoghurt shouldn't be set, either.
21:54:32 <davean> Anyway, we all know set theory refuses to answer some questions, its just recalcitrant like that
21:54:46 × j1n37 quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds)
21:54:57 × tolgo quits (~Thunderbi@199.115.144.130) (Ping timeout: 276 seconds)
21:55:04 → j1n37- joins (~j1n37@user/j1n37)
21:55:35 <darkling> *everything* refuses to answer some questions. Thanks, Kurt.
21:55:58 <davean> Not true!
21:56:12 <davean> Some things are happy to answer whatever question you like
21:56:20 <EvanR> chatGPT
21:56:27 <EvanR> it's complete but inconsistent
21:56:49 <davean> Yes, lets make ChatGPT the new formal basis for mathmatics, that will solve many problems.
21:56:53 <davean> No more lacking answers
21:56:53 <darkling> It's a complete /what/, though?
21:57:03 <EvanR> dumpsterfire
21:57:11 <int-e> scam
21:57:29 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
21:59:13 <davean> Hum, using our new basis of everything to decide this
21:59:19 <davean> "Is ChatGPT a scam?"
21:59:26 <davean> "No, ChatGPT is not a scam. It's a real AI developed by OpenAI, a legitimate artificial intelligence research organization. ChatGPT is used by millions of people for tasks like writing, coding, research, learning, and more."
21:59:29 <davean> Well thats conclusive
22:00:24 <int-e> I wonder if it has opinions on WorldCoin
22:01:16 <davean> I'
22:01:29 <davean> ve started to loath a new trend
22:01:44 <davean> In issues, people throwing the thing at ChatGPT or whatever, and "
22:01:50 <davean> pasting" its answer as a solution
22:02:01 <davean> It make me want to lock the issues and never fix it
22:02:04 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
22:02:14 <davean> Its so actively unhelpful I wonder if people are doing it to troll
22:02:28 <davean> esp when what it pastes is self-evidently non-helpful
22:02:35 <davean> Which, so far, is all I've seen
22:02:44 <haskellbridge> <sm> I wouldn't mind if it's something helpful
22:02:57 <haskellbridge> <sm> I think I posted one of those myself recently
22:02:59 <davean> Its litterly never been, and it mean it kinda obviously won't be?
22:03:05 <davean> ... yah, you are one of the people I was thinking of
22:03:24 <davean> Yours was a great example of self-evidently not helpful
22:03:33 <haskellbridge> <sm> yikes! where was that
22:03:38 <haskellbridge> <sm> called out on my first attempt 🤣
22:03:39 <davean> The wiki one
22:04:14 <davean> Where it suggested A) uncommenting a commented out line (How do you think it got commented out in the first place? If yhou had a question, check the git history) and B) generated an invalid CSS statement
22:04:52 → j1n37 joins (~j1n37@user/j1n37)
22:05:16 <int-e> davean: I understand that it gets worse when there's a monetary incentive (bug bounties)
22:05:37 <davean> Oh god, I wouldn't be surprised if it did
22:05:46 × j1n37- quits (~j1n37@user/j1n37) (Ping timeout: 252 seconds)
22:05:51 <davean> sm: on the plus side, your chatgpt response annyoed someone else enough to just fix it :)
22:05:54 <haskellbridge> <sm> https://github.com/haskell/haskell-wiki-configuration/issues/56#issuecomment-2822104811
22:06:38 <davean> sorry, the "A" side was simplified out from you IRC posting, not the full length one.
22:07:18 <haskellbridge> <sm> I thought it gave some potentially useful context to my previous (human generated, terse) comment, to someone trying to fix this, and if not, would be easy to ignore.
22:08:31 <davean> It made it very evident it was splurting out some tutorial and nothing related to the actual config
22:08:52 <haskellbridge> <sm> to you. Obviously people like me trying to help don't have the same insight
22:09:12 <haskellbridge> <sm> I'll me more cautious on this tracker in future
22:09:16 <haskellbridge> <sm> be
22:09:44 <davean> The state at that comment was https://github.com/haskell/haskell-wiki-configuration/blob/beb924470357d8cc008a5c8118211066897a48ea/flake.nix
22:09:45 → LainIwakura joins (~LainIwaku@user/LainIwakura)
22:09:57 <davean> You'll note a several line block of it commented out
22:10:31 <davean> Someone didn't write all that and comment it out by "accident"
22:11:27 <davean> Which is the sort of theory-of-mind ChatGPT seems to seriously lack
22:11:54 → paotsaq joins (~paotsaq@127.209.37.188.rev.vodafone.pt)
22:11:56 <haskellbridge> <sm> I pointed that out myself, but didn't know why (there was no explanation)
22:11:56 <davean> anyway, sm, you're hardly the worst person with this ever
22:12:33 <davean> Oh the CSS side I sohuld finish
22:12:49 <davean> it was a CSS directive that targeted displayed text, it clearly mixed up context between display and syntax
22:12:56 <davean> anyway, sm, you are HARDLY the worst
22:13:06 <davean> Its a real plauge lately though
22:13:15 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:14:03 <haskellbridge> <sm> I know that I'm not the worst. I was trying to be helpful. No need to beat up a volunteer for an unhelpful post, I've said I'll be more cautious
22:15:07 <davean> For an explanation of why it was commented out, it was commented out because the repo contains the code, but not in a runable state - it requires a specific build procedure to be run before it is a valid extension. As it was just a stylistic display issue I didn't feel like learning a PHP build sytem to get the wiki back online after the great wiki disaster and I hoped something obvious like that
22:15:09 <davean> would get anyone to step up and assist since I didn't want to end up owning the wiki just because I rescued it.
22:15:33 <davean> tolt happened to find a place they had actually already run the build system though, which made it easy to fix
22:16:53 <davean> Hopefully tolt having made a test vm setup thing for it other people might try working on it.
22:18:14 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
22:19:31 <haskellbridge> <sm> I became annoyed enough at the 6 month breakage to try to spend some more time helping. Without access or any insight / status reports I couldn't do more than blind research. I'm glad it helped remind people of the problem, even it if was annoying. It's just another github issue.
22:20:18 <davean> Hum? That is a full container config for the wiki in that repo
22:21:13 <davean> That is litterly the wiki, minutes its data
22:22:36 <haskellbridge> <sm> I'm irritated. Sorry, I'll drop this
22:28:00 → harveypwca joins (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c)
22:28:59 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:31:41 → emmanuelux joins (~emmanuelu@user/emmanuelux)
22:34:31 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
22:34:38 <haskellbridge> <hellwolf> 🫠 tragedy of the gift economy... which needs more cheerleaders
22:35:12 <int-e> . o O ( it's spelled "grift" )
22:35:16 × sprotte24 quits (~sprotte24@p200300d16f1e9b00643a7ed1094ff735.dip0.t-ipconnect.de) (Quit: Leaving)
22:38:04 × gmg quits (~user@user/gehmehgeh) (Remote host closed the connection)
22:42:05 × justsomeguy quits (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds)
22:44:40 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:44:57 → tolgo joins (~Thunderbi@199.115.144.130)
22:45:22 → peterbecich joins (~Thunderbi@syn-047-229-123-186.res.spectrum.com)
22:49:24 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
22:49:44 → justsomeguy joins (~justsomeg@user/justsomeguy)
22:51:25 → Sgeo joins (~Sgeo@user/sgeo)
22:55:11 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
22:55:13 → califax_ joins (~califax@user/califx)
22:56:00 × califax quits (~califax@user/califx) (Ping timeout: 264 seconds)
22:56:26 califax_ is now known as califax
22:59:34 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
23:01:45 × Tuplanolla quits (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
23:10:28 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:15:58 × Buliarous quits (~gypsydang@46.232.210.139) (Remote host closed the connection)
23:16:26 → Buliarous joins (~gypsydang@46.232.210.139)
23:17:26 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
23:18:38 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Quit: Client closed)
23:19:25 → LainIwakura joins (~LainIwaku@user/LainIwakura)
23:21:39 <monochrom> darkling: Actually our department chair has also received students' escalated tickets "I answered something but my prof gave me 0". >:)
23:22:28 <monochrom> There were 3 such cases and the profs were all different. It is becoming a meme across the board.
23:23:47 <int-e> . o O ( I asked ChatGPT and it said I should receive full marks. )
23:27:19 × LainIwakura quits (~LainIwaku@user/LainIwakura) (Quit: Client closed)
23:27:31 × jespada_ quits (~jespada@r179-25-42-1.dialup.adsl.anteldata.net.uy) (Quit: My Mac has gone to sleep. ZZZzzz…)
23:28:28 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:30:25 × tolgo quits (~Thunderbi@199.115.144.130) (Ping timeout: 276 seconds)
23:32:34 <monochrom> Oh yeah have you heard of this old joke: If you think you know everything, you can get a Bachelor's. When you find out you don't know anything, you can get a Master's. When you also find out that your thesis supervisor doesn't know anything either, you can get a PhD.
23:32:50 <monochrom> I have upgraded that to a modern version.
23:33:37 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
23:33:43 <monochrom> If you think LLMs know everything, you can get a Bachelor's. When you find out that LLMs don't know anything, you can get a Master's. When you find out that your thesis supervisor is also relying on LLMs, you can get a PhD.
23:33:46 <darkling> You learn more and more about less and less, until you know everything about nothing...
23:34:02 <darkling> (At which point, they give you a PhD to get rid of you).
23:35:52 <darkling> Somewhat glad I'm not in academia any more. Should have got out much earlier. Would have given me more time to get burned out and recover from industry... :/
23:37:36 × acidjnk_new quits (~acidjnk@p200300d6e71c4f61394430d048071491.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
23:44:15 → merijn joins (~merijn@host-vr.cgnat-g.v4.dfn.nl)
23:45:51 × harveypwca quits (~harveypwc@2601:246:d080:f6e0:27d6:8cc7:eca9:c46c) (Quit: Leaving)
23:46:48 <EvanR> I would like my Master's now
23:47:20 <EvanR> 🫴
23:47:45 <darkling> Don't bother. It's not worth it. :)
23:48:00 × Googulator47 quits (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu) (Quit: Client closed)
23:48:14 → Googulator47 joins (~Googulato@2a01-036d-0106-093f-1dc7-297e-fae3-e794.pool6.digikabel.hu)
23:48:40 <monochrom> Nah, Master's is OK, just don't get sucked into PhD. :)
23:48:42 <int-e> EvanR: those aren't requirements, they're consequences
23:49:01 <int-e> (also it's a joke)
23:49:10 × merijn quits (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
23:50:05 <EvanR> how do you I wasn't joking!
23:50:09 <EvanR> know
23:50:36 <monochrom> <poker face>Everyone is not joking</poker face>
23:50:39 <int-e> EvanR: I don't
23:51:17 <EvanR> this joke is serious
23:51:24 <int-e> EvanR: I mean, you were clearly joking. But I'm not sure what exactly you were joking about ;-)
23:54:15 × JuanDaugherty quits (~juan@user/JuanDaugherty) (Quit: praxis.meansofproduction.biz (juan@acm.org))
23:59:01 × ljdarj quits (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)

All times are in UTC on 2025-04-28.