00:05:06 -!- oerjan has joined.
00:07:03 -!- nchambers has joined.
00:11:22 -!- tromp has quit (Remote host closed the connection).
00:31:17 -!- nfd9001 has joined.
00:31:23 -!- Essadon has quit (Quit: Qutting).
00:49:07 <oerjan> It's apparently the neighbor's turn to have a cold. :(
00:56:14 -!- nfd9001 has quit (Ping timeout: 268 seconds).
01:03:23 -!- tromp has joined.
02:12:21 <zzo38> Do you know that I am making a implementation of Z-machine in Glulx?
02:13:33 <zzo38> So far I got everything in ZIPTEST working up to and including the "test of LOC" (which actually uses IN? and not LOC)
02:31:42 -!- nchambers has changed nick to uplime.
02:33:45 -!- MDude has joined.
02:58:06 <lambdabot> ENVA 050250Z 29008KT 9999 FEW007 SCT010 BKN025 06/05 Q1021 RMK WIND 670FT 28015KT
03:32:15 -!- FreeFull has quit.
03:36:27 <imode> uncle died today. what do you all use to keep programming through times like that.
03:48:23 -!- Lord_of_Life has quit (Ping timeout: 245 seconds).
03:50:16 <oerjan> My condolences. Alas, I'm the worst person to ask.
03:53:26 -!- Lord_of_Life has joined.
04:03:41 <zzo38> That is too bad, but I have not needed anything, in order to do so
04:04:38 -!- moei has joined.
04:04:53 -!- ATMunn has quit (Read error: Connection reset by peer).
04:04:53 -!- Bowserinator has quit (Read error: Connection reset by peer).
04:04:53 -!- moony has quit (Read error: Connection reset by peer).
05:00:32 * oerjan simplifies ais523's three bracket proof
05:02:04 -!- ATMunn has joined.
05:02:26 -!- Bowserinator has joined.
05:02:31 <zzo38> I thought of some idea to combine Go with Scrabble.
05:04:06 -!- moony has joined.
06:18:36 -!- xkapastel has quit (Quit: Connection closed for inactivity).
06:33:12 <esowiki> [[Talk:Nope.]] https://esolangs.org/w/index.php?diff=58926&oldid=58923 * Salpynx * (+2980) using Nope. interpreter for arbitrary output
06:40:00 -!- MDead has joined.
06:41:52 <esowiki> [[Talk:Nope.]] M https://esolangs.org/w/index.php?diff=58927&oldid=58926 * Salpynx * (+80) /* Hello, World! */
06:42:16 -!- MDude has quit (Ping timeout: 268 seconds).
06:42:19 -!- MDead has changed nick to MDude.
06:53:22 <esowiki> [[Brainfuck]] https://esolangs.org/w/index.php?diff=58928&oldid=58897 * Oerjan * (+414) /* Computational class */ Remove claim that was never made remotely rigorous, and add Ais523's new result from CS.SE
06:54:52 <esowiki> [[Brainfuck]] M https://esolangs.org/w/index.php?diff=58929&oldid=58928 * Oerjan * (+0) /* Computational class */ 'pparently it's lower case
07:10:58 <esowiki> [[Funciton]] https://esolangs.org/w/index.php?diff=58930&oldid=51638 * Qpliu * (+150)
07:24:46 <esowiki> [[Funciton]] https://esolangs.org/w/index.php?diff=58931&oldid=58930 * Qpliu * (+103) /* External resources */
07:25:26 <esowiki> [[Special:Log/newusers]] create * FizzyApple12 * New user account
07:31:10 <esowiki> [[Talk:Funciton]] https://esolangs.org/w/index.php?diff=58932&oldid=47233 * Qpliu * (+713) /* Rotation invariant? */
07:44:35 -!- spiegelau has joined.
07:48:34 -!- oerjan has quit (Quit: Nite).
07:49:49 -!- nfd9001 has joined.
08:15:18 -!- tromp has quit (Remote host closed the connection).
08:15:32 -!- tromp has joined.
08:35:07 -!- uplime has quit (Ping timeout: 240 seconds).
08:59:43 -!- AnotherTest has joined.
09:03:30 -!- hakatashi has quit (Remote host closed the connection).
09:03:52 -!- hakatashi has joined.
09:51:13 -!- imode has quit (Ping timeout: 258 seconds).
09:52:16 -!- tromp has quit (Remote host closed the connection).
10:02:37 -!- tromp has joined.
10:22:49 <esowiki> [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=58933&oldid=58919 * FizzyApple12 * (+342) /* Introductions */
10:23:27 <esowiki> [[Laser]] N https://esolangs.org/w/index.php?oldid=58934 * FizzyApple12 * (+3184) Laser is a 2D programming language built by FizzyApple12 (David Roeder) based on lasers, color, brightness and direction.
10:24:55 <esowiki> [[Laser]] https://esolangs.org/w/index.php?diff=58935&oldid=58934 * FizzyApple12 * (+19) /* Hello World */
10:33:51 <esowiki> [[Laser]] M https://esolangs.org/w/index.php?diff=58936&oldid=58935 * FizzyApple12 * (+2) /* Hello World */
10:38:00 <esowiki> [[Laser]] https://esolangs.org/w/index.php?diff=58937&oldid=58936 * FizzyApple12 * (+18) fixed bad formatting
10:42:08 <esowiki> [[Laser]] https://esolangs.org/w/index.php?diff=58938&oldid=58937 * FizzyApple12 * (+13) fixed bad formatting
10:43:12 <esowiki> [[Laser]] https://esolangs.org/w/index.php?diff=58939&oldid=58938 * FizzyApple12 * (-9) fixed bad formatting
10:45:43 <esowiki> [[Laser]] M https://esolangs.org/w/index.php?diff=58940&oldid=58939 * FizzyApple12 * (+28) fix even more bad formatting
10:56:54 -!- copumpkin[m] has quit (Remote host closed the connection).
11:06:53 -!- copumpkin[m] has joined.
12:46:42 -!- AnotherTest has quit (Ping timeout: 252 seconds).
12:53:32 -!- FreeFull has joined.
13:22:54 -!- xkapastel has joined.
13:36:57 -!- arseniiv has joined.
13:37:31 -!- sebbu has quit (Quit: Quitte).
13:43:59 <esowiki> [[Laser]] M https://esolangs.org/w/index.php?diff=58941&oldid=58940 * FizzyApple12 * (-42)
13:54:06 -!- sebbu has joined.
13:55:03 -!- spiegelau has quit (Ping timeout: 245 seconds).
13:55:47 -!- sebbu has quit (Remote host closed the connection).
13:57:18 -!- sebbu has joined.
14:04:40 -!- AnotherTest has joined.
14:19:15 -!- AnotherTest has quit (Ping timeout: 264 seconds).
15:08:54 <esowiki> [[Laser]] https://esolangs.org/w/index.php?diff=58942&oldid=58941 * FizzyApple12 * (+4)
15:24:47 <esowiki> [[Laser]] M https://esolangs.org/w/index.php?diff=58943&oldid=58942 * FizzyApple12 * (-5)
15:48:17 -!- Lord_of_Life_ has joined.
15:48:42 <esowiki> [[Special:Log/newusers]] create * Niceapi * New user account
15:51:06 -!- Lord_of_Life has quit (Ping timeout: 268 seconds).
15:51:13 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
15:54:50 <esowiki> [[User:FizzyApple12]] N https://esolangs.org/w/index.php?oldid=58944 * FizzyApple12 * (+229) Created page with "FizzyApple12 (David Roeder) is a small programmer that does a lot of work in JavaScript, Python, and C# == His Work == === Website === My website is [http://www.fizzyapple..."
16:04:05 <arseniiv> how do I prove that Void (a type with no constructors, the zero type) is isomorphic to forall a. a?
16:05:23 <arseniiv> it’s easy to write two functions Void → (forall a. a) and (forall a. a) → Void, but I can’t prove their two compositions equal to id
16:06:22 <arseniiv> the question in this case is what (case x of {}) is equal to, or how can I prove the isomorphism in some other, not equational way
16:07:45 <arseniiv> as far as it goes, we should be unable to derive anything about the value of (case x of {}), as there are no matchers in there, and so no implications of form “x = … => case x of {…} = …”
16:08:42 <arseniiv> and there are, if we are talking about a sound theory, no other ways to derive a formula of the form “case x of {…} = …”
16:09:01 <arseniiv> if I understand it all correctly, that is
16:13:10 -!- AnotherTest has joined.
16:21:57 <esowiki> [[Laser]] https://esolangs.org/w/index.php?diff=58945&oldid=58943 * FizzyApple12 * (+66)
16:22:16 <esowiki> [[Laser]] https://esolangs.org/w/index.php?diff=58946&oldid=58945 * FizzyApple12 * (+0) /* Truth Machine */
16:30:55 -!- tromp has quit (Remote host closed the connection).
16:59:07 -!- Sgeo__ has joined.
17:02:24 -!- Sgeo_ has quit (Ping timeout: 250 seconds).
17:12:00 -!- uplime has joined.
17:43:16 -!- tromp has joined.
17:54:55 -!- imode has joined.
19:05:19 <esowiki> [[User:Cortex/draft]] https://esolangs.org/w/index.php?diff=58947&oldid=58925 * Cortex * (+19)
19:09:36 -!- b_jonas has joined.
19:15:32 <lambdabot> LOWI 051850Z VRB02KT 6000 -SNRA FEW003 BKN012 01/00 Q1025 R08/19//95 TEMPO 27007KT 4000 SNRA
19:16:44 <fungot> Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc* iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp ukparl youtube
19:17:02 <fungot> Selected style: discworld (a subset of Terry Pratchett's Discworld books)
19:17:06 <int-e> fungot: Rincewind?
19:17:07 <fungot> int-e: there was the sound of his hammer.
19:18:34 <fungot> int-e: " yes, sir." vimes lowered the ape, who wisely didn't make an issue of it because a man angry enough to lift fnord of orangutan without noticing is a man of high reputation!' the archchancellor went on.
19:18:51 <int-e> Ah, we have a winner :)
19:21:03 <int-e> I forgot what the problem with this style was... a tendency to produce literal quotes rather than remixing, maybe?
19:22:15 <fungot> int-e: he gripped the guitar's neck and flung it inexpertly. he was the younger son, and family tradition sent youngest sons into some church or other," she said,
19:22:45 <int-e> fungot quota exceeded :/
20:06:53 <fizzie> fungot: You're so stingy.
20:06:53 <fungot> fizzie: carrot patted him fnord on the wood near the driver, was a squat little house, with a grunt of effort.
20:09:00 * int-e fungots with exceeding fungot
20:09:00 <fungot> int-e: " why'd you want to face the other auditors. with considerable effort, managed to light the lamps and the squeaky rubber hippo. now he could see right to the sheer drop.
20:14:14 -!- ais523 has joined.
20:14:49 -!- uplime has quit (Quit: WeeChat 2.2).
20:14:53 <ais523> <arseniiv> as far as it goes, we should be unable to derive anything about the value of (case x of {}) ← no, you have that backwards, we are able to derive /anything/ about the value of (case x of {})
20:15:25 <ais523> think of it this way: how would you prove that (case x of {true = 4; false = 4}) is 4?
20:16:54 <HackEso> cat: cat: No such file or directory
20:18:20 <HackEso> A canary is a small bright yellow chicken that dwells in deep caves. Unlike bats, canaries are oriented right way up, unless they're pining for the fjords.
20:18:44 <HackEso> oerjän boil̈y oerjän FireFl̈y FireFl̈y
20:19:49 <int-e> "Errol had started eating again. He'd eaten most of the table, the grate, the coal scuttle, several lamps and the squeaky rubber hippo."
20:28:46 -!- AnotherTest has quit (Quit: ZNC - http://znc.in).
20:28:57 -!- AnotherTest has joined.
20:42:21 -!- AnotherTest has quit (Ping timeout: 252 seconds).
20:52:37 -!- uplime has joined.
21:02:48 -!- S_Gautam has joined.
21:02:54 <Taneb> I am back from Italy
21:04:15 <lambdabot> EGLL 052050Z AUTO 28005KT 9999 OVC027 06/02 Q1038
21:05:32 <lambdabot> LIRA 052050Z 04005KT 9999 SCT050 06/M00 Q1019
21:09:37 <Taneb> b_jonas: apparently not
21:10:52 -!- moony has quit (Quit: Bye!).
21:10:52 -!- ATMunn has quit (Quit: lol rip).
21:10:52 -!- Bowserinator has quit (Quit: Blame iczero something happened).
21:11:28 -!- ATMunn has joined.
21:11:45 -!- ais523 has quit (Remote host closed the connection).
21:11:48 -!- Bowserinator has joined.
21:12:57 -!- ais523 has joined.
21:15:46 -!- moony has joined.
21:16:06 -!- uplime has quit (Quit: WeeChat 2.2).
21:17:00 -!- tromp has quit (Remote host closed the connection).
21:17:17 -!- tromp has joined.
21:31:27 -!- moony has quit (Quit: Bye!).
21:31:27 -!- Bowserinator has quit (Quit: Blame iczero something happened).
21:31:27 -!- ATMunn has quit (Quit: lol rip).
21:31:48 -!- ATMunn has joined.
21:34:13 -!- Bowserinator has joined.
21:35:07 <esowiki> [[Hexlr7]] https://esolangs.org/w/index.php?diff=58948&oldid=58756 * Cortex * (-80)
21:35:58 -!- tromp has quit (Remote host closed the connection).
21:36:07 -!- moony has joined.
21:41:12 -!- tromp has joined.
21:41:46 -!- BrightBlackHole has joined.
21:46:41 -!- BrightBlackHole has quit (Ping timeout: 256 seconds).
22:04:04 <Luciole> https://twitter.com/handleym99/status/1081617351328460800 I feel like this tweet is #esoteric-relevant
22:09:41 <int-e> Luciole: so I'm supposed to remove all leap year handling from my code? :P
22:10:20 <Luciole> well, sure. it's a niche edgecase anyway, you're better off not supporting leap years. don't want to feature-bloat your program
22:10:24 <Luciole> just add it back every fourth year
22:11:12 <zzo38> I disagree, you will need leap year support if you are doing date calculations (although you might not need to implement it yourself; it might be part of the standard library). However, if you do not need to convert dates in this way, then you do not need to add special support for leap years either.
22:13:26 <int-e> @google 100 days ago
22:13:27 <lambdabot> https://www.convertunits.com/dates/daysfromnow/-100
22:14:21 <int-e> (Google actually comes back with a date for me.)
22:15:12 <b_jonas> also remove all lines about recognizing hardware errors like a faulty disk. who needs those?
22:18:13 <zzo38> It depend on the program, I think.
22:23:09 <ais523> handling faulty disks should be the responsibility of the language/runtime, not every program that uses disks
22:24:04 <ais523> although unless the language has some sort of unified UI, the runtime may want to tell the program "that wasn't possible, ask the user to save it elsewhere"
22:24:11 <b_jonas> so you remove those lines from the kernel drivers if they haven't been used in a year
22:24:16 <ais523> (languages probably /should/ have a common UI for all programs, but in practice they don't)
22:25:20 <int-e> Luciole: I'm also reminded of, I believe, the .kkrieger game, where in the competition version, the "up" key didn't work in the menu; it turns out that they had a tool to dynamically detect dead code and they used that to squeeze it down to 96k; and in none of the test playthroughs did they ever use the "up" key in the menu.
22:26:00 <b_jonas> it's funny when en.wikipedia has two articles about two people mentioned in the Bible who were probably the same but we're not entirely sure, but hu.wikipedia only has one article, so it's hard to navigate from en.wikipedia to the relevant article on hu.wikipedia because the language links must map one to one
22:26:16 <int-e> (I remember the story better than what the actual game was, and unfortunately I have not found the story itself in my brief search just now.)
22:27:22 <zzo38> Handling faulty disks should be the responsibility of the driver in the operating system, I should think. It can simply tell the program it is error, and the program need not tell the difference from different kind of errors.
22:28:12 <zzo38> b_jonas: Can you add a redirection page to fix that? Will languages work with redirection pages?
22:28:16 <b_jonas> it can also happen backwards, or with two people who are definitely the same but a distinction is made about which name is the patron of a certain Catholic church or parish: that mostly happens with Jesus Christ and Virgin Mary
22:28:49 <b_jonas> zzo38: you can add a redirection page, but not working language links that way I think
22:29:10 <Luciole> int-e: yepyep, the article on that tool (that they wrote to compress it) is really interesting (but I suspect you might've read it, given I think that particular tidbit is from that article)
22:29:34 <Luciole> https://fgiesen.wordpress.com/2012/04/08/metaprogramming-for-madmen/ <- that one
22:29:41 <Luciole> (also the rest of ryg's blog, really)
22:30:15 <b_jonas> there's a similar phenomenon that happens with language links across commons and two wikipedias, because language links must be transitive too:
22:31:08 <b_jonas> often one wikipedia has both an article and a category about something, another wikipedia only has an article, and commons only has a category, and in that case you can't go in an easy way between commons and the second wikipedia
22:31:21 <b_jonas> sometimes this is fixed by ordinary links in the description text of course
22:31:57 <b_jonas> this one actually should be automated in software, because wikidata does collect the relation of an article being the main article of a category,
22:32:26 <b_jonas> so perhaps the mediawiki software could be patched to show the relevant interwiki links automatically in that case
22:34:44 <b_jonas> ais523: sometimes it can happen in user programs too, if it handles fails writes and writes have never failed in that program in the last year. writes could fail not only for a disk hardware failure, but also because of filesystem full, permission denied, no network access to network file system, media removed from driver, etc, but with the use case of some programs these just don't come up
22:37:12 <ais523> some programs, I run less than once per year
22:37:14 <int-e> Luciole: wow, thanks.
22:37:17 <b_jonas> this is why we have a /dev/full for easy testing by the way
22:37:28 <int-e> Luciole: Yes, I've read that before, but it's nice to see it again :)
22:37:48 <arseniiv> ais523> think of it this way: how would you prove that (case x of {true = 4; false = 4}) is 4? => by case analysis: x = true => (case …) = 4, x = false => (case …) = 4, so (case …) = 4 unconditionally. Hm so if we have an empty conjunction of these… hm, no, I don’t exactly follow
22:38:31 * Luciole is now reading https://fgiesen.wordpress.com/2018/12/10/rate-distortion-optimization/
22:38:49 <ais523> arseniiv: the point is that you get a return value of 4 in every branch
22:39:03 <ais523> case x of {} also gives a return value of 4 in every branch
22:39:54 <ais523> you can use a similar argument to prove /anything/ about the return value of "case x of {}" (it's not surprising you can do this, as the code can never run, so this is just a variant of "from a contradiction, anything follows")
22:41:51 <arseniiv> ais523: ah, thanks, now it’s clearer!
22:42:51 <arseniiv> so, then that isomorphism is sealed and I can sleep at ease :D
22:46:02 <b_jonas> https://twitter.com/gro_tsen/status/1081614752231632902 is esoteric-related too.
22:50:14 -!- arseniiv has quit (Ping timeout: 246 seconds).
23:00:22 -!- b_jonas has quit (Quit: leaving).
23:05:35 -!- nfd9001 has quit (Ping timeout: 250 seconds).
23:14:23 <esowiki> [[Bitch]] N https://esolangs.org/w/index.php?oldid=58949 * Helen * (+11472) Created a page for bitch
23:17:01 <esowiki> [[Bitch]] M https://esolangs.org/w/index.php?diff=58950&oldid=58949 * Helen * (+22) Fixed a sentence
23:25:23 <esowiki> [[Bitch]] M https://esolangs.org/w/index.php?diff=58951&oldid=58950 * Helen * (+92) Added a mention to Bitwise, a language like BITCHWISE
23:27:13 <esowiki> [[Bitch]] M https://esolangs.org/w/index.php?diff=58952&oldid=58951 * Helen * (+67) Added categories
23:31:32 <esowiki> [[Bitch]] M https://esolangs.org/w/index.php?diff=58953&oldid=58952 * Helen * (-92) Removed mention to Bitwise
23:32:55 <esowiki> [[Bitch]] M https://esolangs.org/w/index.php?diff=58954&oldid=58953 * Helen * (+4) Fixed lack of newline
23:34:19 <esowiki> [[User:Helen]] https://esolangs.org/w/index.php?diff=58955&oldid=57964 * Helen * (+146)
23:35:04 <esowiki> [[What!?]] M https://esolangs.org/w/index.php?diff=58956&oldid=57970 * Helen * (+42) Added category tags
23:35:22 <esowiki> [[Bitch]] M https://esolangs.org/w/index.php?diff=58957&oldid=58954 * Helen * (+0) Fixed wrong 2018 tag (2018->2019)
23:35:35 -!- oerjan has joined.
23:36:16 <esowiki> [[Category:2019]] N https://esolangs.org/w/index.php?oldid=58958 * Helen * (+12) Created page with "{{yearcat }}"
23:37:46 <esowiki> [[Language list]] M https://esolangs.org/w/index.php?diff=58959&oldid=58924 * Helen * (+12) Added bitch
23:40:58 -!- oerjan has quit.
23:41:57 -!- oerjan has joined.
23:55:36 <oerjan> ais523: I found how to remove the middle brackets, see comment
23:59:59 <ais523> I haven't fully got my head around it yet