Logs on 2024-03-09 (liberachat/#haskell)
| 00:00:46 | <renpose> | (ChatGPT claims it is impossible and Google was not of much help) |
| 00:01:16 | <geekosaur> | ph88, you have Data.C2Hsc in other-modules for the executable,, this causes it to be rebuilt for the executable. You probably want the executable to depend on the library instead |
| 00:02:26 | glguy | sees the highlight and then geekosaur having the right answer |
| 00:02:27 | × | jargon quits (~jargon@154.sub-174-205-226.myvzw.com) (Remote host closed the connection) |
| 00:02:38 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 00:03:27 | <ph88> | geekosaur, i rebuild everything library and executable. Not sure what you mean with missing executable stanza, it's on line 66 |
| 00:03:49 | <geekosaur> | yes, but its ghc-options doesn't have -Wno-incomplete-uni-patterns |
| 00:04:15 | <ph88> | ah it works like that |
| 00:04:17 | <geekosaur> | and because you listed Data.C2Hsc in its other-modules, it rebuilds that module again with the execcutable's ghc-options |
| 00:04:38 | <ph88> | geekosaur, did i mess up line 70? i thought i need to specify that the executable is using the module from the main library |
| 00:05:01 | <geekosaur> | you want to list the library in your build-depends |
| 00:05:22 | <geekosaur> | that is, you want the executable to have a dependency on c2hsc |
| 00:05:34 | <geekosaur> | which will be resolved to the library part |
| 00:06:10 | <ph88> | geekosaur, i did that because i was getting this warning Warning: The following modules should be added to exposed-modules or other-modules |
| 00:06:40 | <ph88> | In exe:c2hsc: Data.C2Hsc |
| 00:07:09 | <geekosaur> | that's because everything is using the same source directory (which defaults to .) so it finds the module while building the executable and wants to rebuild it again |
| 00:07:12 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
| 00:07:35 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 00:07:38 | <geekosaur> | normally you use different hs-sources dirs for different components, and have dependencies between the components |
| 00:08:12 | <ph88> | geekosaur, the library is in ./Data and the executable in . what do you mean same directory ? |
| 00:08:35 | <geekosaur> | Data is part of the library path (Data.C2Hsc) |
| 00:08:47 | <geekosaur> | so it is found from source directory . |
| 00:09:42 | <geekosaur> | that is, the source for a module Foo.Bar is Foo/Bar.hs |
| 00:09:44 | → | mizlan joins (~mizlan@wifi-131-179-21-178.host.ucla.edu) |
| 00:11:03 | <ph88> | aaah i see thanks |
| 00:11:49 | × | mizlan quits (~mizlan@wifi-131-179-21-178.host.ucla.edu) (Remote host closed the connection) |
| 00:12:27 | → | mizlan joins (~mizlan@2607:f010:2e9:b:41e2:3511:eccc:fc51) |
| 00:12:31 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 272 seconds) |
| 00:12:34 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 00:15:25 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 264 seconds) |
| 00:17:25 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 00:17:50 | → | califax joins (~califax@user/califx) |
| 00:22:09 | → | igemnace joins (~ian@user/igemnace) |
| 00:38:16 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 00:39:36 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 255 seconds) |
| 00:44:11 | <renpose> | It is not [distributive](https://github.com/ekmett/distributive), or is it? |
| 00:44:24 | <renpose> | oh my, i think i need a break from this |
| 00:44:57 | → | mvk joins (~mvk@2607:fea8:5c96:5800::f1d8) |
| 00:45:12 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 00:45:46 | × | mvk quits (~mvk@2607:fea8:5c96:5800::f1d8) (Client Quit) |
| 00:45:55 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 255 seconds) |
| 00:46:28 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.2.1) |
| 00:47:23 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 00:49:18 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 00:49:31 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 00:58:23 | → | Inst joins (~Inst@120.244.192.27) |
| 00:58:43 | <Inst> | did anyone ever try to make overloaded chars a thing in Haskell? |
| 00:58:53 | <Inst> | Can't possibly figure out what you'd use it for, but it'd be hilarious |
| 01:02:12 | × | califax quits (~califax@user/califx) (Remote host closed the connection) |
| 01:05:05 | × | dsrt^ quits (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Remote host closed the connection) |
| 01:07:53 | → | jargon joins (~jargon@154.sub-174-205-226.myvzw.com) |
| 01:08:43 | × | jargon quits (~jargon@154.sub-174-205-226.myvzw.com) (Remote host closed the connection) |
| 01:08:51 | × | ph88 quits (~ph88@2a02:8109:9e26:c800:f5bf:fee6:a40b:7301) (Remote host closed the connection) |
| 01:09:10 | → | califax joins (~califax@user/califx) |
| 01:10:08 | → | jargon joins (~jargon@154.sub-174-205-226.myvzw.com) |
| 01:12:36 | <haskellbridge> | <sm> Inst you troublemaker |
| 01:13:01 | <Inst> | Sorry I've been gone, I decided learning Marxism and Communism was more fun than Haskell |
| 01:13:03 | <haskellbridge> | <sm> stop having ideas 😆 |
| 01:13:16 | × | mizlan quits (~mizlan@2607:f010:2e9:b:41e2:3511:eccc:fc51) (Ping timeout: 268 seconds) |
| 01:13:56 | <Inst> | also I need to fulfill sclv's dream by making Haskell way too Red for Anduril to touch |
| 01:14:31 | <sclv> | lol |
| 01:17:19 | <jle`> | renpose: i've had pretty bad luck with chatgpt and haskell heh. it should be possible, since it's possible at least via generics-sop |
| 01:17:58 | <bontaq> | it's weird, I've gotten some alright results w it but I do have to tell it it's wrong to to check it's work a lot |
| 01:18:56 | <jle`> | i guess maybe with respect to type-level programming it struggles since i don't think there's much of a corpus for it to draw from |
| 01:20:01 | <jle`> | it would have to somehow get a mental model of dependently typed programming from the small corpus of dependently typed programs or literature and then synthesize it against the constantly changing GHC capabilities |
| 01:21:05 | <jle`> | (in the context of renpose's original question) |
| 01:23:01 | <sclv> | Inst btw i am in both a categorical topology reading group and a Capital vol 3 reading group :-) |
| 01:25:54 | → | mizlan joins (~mizlan@wifi-131-179-21-178.host.ucla.edu) |
| 01:30:11 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 01:30:24 | × | mizlan quits (~mizlan@wifi-131-179-21-178.host.ucla.edu) (Ping timeout: 260 seconds) |
| 01:30:51 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 01:36:25 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Read error: Connection reset by peer) |
| 01:36:25 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 01:37:06 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 01:37:35 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 01:37:52 | <bontaq> | part of a balanced meal, lil haskell, lil marx |
| 01:43:23 | <Inst> | On my copy it reads: |
| 01:44:02 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Remote host closed the connection) |
| 01:45:30 | <Inst> | 出版物中任何不符合中华人民共和国主权，宪法和法规的内容，该不认可。 |
| 01:45:42 | <Inst> | Any content in the publication that is not in accordance with the sovereignty of the People's Republic of China, its constitution and laws and regulations is not endorsed. |
| 01:45:43 | <Inst> | ;) |
| 01:46:17 | <int-e> | followed by 5 pages? |
| 01:49:25 | <Inst> | You can buy 1984 here both in Western editions and in translation. :) |
| 01:49:51 | <Inst> | I think it's more that the censor tried reading it, then gave up. :) |
| 01:52:19 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 01:53:41 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 02:00:02 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 02:01:03 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 255 seconds) |
| 02:01:05 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 02:01:13 | → | tri joins (~tri@ool-18bc2e74.dyn.optonline.net) |
| 02:03:04 | × | finsternis quits (~X@23.226.237.192) (Read error: Connection reset by peer) |
| 02:04:48 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 02:05:58 | × | tri quits (~tri@ool-18bc2e74.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 02:07:47 | → | finsternis joins (~X@23.226.237.192) |
| 02:24:12 | → | allan453 joins (~allan453@2804:18:40:f10b:58f8:8677:4901:5aa4) |
| 02:26:25 | × | allan453 quits (~allan453@2804:18:40:f10b:58f8:8677:4901:5aa4) (Client Quit) |
| 02:26:25 | <Inst> | sclv: did you guys do Mao yet? |
| 02:26:38 | <Inst> | I guess it's kiddy stuff compared to Capital. |
| 02:33:49 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 02:34:33 | <sclv> | yeah its just a fun little political economy and value theory reading group. lotta people that like to make little spreadsheet models of economic reproduction. |
| 02:44:15 | × | mulk quits (~mulk@p5b11243f.dip0.t-ipconnect.de) (Ping timeout: 255 seconds) |
| 02:44:59 | × | otto_s quits (~user@p4ff27cc1.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 02:45:51 | → | mizlan joins (~mizlan@2607:f010:2a7:1026:cd3d:92f4:f814:59c4) |
| 02:46:33 | → | otto_s joins (~user@p4ff27bc5.dip0.t-ipconnect.de) |
| 02:47:59 | → | mulk joins (~mulk@p5b2dc01b.dip0.t-ipconnect.de) |
| 02:55:18 | <Inst> | I guess it's the Dengist in me, but you should bother to do neoclassical economics as well; IIRC, Marx wrote Capital to explain why, despite his analysis, capitalism hadn't failed in the 1850s, and leftists in general have been waiting more than 170 years for the collapse of capitalism he envisioned to happen. |
| 03:01:00 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 03:02:43 | × | phma quits (phma@2001:5b0:215d:d9f8:8a50:43b0:3984:5f61) (Read error: Connection reset by peer) |
| 03:02:50 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:03:35 | → | phma joins (~phma@host-67-44-208-98.hnremote.net) |
| 03:05:03 | <bontaq> | any moment the contradictions will end it surely |
| 03:07:52 | <monochrom> | https://discourse.haskell.org/t/do-your-taxes-with-haskell/8942/6 is a more interesting and relevant kind of contradiction. |
| 03:08:25 | <monochrom> | Err nevermind, it's underspecified (too many solutions), not contradiction (no solution). |
| 03:13:59 | <sclv> | Inst, that's not my understanding at all but if we're to continue we should probably take it to #haskell-offtopic lol |
| 03:18:25 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 03:20:24 | <Inst> | yeah k |
| 03:42:49 | × | terrorjack quits (~terrorjac@2a01:4f8:c17:87f8::) (Quit: The Lounge - https://thelounge.chat) |
| 03:45:35 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 264 seconds) |
| 03:46:15 | → | terrorjack joins (~terrorjac@2a01:4f8:c17:87f8::) |
| 03:48:16 | × | mizlan quits (~mizlan@2607:f010:2a7:1026:cd3d:92f4:f814:59c4) (Ping timeout: 246 seconds) |
| 03:50:16 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-2678-8497-aa5c-7fa9.res6.spectrum.com) |
| 03:57:06 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 03:59:33 | × | td_ quits (~td@i53870902.versanet.de) (Ping timeout: 256 seconds) |
| 04:01:24 | → | td_ joins (~td@i5387090F.versanet.de) |
| 04:24:15 | × | aforemny quits (~aforemny@i59F516FB.versanet.de) (Ping timeout: 260 seconds) |
| 04:24:27 | → | aforemny_ joins (~aforemny@2001:9e8:6cc9:7200:b326:eda8:743b:1401) |
| 04:26:58 | → | ania123 joins (~ania123@94-43-231-47.dsl.utg.ge) |
| 04:32:54 | × | sp1ff quits (~user@c-24-21-45-157.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 04:33:38 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 04:37:12 | → | slack1256 joins (~slack1256@191.126.144.248) |
| 04:38:29 | <slack1256> | Does the RTS release memory (RSS) back the OS? If so when it? |
| 04:41:30 | <glguy> | slack1256: check out https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5036 |
| 04:41:35 | × | foul_owl quits (~kerry@157.97.134.168) (Quit: WeeChat 3.8) |
| 04:42:18 | → | foul_owl joins (~kerry@157.97.134.168) |
| 04:43:41 | <int-e> | https://gitlab.haskell.org/ghc/ghc/-/blob/master/rts/posix/OSMem.c#L644-650 is relevant too (RSS might not decrease immediately even when the RTS releases memory) |
| 04:58:47 | × | bontaq quits (~user@ool-45779c03.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 04:59:16 | → | igemnace joins (~ian@user/igemnace) |
| 04:59:44 | <slack1256> | This is great info, thanks glguy, int-e . |
| 05:06:05 | → | komikat joins (~akshitkr@218.185.248.66) |
| 05:06:29 | × | komikat_ quits (~akshitkr@218.185.248.66) (Read error: Connection reset by peer) |
| 05:30:46 | × | komikat quits (~akshitkr@218.185.248.66) (Read error: Connection reset by peer) |
| 05:31:00 | → | komikat joins (~akshitkr@218.185.248.66) |
| 05:31:05 | × | machinedgod quits (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 05:31:39 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Quit: peterbecich) |
| 05:32:07 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 05:33:22 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 05:33:54 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 05:49:22 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 05:54:48 | × | slack1256 quits (~slack1256@191.126.144.248) (Remote host closed the connection) |
| 05:57:38 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 252 seconds) |
| 06:06:34 | → | komikat_ joins (~akshitkr@218.185.248.66) |
| 06:06:51 | × | komikat quits (~akshitkr@218.185.248.66) (Read error: Connection reset by peer) |
| 06:07:16 | → | euphores joins (~SASL_euph@user/euphores) |
| 06:08:00 | → | oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 06:17:05 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 06:18:27 | × | notzmv quits (~daniel@user/notzmv) (Ping timeout: 255 seconds) |
| 06:29:17 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 06:46:02 | <endojelly> | Am I seeing it right that there are combinators to set state, but not to get state, in lens? |
| 06:46:17 | <endojelly> | Not a problem, I can just "gets", just wondering if I missed something. |
| 06:48:18 | → | Shaeto joins (~Shaeto@94.25.234.62) |
| 06:50:26 | × | stiell_ quits (~stiell@gateway/tor-sasl/stiell) (Ping timeout: 260 seconds) |
| 06:52:05 | × | m1dnight quits (~christoph@82.146.125.185) (Ping timeout: 240 seconds) |
| 06:52:22 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 06:55:41 | <c_wraith> | endojelly: are you looking for use? |
| 06:55:42 | <c_wraith> | > runState (do { x <- use _1 ; _2 += x }) (3,4) |
| 06:55:44 | <lambdabot> | ((),(3,7)) |
| 07:05:27 | × | oo_miguel quits (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) (Ping timeout: 272 seconds) |
| 07:08:08 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-2678-8497-aa5c-7fa9.res6.spectrum.com) (Remote host closed the connection) |
| 07:08:13 | → | jau joins (~user@2a04:4540:7216:6500:aa9c:7a13:5b21:2c7) |
| 07:12:22 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 260 seconds) |
| 07:13:59 | → | acidjnk_new3 joins (~acidjnk@p200300d6e737e708aca1d43a8c2c1f62.dip0.t-ipconnect.de) |
| 07:17:05 | <Shaeto> | hi, can someone check code https://onlinegdb.com/_Pd25PEum and recommend solution how to solve problem in line 3, i don't understand why compiler can't resolve types automatically |
| 07:19:24 | <c_wraith> | Shaeto: it's a precedence issue. It looks like you're hoping it will parse as blah * (sin $ 2 * g), but it parses as (blah * sin) $ (g * 2) |
| 07:19:51 | <c_wraith> | Shaeto: the easiest fix is to throw out the $ operator entirely and use use parens |
| 07:21:54 | × | dtman34 quits (~dtman34@2601:447:d001:ed50:6848:2021:a4eb:5671) (Ping timeout: 256 seconds) |
| 07:22:14 | <Shaeto> | @c_wraith thank you! okay, so, parens everythere in math :) |
| 07:22:14 | <lambdabot> | Unknown command, try @list |
| 07:22:52 | <c_wraith> | at least until you get comfortable with operator precedence. Parens are nicely unambiguous. |
| 07:28:11 | <Shaeto> | c_wraith: thank you! okay, parens solved problem really don't understand what is bad in the original formula |
| 07:28:31 | <c_wraith> | well, the way it parses, you're trying to multiple a number by a function |
| 07:32:43 | → | waleee joins (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 07:39:37 | × | rainbyte quits (~rainbyte@186.22.19.215) (Ping timeout: 268 seconds) |
| 07:43:46 | <Shaeto> | okay, new example with correct precedence but it does not work w/o parens ":t 0.020 * sin $ 2 * (3.0::Double)" and works now ":t 0.020 * (sin $ 2 * (3.0::Double))" |
| 07:44:23 | <c_wraith> | err, $ will always have lower precedence than * |
| 07:45:13 | <c_wraith> | so that's (0.020 * sin) $ (2 * (3 :: Double)) |
| 07:45:16 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 07:45:48 | <Shaeto> | but sin as a functional call have highest precedence so "2 * (3.0::Double)" must be calculated first ? |
| 07:46:37 | <c_wraith> | only if it's syntactically a function call |
| 07:46:53 | <c_wraith> | but since the token after sin is an operator, it's not syntactically a function call |
| 07:47:08 | <c_wraith> | function calls are a series of non-operator tokens in a row |
| 07:47:37 | <Shaeto> | okay, understand now problem is here "$ 2 *" |
| 07:48:56 | → | zetef joins (~quassel@95.77.17.251) |
| 07:49:03 | × | jinsun quits (~jinsun@user/jinsun) (Ping timeout: 256 seconds) |
| 07:49:20 | <c_wraith> | well, the problem is mixing two different precedences |
| 07:50:36 | <Shaeto> | c_wraith: understand, most books teach me to use . and $ but do not provide table of precedences nor examples :) |
| 07:51:12 | <c_wraith> | You can ask ghci for that |
| 07:51:24 | <c_wraith> | the :info or :i commnad will tell you precedence of operators |
| 07:52:01 | <c_wraith> | To anchor the information, $ has the lowest precedence (0), and . has the highest precedence (9) |
| 07:53:08 | <mauke> | function application has the highestest precedence (10), and record update has the highestestest precedence (11) |
| 07:53:24 | × | zetef quits (~quassel@95.77.17.251) (Ping timeout: 255 seconds) |
| 07:53:29 | <Shaeto> | one more question about . |
| 07:53:36 | → | zetef joins (~quassel@5.2.182.98) |
| 07:53:39 | <Shaeto> | daysSinceJ2000 :: Year -> MonthOfYear -> DayOfMonth -> Double |
| 07:53:43 | <endojelly> | c_wraith, ah, thanks! |
| 07:53:50 | <Shaeto> | sunEclipticLongitude :: Double -> Double |
| 07:54:04 | <Shaeto> | does not work: sunEclipticLongitudeAtDate = sunEclipticLongitude . daysSinceJ2000 |
| 07:54:35 | <mauke> | that's due to the definition of (.) |
| 07:54:44 | <mauke> | (f . g) x = f (g x) |
| 07:54:51 | <mauke> | it only composes functions of one argument |
| 07:55:21 | <mauke> | your code is saying: sunEclipticLongitudeAtDate x = sunEclipticLongitude (daysSinceJ2000 x) |
| 07:56:05 | <mauke> | which is an error because daysSinceJ2000 x is a function (it's will waiting for two more arguments), but sunEclipticLongitude expects a Double |
| 07:56:13 | <Shaeto> | okay, so, it must be : daysSinceJ2000 :: (Year -> MonthOfYear -> DayOfMonth) -> Double |
| 07:56:15 | <mauke> | s/will waiting/still waiting/ |
| 07:56:42 | <mauke> | Shaeto: huh? |
| 07:56:45 | <Shaeto> | sorry, i meant daysSinceJ2000 :: (Year, MonthOfYear, DayOfMonth) -> Double |
| 07:56:56 | <mauke> | yes, that would work |
| 07:57:51 | <Shaeto> | okay thank you, continue to calculate the sun position :) |
| 07:58:32 | → | Domitar joins (~Domitar@193.198.16.218) |
| 07:58:58 | → | jinsun joins (~jinsun@user/jinsun) |
| 08:00:13 | <mauke> | > let { f = fun "f" :: Expr -> Expr } in (f . g) x |
| 08:00:14 | <lambdabot> | f (g x) |
| 08:00:20 | <mauke> | > let { f = fun "f" :: Expr -> Expr } in ((f .) . g) x y |
| 08:00:22 | <lambdabot> | f (g x y) |
| 08:00:34 | <mauke> | > let { f = fun "f" :: Expr -> Expr } in (((f .) .) . g) x y z |
| 08:00:36 | <lambdabot> | f (g x y z) |
| 08:12:34 | → | harveypwca joins (~harveypwc@2601:246:c200:2740:15b6:f225:14ff:9821) |
| 08:27:26 | → | m1dnight joins (~christoph@82.146.125.185) |
| 08:29:17 | → | notzmv joins (~daniel@user/notzmv) |
| 08:29:38 | → | misterfish joins (~misterfis@84.53.85.146) |
| 08:37:44 | × | phma quits (~phma@host-67-44-208-98.hnremote.net) (Read error: Connection reset by peer) |
| 08:38:40 | → | phma joins (phma@2001:5b0:211b:9188:599a:22ec:6887:20f1) |
| 08:40:20 | → | _ht joins (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) |
| 08:41:23 | → | causal joins (~eric@50.35.85.7) |
| 08:43:06 | × | euphores quits (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 08:56:29 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 08:59:15 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 09:00:32 | → | euphores joins (~SASL_euph@user/euphores) |
| 09:12:29 | × | Domitar quits (~Domitar@193.198.16.218) (Remote host closed the connection) |
| 09:14:16 | × | waleee quits (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 268 seconds) |
| 09:22:46 | → | dtman34 joins (~dtman34@2601:447:d001:ed50:71b1:9fdc:d135:745b) |
| 09:34:10 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 264 seconds) |
| 09:37:49 | × | Sgeo quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 09:38:59 | × | Shaeto quits (~Shaeto@94.25.234.62) (Quit: WeeChat 4.2.1) |
| 09:43:11 | × | peterbecich quits (~Thunderbi@047-229-123-186.res.spectrum.com) (Ping timeout: 264 seconds) |
| 09:59:04 | × | econo_ quits (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 10:12:30 | → | Tuplanolla joins (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 10:13:40 | × | tzh quits (~tzh@c-73-164-206-160.hsd1.or.comcast.net) (Quit: zzz) |
| 10:18:16 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 10:19:13 | → | danza joins (~francesco@151.43.204.95) |
| 10:32:42 | × | jinsun quits (~jinsun@user/jinsun) (Read error: Connection reset by peer) |
| 10:36:58 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 10:48:19 | → | rvalue joins (~rvalue@user/rvalue) |
| 10:49:09 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 10:57:24 | → | stiell_ joins (~stiell@gateway/tor-sasl/stiell) |
| 11:10:12 | × | igemnace quits (~ian@user/igemnace) (Read error: Connection reset by peer) |
| 11:10:47 | × | Square quits (~Square@user/square) (Ping timeout: 264 seconds) |
| 11:13:33 | × | noumenon quits (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 11:27:50 | → | igemnace joins (~ian@user/igemnace) |
| 11:30:18 | <raehik> | What do the indexXOffAddr# primops do exactly? They return primitive types, but are somehow not stateful (no State# s tokens), so I can't believe they're reading arbitrary addresses |
| 11:39:51 | × | harveypwca quits (~harveypwc@2601:246:c200:2740:15b6:f225:14ff:9821) (Quit: Leaving) |
| 11:40:26 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 11:47:56 | → | Joao[3] joins (~Joao003@190.108.99.67) |
| 11:50:34 | → | __monty__ joins (~toonn@user/toonn) |
| 12:04:30 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 260 seconds) |
| 12:06:40 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-2678-8497-aa5c-7fa9.res6.spectrum.com) |
| 12:06:43 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 12:08:01 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 256 seconds) |
| 12:11:49 | × | acidjnk_new3 quits (~acidjnk@p200300d6e737e708aca1d43a8c2c1f62.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 12:12:13 | → | fmd joins (~fmd@user/framend) |
| 12:13:35 | × | phma quits (phma@2001:5b0:211b:9188:599a:22ec:6887:20f1) (Read error: Connection reset by peer) |
| 12:14:47 | × | Lycurgus quits (~georg@user/Lycurgus) (Quit: leaving) |
| 12:15:37 | → | phma joins (~phma@host-67-44-208-101.hnremote.net) |
| 12:20:45 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 12:31:53 | <tomsmeding> | raehik: the ones with the "this is only available on LLVM" warning? |
| 12:33:24 | <raehik> | tomsmeding: yes, though not just those |
| 12:33:41 | <raehik> | I figured it out, they're for reading from immutable memory. see #ghc |
| 12:34:25 | <raehik> | the Haddock docstrings are a bit lacking for some of the primops, specifically the ones reading from immutable Addr# (fairly unintuitive) |
| 12:35:13 | tomsmeding | should just lurk in #ghc instead of leaving each time |
| 12:36:27 | <raehik> | with all my recent messing around i should add it back to my autojoin xd |
| 12:43:54 | <tomsmeding> | mauke: https://hackage.haskell.org/package/composition-1.0.2.2/docs/Data-Composition.html |
| 12:48:14 | <jackdk> | tomsmeding: in a similar vein: https://raw.githubusercontent.com/mxswd/flip-plus/master/Control/FlipPlus.hs |
| 12:55:38 | × | danza quits (~francesco@151.43.204.95) (Ping timeout: 252 seconds) |
| 12:58:05 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 240 seconds) |
| 13:11:33 | → | CiaoSen joins (~Jura@2a05:5800:2a2:9900:e6b9:7aff:fe80:3d03) |
| 13:16:29 | × | renpose quits (~renpose@user/renpose) (Ping timeout: 250 seconds) |
| 13:20:03 | × | glguy quits (g@libera/staff/glguy) (Ping timeout: 612 seconds) |
| 13:48:17 | → | bontaq joins (~user@ool-45779c03.dyn.optonline.net) |
| 13:50:05 | → | glguy joins (g@libera/staff/glguy) |
| 13:55:26 | → | acidjnk_new3 joins (~acidjnk@p200300d6e737e7747555095b6f843b59.dip0.t-ipconnect.de) |
| 14:03:00 | × | L29Ah quits (~L29Ah@wikipedia/L29Ah) (Read error: Connection reset by peer) |
| 14:05:04 | → | L29Ah joins (~L29Ah@wikipedia/L29Ah) |
| 14:07:47 | → | Unicorn_Princess joins (~Unicorn_P@user/Unicorn-Princess/x-3540542) |
| 14:07:48 | × | Vajb quits (~Vajb@n70t65z9ztei3blo55b-1.v6.elisa-mobile.fi) (Ping timeout: 260 seconds) |
| 14:08:38 | <komikat_> | hey, I was reading http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html and I kinda don't get why this is true: |
| 14:08:45 | <komikat_> | Exercise Three |
| 14:08:46 | <komikat_> | Show that lift f * lift g = lift (f.g) |
| 14:10:10 | → | Vajb joins (~Vajb@n70t65z9ztei3blo55b-1.v6.elisa-mobile.fi) |
| 14:11:48 | <ncf> | inline definitions and compute? |
| 14:15:09 | <ncf> | spoilers: https://f.monade.li/IQboLk |
| 14:18:55 | <ncf> | or more abstractly, using just the monad law (bind f . unit = f): https://f.monade.li/IwFwLl |
| 14:21:18 | × | sudden quits (~cat@user/sudden) (Ping timeout: 255 seconds) |
| 14:21:58 | → | sudden joins (~cat@user/sudden) |
| 14:33:01 | × | rvalue quits (~rvalue@user/rvalue) (Read error: Connection reset by peer) |
| 14:33:20 | → | rvalue joins (~rvalue@user/rvalue) |
| 14:37:20 | <komikat_> | ncf: i'm not sure what the "*" means in this context |
| 14:38:01 | <mauke> | Given a pair of debuggable functions, f' and g', we can now compose them together to make a new debuggable function bind f' . g'. Write this composition as f'*g'. |
| 14:38:33 | <mauke> | or in other words: f' * g' = bind f' . g' |
| 14:38:48 | <mauke> | unfortunately the definitions are kind of hidden throughout the text |
| 14:39:15 | <komikat_> | makes sense |
| 14:45:51 | × | glguy quits (g@libera/staff/glguy) (Ping timeout: 612 seconds) |
| 14:47:36 | → | misterfish joins (~misterfis@87.215.131.102) |
| 14:51:26 | → | AlexNoo_ joins (~AlexNoo@5.139.232.124) |
| 14:53:49 | × | AlexZenon quits (~alzenon@94.233.241.172) (Ping timeout: 264 seconds) |
| 14:55:14 | × | AlexNoo quits (~AlexNoo@94.233.241.172) (Ping timeout: 256 seconds) |
| 14:55:32 | AlexNoo_ | is now known as AlexNoo |
| 14:57:26 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 15:00:11 | → | __monty__ joins (~toonn@user/toonn) |
| 15:04:16 | → | AlexZenon joins (~alzenon@5.139.232.124) |
| 15:13:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:14:10 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Client Quit) |
| 15:14:54 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 15:18:07 | → | glguy joins (g@libera/staff/glguy) |
| 15:21:54 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 260 seconds) |
| 15:22:09 | × | ania123 quits (~ania123@94-43-231-47.dsl.utg.ge) (Ping timeout: 250 seconds) |
| 15:27:00 | → | noumenon joins (~noumenon@113.51-175-156.customer.lyse.net) |
| 15:31:21 | × | glguy quits (g@libera/staff/glguy) (Ping timeout: 612 seconds) |
| 15:32:33 | → | o-90 joins (~o-90@gateway/tor-sasl/o-90) |
| 15:33:42 | × | o-90 quits (~o-90@gateway/tor-sasl/o-90) (Client Quit) |
| 15:38:00 | × | jau quits (~user@2a04:4540:7216:6500:aa9c:7a13:5b21:2c7) (Quit: Leaving) |
| 15:42:25 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 264 seconds) |
| 15:44:46 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 260 seconds) |
| 15:45:23 | → | machinedgod joins (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 15:52:56 | → | ania123 joins (~ania123@94-43-231-47.dsl.utg.ge) |
| 15:54:26 | → | glguy joins (g@libera/staff/glguy) |
| 16:04:46 | × | Joao[3] quits (~Joao003@190.108.99.67) (Ping timeout: 264 seconds) |
| 16:05:00 | → | adanwan_ joins (~adanwan@gateway/tor-sasl/adanwan) |
| 16:05:18 | × | chiselfuse quits (~chiselfus@user/chiselfuse) (Ping timeout: 260 seconds) |
| 16:05:18 | × | adanwan quits (~adanwan@gateway/tor-sasl/adanwan) (Ping timeout: 260 seconds) |
| 16:05:29 | → | Joao[3] joins (~Joao003@190.108.99.67) |
| 16:05:46 | × | ChaiTRex quits (~ChaiTRex@user/chaitrex) (Ping timeout: 260 seconds) |
| 16:07:43 | → | misterfish joins (~misterfis@87.215.131.102) |
| 16:07:45 | → | chiselfuse joins (~chiselfus@user/chiselfuse) |
| 16:08:00 | → | ChaiTRex joins (~ChaiTRex@user/chaitrex) |
| 16:22:04 | <tomsmeding> | jackdk: that is ridiculous, I love it |
| 16:24:13 | → | agrosant joins (~agrosant@188.4.221.80.dsl.dyn.forthnet.gr) |
| 16:27:07 | × | CiaoSen quits (~Jura@2a05:5800:2a2:9900:e6b9:7aff:fe80:3d03) (Ping timeout: 260 seconds) |
| 16:34:41 | × | ania123 quits (~ania123@94-43-231-47.dsl.utg.ge) (Quit: Client closed) |
| 16:39:48 | → | econo_ joins (uid147250@id-147250.tinside.irccloud.com) |
| 16:46:55 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 16:52:27 | × | fmd quits (~fmd@user/framend) (Ping timeout: 268 seconds) |
| 17:05:01 | → | ania123 joins (~ania123@94-43-231-47.dsl.utg.ge) |
| 17:05:46 | → | fmd joins (~fmd@2a02-8429-4b52-f901-b9d3-e786-8cb7-0e3d.rev.sfr.net) |
| 17:10:21 | → | tzh joins (~tzh@c-73-164-206-160.hsd1.or.comcast.net) |
| 17:12:45 | × | glguy quits (g@libera/staff/glguy) (Ping timeout: 612 seconds) |
| 17:12:50 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 17:24:05 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 17:25:48 | × | misterfish quits (~misterfis@87.215.131.102) (Ping timeout: 255 seconds) |
| 17:28:20 | → | ph88 joins (~ph88@2a02:8109:9e26:c800:61b8:7e22:3ff5:acf1) |
| 17:30:12 | <ph88> | i have this code which type checks https://bpa.st/MZKA i'm looking for ways to make it more concise. For example i wonder if it is possible to map over the error somehow so that i don't have to do runError twice. Does someone have some advises on how to improve this code ? |
| 17:30:29 | <ph88> | This is relevant documentation https://hackage.haskell.org/package/effectful-core-2.3.0.1/docs/Effectful-Error-Static.html |
| 17:35:43 | <ph88> | hmm actually i think i'm already on my way to reduce this code |
| 17:38:17 | → | azimut joins (~azimut@gateway/tor-sasl/azimut) |
| 17:38:41 | <ph88> | improvement but still could be clearer https://bpa.st/QYGQ |
| 17:40:41 | → | rito joins (~ritog@45.112.243.170) |
| 17:46:22 | × | destituion quits (~destituio@2a02:2121:650:17b6:dadb:8eeb:69ad:5745) (Ping timeout: 256 seconds) |
| 17:46:34 | → | destituion joins (~destituio@2001:4644:c37:0:6086:64f4:a213:b80d) |
| 17:50:07 | × | rito quits (~ritog@45.112.243.170) (Quit: Leaving) |
| 17:56:12 | → | target_i joins (~target_i@user/target-i/x-6023099) |
| 17:57:47 | × | a51 quits (a51@gateway/vpn/protonvpn/a51) (Quit: WeeChat 4.2.1) |
| 17:58:16 | × | tabemann quits (~tabemann@2600:1700:7990:24e0:cad5:895e:d141:167b) (Remote host closed the connection) |
| 17:58:35 | → | tabemann joins (~tabemann@2600:1700:7990:24e0:bade:358a:4ab3:923a) |
| 17:59:44 | → | misterfish joins (~misterfis@84.53.85.146) |
| 17:59:51 | × | ania123 quits (~ania123@94-43-231-47.dsl.utg.ge) (Quit: Client closed) |
| 18:07:17 | × | puke quits (~puke@user/puke) (Ping timeout: 272 seconds) |
| 18:15:18 | × | causal quits (~eric@50.35.85.7) (Quit: WeeChat 4.1.1) |
| 18:15:49 | <Joao[3]> | How do I get the last element of a list, while providing a default value if the list is empty? |
| 18:19:41 | → | jespada_ joins (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) |
| 18:21:41 | × | jespada quits (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Ping timeout: 240 seconds) |
| 18:22:20 | × | rvalue quits (~rvalue@user/rvalue) (Ping timeout: 252 seconds) |
| 18:24:30 | <monochrom> | if null xs then default else last xs |
| 18:28:01 | → | rvalue joins (~rvalue@user/rvalue) |
| 18:29:48 | <int-e> | :t fromMaybe ?default . listToMaybe |
| 18:29:49 | <lambdabot> | (?default::c) => [c] -> c |
| 18:29:58 | → | michalz joins (~michalz@185.246.207.222) |
| 18:32:36 | <ncf> | wait what |
| 18:32:43 | <geekosaur> | int-e, that doesn't produce the last item in a non-empty list |
| 18:32:49 | <Joao[3]> | listToMaybe gets the first item |
| 18:32:54 | <mauke> | :t last . (++ [?default]) |
| 18:32:55 | <lambdabot> | (?default::c) => [c] -> c |
| 18:33:05 | <Joao[3]> | that just returns default |
| 18:33:09 | <int-e> | geekosaur: ah |
| 18:33:11 | <ncf> | am i having a stroke |
| 18:33:13 | <ncf> | :t ?default |
| 18:33:14 | <lambdabot> | (?default::t) => t |
| 18:33:22 | <ncf> | :t ?what |
| 18:33:23 | <lambdabot> | (?what::t) => t |
| 18:33:25 | <mauke> | :t last . (++ [?renault]) |
| 18:33:26 | <lambdabot> | (?renault::c) => [c] -> c |
| 18:33:43 | <ncf> | What Is This |
| 18:33:53 | <mauke> | :t ?what ?is ?this |
| 18:33:54 | <lambdabot> | (?is::t1, ?this::t2, ?what::t1 -> t2 -> t3) => t3 |
| 18:33:54 | <int-e> | an implicit argument |
| 18:33:58 | <Joao[3]> | :t fromMaybe ?default . listToMaybe . reverse |
| 18:33:59 | <lambdabot> | (?default::c) => [c] -> c |
| 18:34:14 | <ncf> | > since 6.8.1 |
| 18:34:15 | <lambdabot> | error: |
| 18:34:15 | <lambdabot> | Variable not in scope: since :: t0 -> b0 -> c |
| 18:34:27 | <ncf> | i must be from an alternate reality |
| 18:34:42 | <geekosaur> | they're not used very often |
| 18:34:54 | <Joao[3]> | "am i having a stroke" yes you are |
| 18:35:11 | <geekosaur> | https://chrisdone.com/posts/whats-wrong-with-implicitparams/ |
| 18:35:36 | <monochrom> | Implicit parameters are how HasCallStack works. >:) |
| 18:35:39 | <int-e> | ncf: Ironically I essentially never use implicit arguments, but lambdabot is one context where they're occasionally useful... it's more pleasent to write ... ?default ... than to write a lambda abstraction \default -> ... default ... |
| 18:35:41 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 18:35:54 | <Joao[3]> | now let's make it point free >:) |
| 18:36:01 | <mauke> | :t last (theList ++ [?theDefault]) |
| 18:36:02 | <lambdabot> | error: |
| 18:36:02 | <lambdabot> | • Variable not in scope: theList :: [a] |
| 18:36:02 | <lambdabot> | • Perhaps you meant one of these: |
| 18:36:05 | <mauke> | :t last (?theList ++ [?theDefault]) |
| 18:36:06 | <lambdabot> | (?theDefault::a, ?theList::[a]) => a |
| 18:36:09 | <mauke> | there we go |
| 18:36:20 | <Joao[3]> | that just returns the default |
| 18:36:27 | <mauke> | true, I'm dumb |
| 18:36:37 | <mauke> | but at least I got the implicit parameters right! |
| 18:36:49 | <Joao[3]> | @pl \d -> fromMaybe d . listToMaybe . reverse |
| 18:36:49 | <lambdabot> | (. (listToMaybe . reverse)) . fromMaybe |
| 18:36:58 | <monochrom> | foo d xs = if null xs then d else last xs. Now you can use foo in pointfree code. |
| 18:36:59 | <int-e> | it should be last (?default : ?list) instead |
| 18:37:11 | <int-e> | (mauke's code that is) |
| 18:37:22 | <mauke> | thanks |
| 18:37:38 | <int-e> | I guess we've now mixed up head and last once each :) |
| 18:37:46 | <Joao[3]> | also the compiler knows you're stupid and even says it's type `a` |
| 18:38:05 | <mauke> | the type is correct from what I can see |
| 18:38:15 | <ncf> | > ?a + ?b |
| 18:38:17 | <lambdabot> | mueval-core: internal error: PAP object (0x42041f4be8) entered! |
| 18:38:17 | <lambdabot> | (GHC version 8.10.2 for x86_64_unknown_linux) |
| 18:38:17 | <lambdabot> | Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug |
| 18:38:18 | <int-e> | (my type was correct too) |
| 18:38:20 | <ncf> | lol |
| 18:38:31 | <int-e> | ncf: ow |
| 18:38:33 | <ncf> | % ?a + ?b |
| 18:38:33 | <yahb2> | <interactive>:281:1: error: ; • Unbound implicit parameters (?a::Integer, ?b::Integer) ; arising from a use of ‘it’ ; • In the first argument of ‘Yahb2Defs.limitedPrint’, namely ‘it... |
| 18:38:38 | <ncf> | lmao |
| 18:38:56 | <mauke> | @pl \d xs -> last (d : xs) |
| 18:38:56 | <lambdabot> | (last .) . (:) |
| 18:39:10 | <Joao[3]> | -_- |
| 18:40:28 | <int-e> | (It's 99.99% not a ghc bug, mueval uses unsafeCoerce after some manual type-checking that appears to be insufficient in this case) |
| 18:41:00 | <Joao[3]> | > let f = f in f |
| 18:41:02 | <lambdabot> | *Exception: <<loop>> |
| 18:42:55 | <Joao[3]> | > let f _ = f f in f f -- let's see what happens!!! |
| 18:42:56 | <lambdabot> | error: |
| 18:42:56 | <lambdabot> | • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t2 |
| 18:42:57 | <lambdabot> | • In the first argument of ‘f’, namely ‘f’ |
| 18:43:09 | <mauke> | @v |
| 18:43:09 | <lambdabot> | Just 'J' |
| 18:44:53 | <int-e> | > let f :: a -> b; f = f f in f f |
| 18:44:55 | <lambdabot> | *Exception: <<loop>> |
| 18:45:15 | <Joao[3]> | > let v = show v in v |
| 18:45:17 | <lambdabot> | "\"\\\"\\\\\\\"\\\\\\\\\\\\\\\"\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\"\\\\\\\\\\\\\... |
| 18:45:23 | <int-e> | > let f :: a -> b; f _ = f f in f f |
| 18:45:29 | <lambdabot> | mueval-core: Time limit exceeded |
| 18:46:37 | <int-e> | Joao[3]: an ancient version of lambdabot wrapped the expression in something like `let v = <expr> in show v`, so you could give `show v` as the expression and it would print that fixed point |
| 18:46:41 | <int-e> | > fix show |
| 18:46:43 | <lambdabot> | "\"\\\"\\\\\\\"\\\\\\\\\\\\\\\"\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\"\\\\\\\\\\\\\... |
| 18:48:00 | <Joao[3]> | > show show |
| 18:48:01 | <lambdabot> | "<() -> [Char]>" |
| 18:48:11 | <Joao[3]> | > iterate show show |
| 18:48:13 | <lambdabot> | error: |
| 18:48:13 | <lambdabot> | • Couldn't match type ‘a0 -> String’ with ‘[Char]’ |
| 18:48:13 | <lambdabot> | Expected type: String |
| 18:48:24 | <Joao[3]> | > iterate show $ show show |
| 18:48:25 | <lambdabot> | ["<() -> [Char]>","\"<() -> [Char]>\"","\"\\\"<() -> [Char]>\\\"\"","\"\\\"\... |
| 18:48:55 | <Joao[3]> | > (iterate show $ show show)!!100 |
| 18:48:56 | <lambdabot> | "\"\\\"\\\\\\\"\\\\\\\\\\\\\\\"\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\"\\\\\\\\\\\\\... |
| 18:53:21 | × | igemnace quits (~ian@user/igemnace) (Quit: WeeChat 4.2.1) |
| 18:54:48 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 19:04:55 | → | elnegro joins (elnegro@r167-57-20-188.dialup.adsl.anteldata.net.uy) |
| 19:08:23 | × | vgtw quits (~vgtw@user/vgtw) (Ping timeout: 264 seconds) |
| 19:10:53 | → | elnegro1 joins (elnegro@r167-57-9-32.dialup.adsl.anteldata.net.uy) |
| 19:11:41 | × | elnegro quits (elnegro@r167-57-20-188.dialup.adsl.anteldata.net.uy) (Ping timeout: 240 seconds) |
| 19:11:51 | → | vgtw joins (~vgtw@user/vgtw) |
| 19:12:03 | <tomsmeding> | I see you guys have been useful today |
| 19:12:19 | → | oo_miguel joins (~Thunderbi@78-11-181-16.static.ip.netia.com.pl) |
| 19:13:25 | <Joao[3]> | > fix id -- :) |
| 19:13:26 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 19:13:27 | <lambdabot> | *Exception: <<loop>> |
| 19:13:46 | × | benjaminl quits (~benjaminl@user/benjaminl) (Remote host closed the connection) |
| 19:14:03 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 19:17:31 | <Joao[3]> | > fix fix -- >:D |
| 19:17:32 | <lambdabot> | error: |
| 19:17:33 | <lambdabot> | • Occurs check: cannot construct the infinite type: a ~ a -> a |
| 19:17:33 | <lambdabot> | Expected type: a -> a |
| 19:18:10 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 19:18:20 | → | hueso_ joins (~root@user/hueso) |
| 19:18:54 | × | hueso quits (~root@user/hueso) (Read error: Connection reset by peer) |
| 19:21:16 | × | hueso_ quits (~root@user/hueso) (Client Quit) |
| 19:21:31 | → | Lycurgus joins (~georg@user/Lycurgus) |
| 19:22:49 | → | hueso joins (~root@user/hueso) |
| 19:24:06 | <EvanR> | fix error |
| 19:24:08 | <EvanR> | break error |
| 19:24:09 | <EvanR> | break fix |
| 19:24:31 | <tomsmeding> | :t break |
| 19:24:32 | <lambdabot> | (a -> Bool) -> [a] -> ([a], [a]) |
| 19:24:42 | <tomsmeding> | :t break fix |
| 19:24:43 | <lambdabot> | [Bool -> Bool] -> ([Bool -> Bool], [Bool -> Bool]) |
| 19:24:48 | <EvanR> | lol |
| 19:25:11 | tomsmeding | was expecting "'break' not defined", had forgotten about this function |
| 19:25:23 | <EvanR> | it's a good one |
| 19:25:49 | <tomsmeding> | 'break fix' is not terribly useful though lol |
| 19:26:00 | <EvanR> | it does explain the need to fix fix though |
| 19:26:07 | <EvanR> | unfortunate that it doesn't typecheck |
| 19:27:05 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 19:27:17 | <tomsmeding> | any function f of type Bool -> Bool for which 'fix f' terminates is either 'const True' or 'const False' |
| 19:28:24 | <EvanR> | so there's at least two options |
| 19:28:30 | <tomsmeding> | :t break ($ False) |
| 19:28:32 | <EvanR> | then [Bool -> Bool] can do a lot |
| 19:28:33 | <lambdabot> | [Bool -> Bool] -> ([Bool -> Bool], [Bool -> Bool]) |
| 19:28:44 | <tomsmeding> | for all parts of the output where both terminate, this is exactly the same function :') |
| 19:28:45 | <EvanR> | like encode reals |
| 19:30:04 | <EvanR> | const True and const False are well behaved in the sense you can check for them |
| 19:30:25 | <EvanR> | tell them apart |
| 19:30:53 | × | benjaminl quits (~benjaminl@user/benjaminl) (Ping timeout: 240 seconds) |
| 19:31:08 | → | benjaminl joins (~benjaminl@user/benjaminl) |
| 19:32:30 | → | peterbecich joins (~Thunderbi@047-229-123-186.res.spectrum.com) |
| 19:39:21 | <ncf> | fun fact: for any function f :: Bool -> Bool, f (f True) is the existential quantification of f |
| 19:39:34 | <ncf> | that is, f (f True) == True iff ∃ b. f b == True |
| 19:39:55 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Remote host closed the connection) |
| 19:40:03 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 19:45:12 | ← | elnegro1 parts (elnegro@r167-57-9-32.dialup.adsl.anteldata.net.uy) () |
| 19:46:52 | × | Joao[3] quits (~Joao003@190.108.99.67) (Quit: Bye!) |
| 19:52:53 | → | ania123 joins (~ania123@94-43-231-47.dsl.utg.ge) |
| 19:55:37 | <monochrom> | That is interesting. :) |
| 19:58:48 | × | dcoutts quits (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) (Ping timeout: 255 seconds) |
| 19:59:42 | → | yangby joins (~secret@115.192.99.212) |
| 20:06:30 | → | jm_ joins (~jm@pool-108-45-177-252.washdc.fios.verizon.net) |
| 20:12:03 | × | fmd quits (~fmd@2a02-8429-4b52-f901-b9d3-e786-8cb7-0e3d.rev.sfr.net) (Ping timeout: 272 seconds) |
| 20:12:45 | × | jm_ quits (~jm@pool-108-45-177-252.washdc.fios.verizon.net) (Ping timeout: 255 seconds) |
| 20:13:23 | × | yangby quits (~secret@115.192.99.212) (Quit: Go out for a walk and buy a drink.) |
| 20:21:51 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 20:22:43 | → | zetef_ joins (~quassel@5.2.182.98) |
| 20:23:23 | × | zetef_ quits (~quassel@5.2.182.98) (Client Quit) |
| 20:25:48 | × | zetef quits (~quassel@5.2.182.98) (Ping timeout: 255 seconds) |
| 20:29:51 | → | Joao[3] joins (~Joao003@190.108.99.67) |
| 20:30:46 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 255 seconds) |
| 20:31:08 | × | Joao[3] quits (~Joao003@190.108.99.67) (Remote host closed the connection) |
| 20:31:32 | → | Joao[3] joins (~Joao003@190.108.99.67) |
| 20:32:29 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 20:43:17 | × | santiagopim quits (~user@90.167.66.131) (Ping timeout: 240 seconds) |
| 20:43:29 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 20:50:29 | × | __monty__ quits (~toonn@user/toonn) (Ping timeout: 240 seconds) |
| 20:52:35 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 20:59:40 | → | cole-k joins (~cole@024-043-123-092.biz.spectrum.com) |
| 21:00:20 | <cole-k> | Is there something like cargo-dist (https://github.com/axodotdev/cargo-dist) for autogenerating a workflow to generate binaries for a release? |
| 21:01:32 | <cole-k> | best i found was this from a reddit thread: https://gist.github.com/aspidites/b27b1326fada1506f8f457286e8df5db |
| 21:05:51 | × | hgolden quits (~hgolden@2603-8000-9d00-3ed1-2678-8497-aa5c-7fa9.res6.spectrum.com) (Read error: Connection reset by peer) |
| 21:06:01 | × | driib quits (~driib@vmi931078.contaboserver.net) (Quit: The Lounge - https://thelounge.chat) |
| 21:06:46 | → | hgolden joins (~hgolden@2603-8000-9d00-3ed1-2678-8497-aa5c-7fa9.res6.spectrum.com) |
| 21:09:20 | × | _ht quits (~Thunderbi@28-52-174-82.ftth.glasoperator.nl) (Quit: _ht) |
| 21:11:10 | → | bgamari_ joins (~bgamari@64.223.200.57) |
| 21:11:25 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:11:35 | × | bgamari quits (~bgamari@64.223.237.41) (Ping timeout: 272 seconds) |
| 21:13:36 | <Joao[3]> | I have an idea: If you want `tail` to return `[]` if the list is empty, just use `drop 1` instead >:) |
| 21:14:52 | <haskellbridge> | <sm> indeed, take and drop are sometimes useful that way |
| 21:15:40 | <haskellbridge> | <sm> otherwise I like to use safe's tailDef |
| 21:16:01 | <Joao[3]> | what is <sm> |
| 21:16:08 | → | driib joins (~driib@vmi931078.contaboserver.net) |
| 21:16:24 | <sm> | that is me |
| 21:16:33 | × | misterfish quits (~misterfis@84.53.85.146) (Ping timeout: 256 seconds) |
| 21:16:56 | <Joao[3]> | oh... why are they pinging you then if they're talking to me |
| 21:17:24 | <sm> | it's because I was talking from matrix. A bridge copied those messages here. |
| 21:17:36 | <Joao[3]> | oh |
| 21:17:49 | <sm> | the formatting is a bit weird. |
| 21:18:24 | <sm> | why is it always shown as <s_m> here, geekosaur ? |
| 21:20:22 | × | cole-k quits (~cole@024-043-123-092.biz.spectrum.com) (Ping timeout: 264 seconds) |
| 21:20:23 | <geekosaur> | because it inserts a zero-width space to try to prevent pinging |
| 21:20:39 | <sm> | aha |
| 21:20:46 | → | cole-k joins (~cole@024-043-123-092.biz.spectrum.com) |
| 21:21:16 | <tomsmeding> | (weechat doesn't show the ZWSP) |
| 21:21:27 | sm | is using erc |
| 21:21:36 | tomsmeding | uses vim |
| 21:21:56 | <ski> | sm : no. it's shown as "<sm>", not as "<s_m>", with a ZWSP (U+200B ZERO WIDTH SPACE) after the "s" |
| 21:22:13 | <geekosaur> | depends on the client |
| 21:22:21 | <Joao[3]> | geekosaur: true |
| 21:22:25 | <geekosaur> | we already know of a few which do weird things when they see ZWSP |
| 21:22:34 | <Joao[3]> | i use hexchat and it doesn't show the ZWSP |
| 21:22:39 | ski | 's suggested it not insert that, at least if there's no nick with that name on the IRC side, in the channel |
| 21:22:42 | <tomsmeding> | honestly it's not too surprising that a client would insert a replacement character when it finds non-ascii characters in a nick |
| 21:23:00 | → | Shaeto joins (~Shaeto@94.25.234.62) |
| 21:23:04 | <geekosaur> | sadly there's not a lot I can do unless I want to take over matterbridge |
| 21:23:05 | <ski> | (to me, it displays the ZWSP as a dotted box around the "s" (first character of nickname)) |
| 21:23:14 | <tomsmeding> | (there is, in this case, though) |
| 21:23:29 | <geekosaur> | it doesn't track who's on either side of the bridge, for example |
| 21:24:09 | <ski> | (i'd rather have it not do that at all, tbh) |
| 21:24:13 | <tomsmeding> | keeping a nicklist on the irc side is little work, but I don't know how much of a refactor that would entail |
| 21:24:50 | <Shaeto> | hi, how to get UniversalTime from UTCTime ? |
| 21:25:01 | × | Joao[3] quits (~Joao003@190.108.99.67) (Quit: Bye!) |
| 21:25:21 | × | jargon quits (~jargon@154.sub-174-205-226.myvzw.com) (Read error: Connection reset by peer) |
| 21:26:09 | <tomsmeding> | Shaeto: what do you need UniversalTime for? Are you sure you don't want UTCTime? |
| 21:26:11 | <ski> | (as it is, when i want to respond to someone, over the bridge, i have to manually remove the ZWSP, after copying the nickname) |
| 21:26:44 | <Shaeto> | tomsmeding: i calculate the Sun coordinates, i need days + fractional part (time) :) |
| 21:27:03 | <tomsmeding> | you'll need a specialised library for that :p |
| 21:27:17 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 21:27:54 | <geekosaur> | tomsmeding, it's written in Go. I'd rather program in Python 😕 |
| 21:28:26 | <int-e> | Would ^O (mIRC, reset color) instead of ZWSP work better? I guess clients might filter that before checking for nickname matches. |
| 21:29:17 | <Shaeto> | i see what UniversalTime has instance of ParseTime mb i can parse some string to UniversalTime ? but i don't understand how |
| 21:29:38 | <tomsmeding> | that would be to parse a string representation of the date to a date value |
| 21:29:48 | <tomsmeding> | that doesn't help you for _computing_ that date value from a different unit |
| 21:29:59 | <sm> | maybe the https://wiki.haskell.org/Time cheatsheet helps a bit |
| 21:30:13 | <tomsmeding> | I know very little about this but looking at this you'll need some kind of database of time offsets https://www.nist.gov/pml/time-and-frequency-division/time-realization/leap-seconds |
| 21:30:21 | <tomsmeding> | if you're interested in this level of precision |
| 21:31:04 | <tomsmeding> | sm: that link confirms what I found: "Converting between UniversalTime and AbsoluteTime would require a database build upon astronomical observations. No such conversion utilities are provided. " :p |
| 21:31:57 | <Shaeto> | okay thank you think i can leave w/o leap second... will calculate fractional part of dat from seconds |
| 21:32:05 | <sm> | this is an excellent page. Haskell wiki doing the job yet again |
| 21:33:02 | <tomsmeding> | in fact, it would be helpful to have that text in the haddocks for UniversalTime |
| 21:33:21 | <tomsmeding> | the current text is... unhelpful if you don't already know these details |
| 21:33:47 | <sm> | (the diagram implies you can go UTCTime -> LocalTime -> UniversalTime though) |
| 21:33:52 | <ania123> | ski: hi |
| 21:34:13 | <sm> | ooh. "Updates? Ask EvanR on #haskell." |
| 21:34:34 | <tomsmeding> | that sounds wrong |
| 21:34:42 | × | cole-k quits (~cole@024-043-123-092.biz.spectrum.com) (Remote host closed the connection) |
| 21:35:03 | <sm> | the Longitude arrow should be red maybe |
| 21:35:17 | <tomsmeding> | no it should be black but you need more info than just that |
| 21:35:24 | <sm> | I see |
| 21:35:27 | <tomsmeding> | it's "Gain info" :p |
| 21:35:30 | <tomsmeding> | by magic |
| 21:35:42 | <sm> | yes, "magic happens" |
| 21:36:02 | <sm> | you consult the stars and intuit their meaning |
| 21:36:50 | <tomsmeding> | summarising my nist link: TAI is seconds since an epoch, UT1 is astronomical time, UTC is TAI + an integer number of seconds so that it's close to UT1 |
| 21:37:00 | <tomsmeding> | that integer number of seconds is the leap seconds between epoch and now |
| 21:37:17 | <tomsmeding> | so UTCTime ---(LeapSecondTable)--> TAI |
| 21:37:26 | <tomsmeding> | which is AbsoluteTime, which is correct in the diagram |
| 21:38:16 | <tomsmeding> | but I hink it would need to be AbsoluteTime(maybe UTCTime?) ---(AstronomicalObservationsTable)--> UT1=UniversalTime |
| 21:38:32 | <EvanR> | universal time is literally localtime with a longitude |
| 21:38:34 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 21:38:51 | <tomsmeding> | a ModJulianDate? |
| 21:39:07 | <tomsmeding> | is your "universal time" the UT1 from wikipedia / https://www.nist.gov/pml/time-and-frequency-division/time-realization/leap-seconds ? |
| 21:39:35 | <tomsmeding> | owait |
| 21:39:52 | <tomsmeding> | do you mean a longitude offset, as in an Earth rotation angle? |
| 21:39:55 | <geekosaur> | "does annybody really know what time it is?" |
| 21:40:05 | <tomsmeding> | close enough to be in time for meetings |
| 21:40:20 | <EvanR> | ok, it's not literally LocalTime + longitude |
| 21:41:08 | <tomsmeding> | there's got to be a database of offsets somewhere in the process of computing a UniversalTim |
| 21:41:10 | <tomsmeding> | e |
| 21:41:11 | <EvanR> | it's calendar day plus a fraction |
| 21:41:36 | <EvanR> | you can convert LocalTime to a UniversalTime by giving the longitude |
| 21:41:39 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 260 seconds) |
| 21:41:51 | <tomsmeding> | EvanR: is that UT1? |
| 21:41:57 | <tomsmeding> | or some other thing called "universal time" |
| 21:42:26 | <EvanR> | UniversalTime is a type in the time library whose documentation says "used to represent UT1" |
| 21:42:32 | <tomsmeding> | right |
| 21:42:43 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 21:42:53 | → | Joao[3] joins (~Joao003@190.108.99.67) |
| 21:42:57 | <tomsmeding> | but NIST claims that UT1 differs from UTC by on the order of 50ms |
| 21:43:08 | <tomsmeding> | (at least somewhere in 2023) |
| 21:43:16 | <EvanR> | I'm not surprised by that |
| 21:43:29 | <EvanR> | LocalTime and UniversalTime have nothing to do with UTC |
| 21:43:41 | <tomsmeding> | well LocalTime is UTC + time zone, right? |
| 21:43:53 | <tomsmeding> | UT1 has nothing to do with time zones as far as I can tell |
| 21:44:05 | <tomsmeding> | so I don't see how LocalTime gets you closer to UT1 than UTC does |
| 21:44:27 | <EvanR> | UTC is its own thing, you can express it using a LocalTime with the understanding you're talking about UTC's timezone |
| 21:44:37 | <tomsmeding> | I guess "LocalTime is UTC + geographical/geopolitical info" is more accurate |
| 21:44:41 | <EvanR> | the TimeZone type is basically a shift in time, not much of a time zone (series) |
| 21:45:04 | <EvanR> | LocalTime is very dumb it is just YY-MM-DD HH:MM:SS:etc |
| 21:45:14 | <EvanR> | with no other information so you can interpret it how you want |
| 21:45:29 | <EvanR> | all these types are like islands of ontology |
| 21:45:43 | <tomsmeding> | right |
| 21:46:11 | <tomsmeding> | I was interpreting "LocalTime" as "the time in my current timezone" which is inaccurate |
| 21:46:18 | <EvanR> | it could be! |
| 21:46:23 | <tomsmeding> | yeah true |
| 21:46:30 | <tomsmeding> | but that's not the relevant interpretation in this conversation |
| 21:46:37 | <EvanR> | I missed the beginning |
| 21:46:52 | <tomsmeding> | the beginning was someone asking "how do I convert from UTCTime to UniversalTime" |
| 21:47:08 | <Shaeto> | if forget about conversion .. how to parse UT1 from string ? |
| 21:47:32 | <tomsmeding> | EvanR: and then the diagram on haskell wiki suggests that you can suffice with a TimeZone and a Longitude, which I found doubtful |
| 21:47:49 | <EvanR> | let me try to find the function that that Longitude arrow is implying |
| 21:48:02 | <EvanR> | localTimeToUT1 :: Rational -> LocalTime -> UniversalTime |
| 21:48:26 | <geekosaur> | ain't nothing rational about that 😛 |
| 21:48:32 | <EvanR> | there's another straightforward function which renders UTCTime as a LocalTime in the UTC time zone |
| 21:48:45 | <EvanR> | so basically you have to pick the longitude |
| 21:48:54 | <EvanR> | "Get the UT1 time of a local time on a particular meridian (in degrees, positive is East)." |
| 21:49:28 | <tomsmeding> | _what_ hackage quick search is useless |
| 21:49:40 | <tomsmeding> | I was expecting to get all signatures involving UniversalTime by searching for "UniversalTime" |
| 21:49:42 | tomsmeding | sad |
| 21:50:06 | → | dcoutts joins (~duncan@cpc69402-oxfd27-2-0-cust903.4-3.cable.virginm.net) |
| 21:50:36 | × | sudden quits (~cat@user/sudden) (Ping timeout: 256 seconds) |
| 21:51:03 | → | sudden joins (~cat@user/sudden) |
| 21:51:34 | <EvanR> | this is more complicated than it needs to be, since you have the time in UTC, you just use zero as the Rational |
| 21:51:45 | <EvanR> | since the time you had was in UTC |
| 21:51:57 | <tomsmeding> | my understanding is that UT1 is a global standard and is not dependent on location :p |
| 21:51:58 | <EvanR> | though, you say, it differs by 50ms for some reason |
| 21:52:26 | <tomsmeding> | it differs by a small <1s fraction because astronomical stuff is not as digital as we'd like |
| 21:52:28 | <tomsmeding> | UT1 != UTC |
| 21:52:28 | <EvanR> | the universal time doesn't depend on location, but that function takes LocalTime and can't know where that time came frmo |
| 21:52:45 | <EvanR> | the Rational is telling the function where the LocalTime is reported at |
| 21:52:52 | <EvanR> | in this case, zero degrees east |
| 21:52:55 | <Joao[3]> | why are we talking about time zones in a channel about haskell |
| 21:53:18 | <EvanR> | because haskell somehow ended up with one of the most correctish time libraries unfortunately for programmers |
| 21:53:23 | × | agrosant quits (~agrosant@188.4.221.80.dsl.dyn.forthnet.gr) (Ping timeout: 264 seconds) |
| 21:53:30 | <Joao[3]> | :/ |
| 21:53:48 | <tomsmeding> | localTimeToUT1 sounds to me like if I start in Greenwich and move east very quickly (so that I can move around the world in a few minutes, say), UT1 will first decrease until I cross the time zone border into UTC+1 at which point it will jump ahead by an hour, after which it will decrease again, etc. |
| 21:53:50 | <EvanR> | you can identify subcomponents of the time package which other languages used as their basis, or have messed up |
| 21:53:56 | <tomsmeding> | that does _not_ sound proper :p |
| 21:54:57 | <EvanR> | tomsmeding, the argument pertains to the location you looked at the clock so it can get back to zero degrees, which is where the mod julian date is measured at |
| 21:55:03 | <tomsmeding> | in my few minutes of travelling around the world, UT1 should steadily increase by about the same number of minutes |
| 21:55:04 | → | komikat joins (~akshitkr@218.185.248.66) |
| 21:55:32 | <EvanR> | e.g. you have 90 degrees west and a local time, you can get the universal time now |
| 21:55:34 | <tomsmeding> | is that LocalTime argument to localTimeToUT1 supposed to be the geopolitical local time at that place on Earth? |
| 21:55:43 | <EvanR> | LocalTime is localtime yes |
| 21:55:47 | <EvanR> | just some time |
| 21:55:50 | <EvanR> | and date |
| 21:55:55 | <tomsmeding> | but then... my thought experiment? |
| 21:56:01 | <tomsmeding> | where does my reasoning go wrong |
| 21:56:36 | <EvanR> | you go west and your Rational decreases and your LocalTime increases, theoretically? |
| 21:56:57 | <EvanR> | we I got east and west backwards |
| 21:57:01 | <EvanR> | er |
| 21:57:07 | <tomsmeding> | yeah my point is not so much + vs - :p |
| 21:57:43 | <EvanR> | if you move across the globe at the same time, presumably your LocalTime changes as much as your longitude |
| 21:57:57 | <EvanR> | they should cancel out in localTimeToUT1 |
| 21:58:02 | <tomsmeding> | it's that in my thought experiment, according to that function, in my travel around the world UT1 would apparently move non-monotonically in a sawtooth wave, where the speed of change in each diagonal part is proportional to my speed of motion |
| 21:58:14 | <tomsmeding> | where UT1 surely does not depend on how fast I'm moving around the Earth?! |
| 21:58:15 | <EvanR> | it shouldn't move at all right |
| 21:58:22 | <EvanR> | since it's the same everywhere |
| 21:58:27 | × | komikat_ quits (~akshitkr@218.185.248.66) (Ping timeout: 272 seconds) |
| 21:58:27 | <tomsmeding> | yes |
| 21:58:31 | <EvanR> | it's the mod julian date |
| 21:58:35 | <EvanR> | in the definition |
| 21:58:42 | <tomsmeding> | but my Longitude is changing proportional to my speed of motion, and my LocalTime is changing... erratically |
| 21:59:02 | <tomsmeding> | their difference is erratic, surely not smooth and slow like UT1 is supposed to be |
| 21:59:35 | <EvanR> | yeah, so this function would only really work if you got LocalTime out of the reverse conversion |
| 21:59:45 | <EvanR> | ut1ToLocalTime :: Rational -> UniversalTime -> LocalTime |
| 21:59:58 | <EvanR> | the local time coming out of there has nothing to do with anything |
| 22:00:01 | <tomsmeding> | right |
| 22:00:08 | <EvanR> | sorted xD |
| 22:00:08 | <tomsmeding> | okay I'm with you there |
| 22:00:43 | <tomsmeding> | but then, like, ut1ToLocalTime gives a LocalTime that doesn't mean anything standard (though it does mean something well-defined -- UT1 + (some fraction) * longitude) |
| 22:00:53 | <EvanR> | anyway, since the Rational will equal zero, none of that matters |
| 22:01:02 | <tomsmeding> | and localTimeToUT1 needs a LocalTime according to that undocumented standard |
| 22:01:12 | <tomsmeding> | which you can only get if you had a UniversalTime in the first place |
| 22:01:20 | → | tromp joins (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 22:01:26 | <tomsmeding> | so you still can't compute a UniversalTime from anything else using the time library XD |
| 22:01:56 | <tomsmeding> | so, in my opinion, the LocalTime ---Longitude--> UniversalTime arrow is still wrong, or at best misleading |
| 22:02:14 | <tomsmeding> | yes, you can get something of type UniversalTime by putting in something of type LocalTime and a longitude value |
| 22:02:32 | <tomsmeding> | but that thing of type LocalTime is not anything that anyone has, normally |
| 22:02:46 | <tomsmeding> | it's not what you get by following the arrows from other places in that diagram |
| 22:02:53 | <EvanR> | if they have UTCTime it seems obvious what to do now |
| 22:03:00 | <tomsmeding> | no |
| 22:03:05 | × | noumenon quits (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 22:03:07 | <tomsmeding> | because then they'll miss that variable ~50ms offset |
| 22:03:20 | <tomsmeding> | and if you don't care about that offset, you should be using UTCTime, not UniversalTime |
| 22:03:29 | <tomsmeding> | the whole _point_ of UT1 is that it has that ~50ms offset |
| 22:04:03 | <EvanR> | make sure to adjust the answer by 50ms xD |
| 22:04:16 | <tomsmeding> | where that 50ms depends on the date and time lol |
| 22:04:26 | <tomsmeding> | so you need a table derived from astronomical observations |
| 22:04:33 | → | a51 joins (a51@gateway/vpn/protonvpn/a51) |
| 22:04:36 | <tomsmeding> | that NIST page I linked gives some entries |
| 22:05:01 | <EvanR> | I wonder if the need for UT1 was real |
| 22:05:05 | <tomsmeding> | I really appreciate that the 'time' library separates out all of these concepts |
| 22:05:19 | <tomsmeding> | I just think that some of the docs around UniversalTime can be significantly improved |
| 22:05:23 | <EvanR> | yes |
| 22:05:23 | <tomsmeding> | EvanR: it probably was not lol |
| 22:05:31 | <geekosaur> | astronomers use it |
| 22:05:35 | <tomsmeding> | for sure |
| 22:05:37 | <geekosaur> | I don't think anyone else cares |
| 22:05:39 | <Shaeto> | https://play.haskell.org/saved/oVpaI9xO |
| 22:05:40 | <tomsmeding> | it exists for a reason |
| 22:05:51 | <EvanR> | UniversalTime can be used to represent UT1, but the conversions to the other types need work it seems |
| 22:05:59 | <Shaeto> | why package doc says "The Modified Julian Day is a standard count of days, with zero being the day 1858-11-17." |
| 22:06:11 | <tomsmeding> | there _are_ no conversions to the other types without a regularly updated table of astronomical observations |
| 22:06:19 | <tomsmeding> | any conversion without such a table is misleading |
| 22:06:21 | <EvanR> | MJD is just JD shifted over to make that the zero day |
| 22:06:22 | <Shaeto> | but returns 60378 days for "today" |
| 22:06:31 | <EvanR> | it's an integer |
| 22:06:39 | <EvanR> | the count of days |
| 22:06:47 | <EvanR> | don't ask what a day is |
| 22:07:06 | <tomsmeding> | Shaeto: the Modified Julian Day for 1858-11-17 (why on earth that day, but whatever) is 0 |
| 22:07:13 | <tomsmeding> | 1858-11-18 is 1, etc. |
| 22:07:17 | <Joao[3]> | why??? |
| 22:07:17 | <Shaeto> | ahh sorry /365 :) |
| 22:07:18 | <geekosaur> | and really don't ask about days that went missing when various countries switched to Gregorian |
| 22:07:24 | <tomsmeding> | today is apparently 60378 |
| 22:07:26 | <EvanR> | lol |
| 22:07:42 | <EvanR> | those days didn't go missing in the JD, MJD system |
| 22:07:48 | <Joao[3]> | Shaeto: /365.2425 |
| 22:07:49 | <tomsmeding> | > 60378/365.2425 |
| 22:07:51 | <lambdabot> | 165.30934926795211 |
| 22:07:55 | <EvanR> | and the day of the week remained the same miraculously! |
| 22:07:58 | <tomsmeding> | 2024-165 |
| 22:07:59 | <geekosaur> | right but they matter if you try to convert from/to YMD |
| 22:08:01 | <tomsmeding> | > 2024-165 |
| 22:08:03 | <lambdabot> | 1859 |
| 22:08:06 | <tomsmeding> | checks out |
| 22:08:32 | <EvanR> | yes YMD means you're now doing calendrical gymnastics |
| 22:09:07 | <Joao[3]> | > 2024.1883-165.30934926795211 |
| 22:09:08 | <lambdabot> | 1858.878950732048 |
| 22:09:55 | × | Joao[3] quits (~Joao003@190.108.99.67) (Quit: Bye!) |
| 22:10:14 | <EvanR> | tomsmeding, at least, going from UniversalTime to a LocalTime at some longitude makes sense. Though it won't correspond to anyone's actual clock, not that LocalTime itself has any expectations |
| 22:10:46 | <EvanR> | what is shows on my microwave could be represented as LocalTime and means about as much |
| 22:10:52 | <EvanR> | no my microwave doesn't have internet |
| 22:11:11 | <geekosaur> | mine likes to run fast 😛 |
| 22:11:28 | × | michalz quits (~michalz@185.246.207.222) (Quit: ZNC 1.8.2 - https://znc.in) |
| 22:16:28 | <tomsmeding> | EvanR: Sure, UniversalTime + Longitude -> LocalTime makes some sense, but then that function (ut1ToLocalTime) should have a big disclaimer that this LocalTime is not what every programmer ever will expect when seeing the name "LocalTime" |
| 22:16:59 | <tomsmeding> | _especially_ because LocalTime does not contain any information describing what it's local to |
| 22:17:15 | <EvanR> | LocalTime does have the same structure as DateTime or whatever in many languages, where I have no idea what programmers think that means |
| 22:17:23 | <tomsmeding> | for sure |
| 22:17:28 | <tomsmeding> | again, I appreciate the separation |
| 22:17:39 | <EvanR> | except for a time zone code or something that usually doesn't help |
| 22:18:03 | <tomsmeding> | and I now see that there _is_ a note about UT1 in the haddocks for LocalTime, but the 'time' documentation could make more use of its good separation of definitions and explain what it's doing :p |
| 22:18:51 | <EvanR> | I had a hard time finding the UniversalTime docs |
| 22:18:58 | <EvanR> | such as they are |
| 22:18:59 | <tomsmeding> | @hackage time |
| 22:18:59 | <lambdabot> | https://hackage.haskell.org/package/time |
| 22:19:05 | <tomsmeding> | <s> UniversalTime <enter> |
| 22:19:19 | <EvanR> | yeah I had that but it's not in the top level module listings |
| 22:19:20 | <tomsmeding> | haddocks quick search does work that far :p |
| 22:19:28 | <tomsmeding> | try the 's' key on your keyboard |
| 22:19:41 | <tomsmeding> | or the 'Quick Jump' link on the page, does the same thing |
| 22:20:54 | <Shaeto> | my current dirty replacement for UT is fromIntegral (diffDays (utctDay now) (fromGregorian 2000 1 1)) + (utctDayTime now) / 86401.0 |
| 22:22:10 | <EvanR> | what dark incantation is that |
| 22:22:19 | <tomsmeding> | that would be since 2000-01-01, not since the actual UT1 epoch |
| 22:22:40 | <EvanR> | dividing by 86401 wtf xD |
| 22:22:52 | <tomsmeding> | that's just "number of seconds, as measured by UTC including leap second magic, since 2000-01-01 00:00:00" |
| 22:22:58 | <tomsmeding> | and also yes where does that 1 come from lol |
| 22:23:12 | <tomsmeding> | > 24*60*60 |
| 22:23:13 | <lambdabot> | 86400 |
| 22:23:16 | <Shaeto> | because of utctDayTime doc :) |
| 22:23:25 | <EvanR> | no... |
| 22:23:34 | <tomsmeding> | > Note that if a day has a leap second added to it, it will have 86401 seconds. |
| 22:23:39 | <tomsmeding> | if not, it will have 86400 seconds |
| 22:23:55 | <tomsmeding> | whether it has depends on some table you'll have to load from somewhere, it's unpredictable |
| 22:24:01 | <tomsmeding> | this is the whole debacle we've been talking about :p |
| 22:24:26 | <tomsmeding> | dividing by 86400 will give you something that's very close to UT1 |
| 22:24:37 | <tomsmeding> | but not quite exactly the same, it will differ by up to 0.9 seconds |
| 22:24:42 | <tomsmeding> | in the worst case |
| 22:24:51 | × | takuan quits (~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection) |
| 22:24:58 | <EvanR> | 86401 would assume there's a leap second every day |
| 22:25:03 | <EvanR> | which there isn't |
| 22:25:26 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Ping timeout: 252 seconds) |
| 22:25:31 | <tomsmeding> | you don't know whether I make a leap for a second every day |
| 22:31:08 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 22:31:33 | × | tromp quits (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 22:52:26 | × | wootehfoot quits (~wootehfoo@user/wootehfoot) (Read error: Connection reset by peer) |
| 22:56:33 | → | pavonia joins (~user@user/siracusa) |
| 22:58:25 | × | Shaeto quits (~Shaeto@94.25.234.62) (Quit: WeeChat 4.2.1) |
| 23:04:19 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 23:04:47 | → | rainbyte joins (~rainbyte@186.22.19.215) |
| 23:07:41 | × | kimiamania quits (~7da15a40@user/kimiamania) (Quit: PegeLinux) |
| 23:08:11 | × | destituion quits (~destituio@2001:4644:c37:0:6086:64f4:a213:b80d) (Ping timeout: 256 seconds) |
| 23:09:02 | → | kimiamania joins (~7da15a40@user/kimiamania) |
| 23:22:30 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 23:23:19 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:25:19 | → | destituion joins (~destituio@2a02:2121:650:17b6:7013:905e:d9bb:b716) |
| 23:34:49 | × | acidjnk_new3 quits (~acidjnk@p200300d6e737e7747555095b6f843b59.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 23:35:50 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 23:37:45 | × | ski quits (~ski@ext-1-033.eduroam.chalmers.se) (Remote host closed the connection) |
| 23:37:52 | → | ski joins (~ski@ext-1-033.eduroam.chalmers.se) |
| 23:38:09 | → | agrosant joins (~agrosant@77.49.41.227.dsl.dyn.forthnet.gr) |
| 23:38:15 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:46:44 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 23:47:30 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:48:02 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 23:48:49 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:50:03 | × | emmanuelux quits (~emmanuelu@user/emmanuelux) (Read error: Connection reset by peer) |
| 23:50:36 | → | emmanuelux joins (~emmanuelu@user/emmanuelux) |
| 23:57:09 | → | glguy joins (g@libera/staff/glguy) |
| 23:57:20 | × | target_i quits (~target_i@user/target-i/x-6023099) (Quit: leaving) |
All times are in UTC on 2024-03-09.