00:06:08 -!- tromp has quit (Remote host closed the connection).
00:08:05 -!- Phantom_Hoover has quit (Remote host closed the connection).
00:23:05 -!- AnotherTest has quit (Ping timeout: 246 seconds).
00:40:06 -!- oerjan has joined.
00:40:21 -!- Lord_of_Life_ has joined.
00:42:23 -!- tromp has joined.
00:42:52 -!- Lord_of_Life has quit (Ping timeout: 250 seconds).
00:42:53 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
01:10:51 <esowiki> [[Inflection]] https://esolangs.org/w/index.php?diff=60806&oldid=44480 * Prof Apex * (+262)
01:49:05 <esowiki> [[AlphaBeta]] https://esolangs.org/w/index.php?diff=60807&oldid=54154 * Illuminatu * (+306)
01:50:20 -!- nikgre has joined.
01:51:29 <esowiki> [[AlphaBeta]] https://esolangs.org/w/index.php?diff=60808&oldid=60807 * Illuminatu * (+12)
01:58:16 -!- nikgre has quit (Quit: Leaving).
02:08:31 <zzo38> Does any C compiler have "goto case" and "goto default"?
02:13:29 <fizzie> Not as far as I know, though some of the nearby languages (C#, D) do.
02:16:29 <oerjan> . o O ( What about Db )
02:18:07 <oerjan> ah https://www.codeproject.com/Articles/13639/Db-The-Future-Is-Coming
02:18:51 <fizzie> I'm guessing it's more common in languages with no implicit fall-through.
03:06:17 -!- Essadon has quit (Quit: Qutting).
03:20:22 <zzo38> Do you have any kind of advice of implementing NNTP server with SQLite?
03:32:40 <zzo38> If they want us to defend their church from an attack (after they helped us to get underground through their passage) but now we are too tired to help them and should sleep instead, then what are we going to do? Hire someone else to help them? (This is the GURPS game.)
03:38:31 <zzo38> Do you know if FreeDOS can load overlong COM files?
03:47:09 -!- FreeFull has quit.
04:02:14 -!- oerjan has quit (Quit: Nite).
04:10:32 -!- quintopia has quit (Ping timeout: 272 seconds).
04:10:40 -!- quintopia has joined.
08:14:04 -!- tromp has quit (Remote host closed the connection).
08:14:18 -!- tromp has joined.
09:19:50 -!- arseniiv has joined.
09:28:16 -!- tromp has quit (Remote host closed the connection).
09:34:00 -!- tromp has joined.
10:13:48 -!- aloril_ has quit (Remote host closed the connection).
10:23:28 -!- aloril has joined.
11:16:42 -!- rodgort has quit (*.net *.split).
11:16:42 -!- Melvar has quit (*.net *.split).
11:16:42 -!- HackEso has quit (*.net *.split).
11:16:42 -!- oren has quit (*.net *.split).
11:16:42 -!- lifthrasiir_ has quit (*.net *.split).
11:16:43 -!- APic has quit (*.net *.split).
11:17:11 -!- lifthrasiir has joined.
11:17:11 -!- rodgort has joined.
11:17:14 -!- oren has joined.
11:17:20 -!- Melvar has joined.
11:19:02 -!- HackEso has joined.
11:19:58 -!- vertrex has quit (Ping timeout: 255 seconds).
11:20:25 -!- sftp has quit (Ping timeout: 255 seconds).
11:21:36 -!- sftp has joined.
11:21:48 -!- vertrex has joined.
11:21:48 -!- vertrex has quit (Changing host).
11:21:48 -!- vertrex has joined.
11:22:16 -!- APic has joined.
11:35:37 -!- AnotherTest has joined.
12:16:09 <int-e> so quiet on the wiki - the A-team must be out of town.
12:19:35 <fungot> int-e: curl is not the true finish.
12:19:59 <int-e> fungot: you can do better than that
12:23:37 <fizzie> fungot: Giving them the cold shoulder, eh?
12:23:38 <fungot> fizzie: i.e. a list of words with him, regardless of whether scheme48 is being proper, it's important to know where it is
12:23:46 <fizzie> (Is that even a correct idiom?)
12:24:28 <lambdabot> *** "cold shoulder" wn "WordNet (r) 3.0 (2006)"
12:24:29 <lambdabot> n 1: a refusal to recognize someone you know; "the snub was
12:24:31 <lambdabot> clearly intentional" [syn: {snub}, {cut}, {cold shoulder}]
12:25:03 <int-e> Or maybe it's "show" rather than "give"? I don't know.
12:25:50 <fizzie> "Even the best A&R—artist and repertoire—staff in the world couldn't save you if radio gave you the cold shoulder."
12:26:04 <fizzie> (From the Google snippet of an OED entry.)
12:26:26 <int-e> Yeah I think the "show" is inspired by the parallel idiom in German.
12:27:23 <int-e> Which is "jemandem die kalte Schulter zeigen" - the verb is "zeigen": to show; to demonstrate; to point out)
12:30:22 <fizzie> Looks like it's also a verb.
12:30:23 <fizzie> `` wn "cold shoulder" -over | sed -e '1,/verb/d;/^1/p;d'
12:30:24 <HackEso> 1. slight, cold-shoulder -- (pay no attention to, disrespect; "She cold-shouldered her ex-fiance")
12:31:20 <fizzie> (Guess almost any noun can be verbed though.)
12:33:27 <int-e> verbificationizing is lots of fun.
12:43:08 -!- Lord_of_Life_ has joined.
12:43:41 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
12:45:31 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
13:12:39 -!- Essadon has joined.
14:40:49 -!- FreeFull has joined.
15:52:09 -!- oerjan has joined.
15:57:36 <oerjan> "This expression and its German equivalent are mistranslations of dederunt umerum recedentem from the Book of Nehemiah 9.29 from the Vulgate Bible, which actually means "stubbornly they turned their backs on you", which comes from the Septuagint Bible's equivalent ἔδωκαν (édōkan) νῶτον ἀπειθοῦντα. Latin umerus means both "shoulder" and "back"."
16:20:30 -!- Phantom_Hoover has joined.
16:20:31 -!- Phantom_Hoover has quit (Changing host).
16:20:31 -!- Phantom_Hoover has joined.
16:20:52 <kmc> good morning y'all
16:49:46 <arseniiv> hm how do you think should “hot shoulder” mean misrecognition of people you don’t actually know?
17:03:43 <kmc> oh, another disadvantage of using sound cards as modems for ham radio: sometimes people end up transmitting their Windows alert sounds by accident :P
17:07:58 <zzo38> Other way is to not use Windows, or if you are using Windows to disable the alert sounds, or maybe you have surround sound you can use some channel for different purposes? There are other cases too where such a thing might be wanted.
17:09:12 <oerjan> zzo38: none of those ways help with accidents happening because some people are too dumb to know about them
17:12:56 <b_jonas> kmc: is that like when people give a presentation in a conference and there are popups prompting for software updates and friends who have come online on skype over the slides?
17:12:59 <zzo38> Yes, that is true probably
17:14:16 <esowiki> [[User:Sentry]] N https://esolangs.org/w/index.php?oldid=60809 * Sentry * (+63) Created page with "a young aspiring programmer and student, open source enthusiast"
17:14:51 <oerjan> `le/rn Aspiring is like perspiring, but more hopeful.
17:14:52 <HackEso> Usage: `le/[/]rn <key>//<wisdom>
17:14:59 <oerjan> `learn Aspiring is like perspiring, but more hopeful.
17:15:01 <HackEso> Learned 'aspiring': Aspiring is like perspiring, but more hopeful.
17:28:00 <kmc> b_jonas: yes
17:31:20 <kmc> zzo38: yeah, the best solution is to use a dedicated sound card for the radio. you can buy USB sound interfaces like RIGblaster and SignaLink that are made for this, they generally have better quality, better filtering and such, and some of them can control your radio too, so you can set the frequency etc from software
17:31:38 <kmc> and some of the newer radios have a USB port built in so that you get both audio and control with a single USB cable
17:31:46 <kmc> but yeah it still relies on the operator configuring their software correctly
18:02:21 -!- oerjan has quit (Quit: Later).
18:03:47 <fizzie> `learn The password of the month is invalid.
18:03:49 <HackEso> Relearned 'password': The password of the month is invalid.
18:03:51 <fizzie> (Feel free to change, it just dawned on me we'll soon miss having one for March.)
18:06:38 <fizzie> We did an escape room as a team thing the other day, and they did the "password IS invalid" thing.
18:09:19 <kmc> I know someone who chose their wifi password as "alllowercasenospaces"
18:12:32 <int-e> followtheinstructionstotheletter
18:16:05 <b_jonas> it turns out that French has a word with "à" in it other than "à", "là", and prefixed versions derived from "là". it's "en-deçà" and I don't think I've seen it until today.
18:23:48 <FireFly> kmc: I've seen that but worse, lemme see if I can find a pic..
18:24:03 -!- Lymia has quit (Remote host closed the connection).
18:27:51 <FireFly> Hmm, no picture, but something along the lines of "the wifi password is designed to mess with the use-mention distinction"
18:28:20 <FireFly> with the password being literally the bit after 'is', with spaces and all-lowercase
18:28:21 <kmc> yeah I know people who would set that kind of password
18:29:21 -!- Lymia has joined.
18:29:50 <j4cbo> the password is “contained in greengrocers’ quotes”
18:32:47 <zzo38> The book Godel,Escher,Bach defines the TNT (Typographical Number Theory), and you can define the rules to make a theorem. But, then maybe you want to define if a sentence of TNT (open formulas don't count) is true? I thought maybe: [1] If X is a theorem then X is true. [2] If X and Y are true and are assumed as axioms then Z would be a theorem, then Z is true. [3] If X starts with a universal quantifier and all sentences formed by removing the
18:34:22 <zzo38> What do you think?
18:57:11 <esowiki> [[Bitter]] M https://esolangs.org/w/index.php?diff=60810&oldid=58719 * DMC * (-1) /* Truth Machine */
18:57:50 <esowiki> [[Bitter]] M https://esolangs.org/w/index.php?diff=60811&oldid=60810 * DMC * (+1) /* Truth Machine */
18:58:25 <arseniiv> zzo38: and all sentences formed by removing the => is it only my IRC client, but it seems truncated after “the”
19:02:15 <arseniiv> I don’t remember what the formulation is in that book, though, to tell something useful
19:02:18 <esowiki> [[User:DMC]] M https://esolangs.org/w/index.php?diff=60812&oldid=60517 * DMC * (+100)
19:03:08 <kmc> zzo38: I think it uses the usual definition from modal logic
19:03:22 <kmc> or, not modal
19:03:24 <kmc> what's it called
19:03:56 <kmc> model theory
19:05:38 <arseniiv> there’s also another definition which is basically a simplification of this one applied to the canonical model, which I don’t remember if is always defined
19:05:39 <int-e> [1] has a name: soundness
19:06:07 <zzo38> [3] If X starts with a universal quantifier and all sentences formed by removing the quantifer and replacing that variable with the same number everywhere is true no matter what number you put, then X is true.
19:06:26 <int-e> [2] is really just a facet of soundness. (if X and Y are axioms, then the models that are considered for soundness are those that make X and Y (and the other axioms) true)
19:07:00 <arseniiv> (cont. to mine) ah, yeah, it shouldn’t be defined if there’s no equality in the language (and equality axioms in the theory)
19:07:01 <int-e> [3] is part of the /definition/ of truth of a formula in a model.
19:10:04 <int-e> (You usually need to do [3] a bit differently, working with assignments that assign model elements to the free variables of a formula, because for most models, the objects are not representable as expressions.)
19:11:25 <int-e> (But in the special case that's treated in GEB that's not the case; only the standard model is really considered (just the natural numbers, no nonstandard ones), and all those can be represented as 0, S0, SS0, etc.)
19:23:43 <esowiki> [[Special:Log/newusers]] create * Fuzzyastrocat * New user account
19:29:01 <arseniiv> btw a big ramble and a question:
19:29:01 <arseniiv> btw nonstandard naturals are a mind-blower: no simultaneously computable addition and multiplication is like wtf should it at all be possible right here, aren’t we talking about simple natural-numbery things?
19:29:01 <arseniiv> and we can’t get rid of nonstandard models either: say, we take second-order logic axiomatization, but now we don’t have several crucial properties of first-order language;
19:29:01 <arseniiv> should we specially pick the standard model, then we could ask ourselves how do we to understand sets (which are needed to define a model, and specifically the standard model)—
19:29:01 <arseniiv> and why aren’t there nonstandard set universe models then (and there are!);
19:29:02 <arseniiv> finally, informal set theory as a base is in this case not much better than simply informal arithmetic (which we were to formalize in the first place as we’re wary about things like those same nonstandards etc.)
19:29:02 <arseniiv> so if I’m getting things right, we are left to presuppose we can somehow work with the standard naturals, akin to presupposing ZFC or PA are consistent, and not much else?
19:29:53 <arseniiv> (oh forgot to delete the second “btw”)
19:33:11 <int-e> I guess people mostly don't think much about it, probably taking a second-order view on the axiom of induction for most purposes.
19:33:57 <int-e> (the second order version is, any set that contains 0 and is closed under taking the successor, contains all natural numbers)
19:34:27 <kmc> @quote skolem
19:34:27 <lambdabot> byorgey says: Escaped skolem! Authorities mount massive search. News at 11.
19:34:29 <kmc> @quote skolem
19:34:29 <lambdabot> byorgey says: Escaped skolem! Authorities mount massive search. News at 11.
19:34:31 <kmc> @quote skolem
19:34:31 <lambdabot> byorgey says: Escaped skolem! Authorities mount massive search. News at 11.
19:34:39 <kmc> @quote Tolkeinesque
19:34:39 <lambdabot> No quotes match. I can't hear you -- I'm using the scrambler.
19:35:45 <int-e> arseniiv: that shifts the problem one level down the stack, of course; I have no clue how that plays out if you take an arbitrary model of ZFC (can we even pinpoint a standard model of ZFC? perhaps using some specific large ordinal?)
19:37:11 <int-e> @quote Tolkienesque
19:37:11 <lambdabot> chrisdone says: anyone got a fixed version of the split library for ghc7? some Tolkienesque error messages about skolems escaping
19:37:41 <int-e> I'm not sure about the Tolkien connection.
19:38:51 <int-e> Is this supposed to allude to the Balrog and Gandalf situation? "Thou shalt not pass!"?
19:39:19 <arseniiv> int-e: as far as I don’t know about it, I’ve thought there would be the same problem, and for a theory ZFC + <existence of a suitably large sets> there should be no less but maybe even more problems (though I don’t see how it can be more, either)
19:41:11 <int-e> arseniiv: one resolution is that mathematicians care more about provability than about truth :P
19:41:43 <kmc> "you shall not pass!" <--- me when I'm wearing a t-shirt :/
19:41:49 <arseniiv> int-e: yeah, I suppose it delivers some peace of mind
19:42:53 <int-e> Personally I also have this illusion that I understand the natural numbers... 0, 1, 2, and so on.
19:42:58 <int-e> What could possibly go wrong? :)
19:43:11 <arseniiv> there are still t-shirt haters in the world? :( isn’t it snobbish
19:43:16 <int-e> (they really are *natural* that way)
19:43:17 <b_jonas> int-e: 0, 1, and 2 are easy. the problem is that there are more natural numbers than those.
19:43:54 <arseniiv> int-e> What could possibly go wrong? :) => yeah, the same feeling there
19:45:04 <arseniiv> I like to say something about inductive types, though it shouldn’t be a panacea if one’s to look closer, but I don’t know type theory on that level
19:47:09 <int-e> b_jonas: I'm not playing that game (the game being: who can name more natural numbers?)
19:47:51 <int-e> > [0..] -- Or maybe I am. But not seriously.
19:47:53 <arseniiv> oh, also about something probably more discoverable: is there any connection between λ term (Y succ) aka ∞, and nonstandard naturals? Perhaps there are much more inequivalent such terms?
19:47:53 <lambdabot> [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,2...
19:48:23 <rain1> no i don't think they have a relationship
19:48:52 <int-e> arseniiv: no, you can't compute with that term. For example x - x = 0 is true for all non-standard natural numbers.
19:48:55 <arseniiv> there seems to be an error in lambdabot, they say 2 is after both 1 and 27
19:49:35 <arseniiv> rain1: int-e: thanks for straightening this out
19:49:35 <int-e> arseniiv: I think you hit the right level of insightfulness there, for this discussion. :)
19:49:53 <esowiki> [[Special:Log/newusers]] create * KerbalEngineer * New user account
19:53:38 <arseniiv> (oh I have two friends playing KSP. They didn’t manage to pull me in yet, though)
19:54:38 <int-e> I consciously try to avoid such time sinks as much as possible. Pure puzzle games are bad enough.
19:55:28 <int-e> (KSP in particular also seems quite expensive. But that's a secondary issue.)
19:56:12 <int-e> (Pure puzzle games... Baba is You is at 35 hours... still not done. I'm stuck on level 3 in Depths...)
19:58:22 <arseniiv> to say about that ∞, or more precisely a coinductive type N̅, some time ago I bemusingly found it’s perfect in defining how many steps for some machine to run; the code uses solely `prev` destructor and becomes very clean (if the language is sufficiently good at expressing N̅)
19:58:43 <arseniiv> hm time sinks is my issue I think
20:02:49 <arseniiv> it even rhymes, it should be true
20:04:48 <int-e> arseniiv: that is a fairly standard trick to make total languages with coinductive types Turing-complete (not sure which it was... Agda, probably): data Result a = Skip (Result a) | Return a
20:05:02 <int-e> (where data is the Haskell thing, so really a codata)
20:06:40 <int-e> For related reasons (avoiding recursion in a worker, helping the compiler to do the right kind of inlining) a similar "Skip" has found its way into some stream fusion libraries (bytestring?).
20:07:46 <int-e> I should probably refresh my memory on where I really encountered those...
20:23:31 <arseniiv> int-e: thanks, I haven’t thought it reaches further!
20:26:44 <arseniiv> though my case even was in a language without explicit codata, and I defined ∞ as a special case, so one could see if the value is ∞. But operationally it was still codata Nat' = Z | S Nat'
20:27:49 <arseniiv> where “operationally” means interoperation between Z, S and prec. I should pick words more accurately
20:27:50 <int-e> I guess it's dual in some sense to the Skip... you can provide an infinite amount of fuel to a computation.
20:29:16 <arseniiv> I thought Skip meant to be analogous to S? (and Return to Z)
20:29:42 <int-e> arseniiv: yes but it's used in a result of a computation rather than as input
20:31:17 <int-e> So the function can be productive (produce a new constructor in finite time) without ever producing an answer.
20:31:56 <int-e> In the end you'll have a non-total run-time system that discards all the 'Skip's and waits for the result.
20:32:29 <int-e> But everything else can be total (respectively productive).
20:38:11 <arseniiv> hm, about duality: runSteps :: Nat' → s → s vs. runStep :: Result s → Result s. Could these be turned to something more explicitly dual?..
20:40:44 <int-e> You'd have runStep :: s -> Result s. (Result is a monad, so that's where you can eat the Skips when forwarding results). I suppose (Nat' -> s) is isomorphic to (Result s) if you think about it operationally; whenever the former consumes a "Suc", the latter will produce a "Skip".
20:41:59 <int-e> This is not a perfect match; maybe Nat' -> (s, Nat') with the convention that the Nat' is the remaining fuel makes it better; then you have a corresponding (state) monad.
20:43:23 <int-e> Maybe Cale will wake up and point out that this is just a pair of adjoint functors and that explains it all somehow. ;-)
20:44:17 <arseniiv> also have a sense of adjointness. Any unknown categorial magic should be due to adjoints!
20:46:22 <Cale> What are we explaining?
20:46:30 -!- AnotherTest has quit (Ping timeout: 255 seconds).
20:48:34 <arseniiv> Cale: hm I think it could be phrased as “in what sense is returning Result s is dual to taking Nat'), but int-e may say it better
20:50:52 <Cale> What is this Result type?
20:51:16 <int-e> the Skip monad, I got the naming wrong.
20:51:53 <arseniiv> okay I’ll probably go and the next day will read the logs
20:51:59 * int-e has always been better with ideas than with terminology.
20:52:08 <Cale> Maybe Free vs. Cofree can explain it...
20:52:56 <int-e> Cale: sorry for the bait, but it was too tempting :)
20:53:24 <arseniiv> could those types be resp. Free somethingsomething and Cofree cosomethingsomething maybe?
20:55:10 <int-e> Oh for this purpose we should probably take [co]data Nat' = Suc Nat'. The Zero constructor will produce a lot of garbage.
20:55:41 <int-e> And then it becomes really weird because we have only one value.
20:56:22 <Cale> .oO( Cofree Proxy a -> b vs. a -> Free Proxy b )
20:57:46 <Cale> I don't actually want more a's :)
20:57:48 <int-e> So there's a mismatch. Nat' -> s needs partiality in the arrows, in whatever category that lives in; the Result s has extra structure in the result (namely the number of Skips).
20:58:22 -!- arseniiv has quit (Ping timeout: 246 seconds).
20:58:37 <Cale> Well, Nat' -> s -> s also means you're theoretically allowed to depend on that Nat' and not just use it as computational fuel
20:58:59 <Cale> and yeah, on the other side, you're effectively producing an additional Nat
20:59:01 <int-e> Yes, that would be the garbage :)
20:59:04 <b_jonas> try taking powers modulo a large prime
20:59:15 <int-e> (depending on the Nat' value)
21:00:20 <int-e> So I want to do something intensional where I look inside the computation and see how many Suc are consumed, and shift that to the output. I guess category theory will not really help there. :)
21:01:02 <int-e> (I also want some linearity... the shifting becomes difficult if the Nat' value ever gets duplicated)
21:04:44 <esowiki> [[Control Character]] https://esolangs.org/w/index.php?diff=60813&oldid=60790 * EnilKoder * (+90) /* Syntax */
21:13:42 -!- FreeFull has quit (Quit: Rebooting).
21:15:03 -!- FreeFull has joined.
21:37:52 <esowiki> [[Control Character]] https://esolangs.org/w/index.php?diff=60814&oldid=60813 * EnilKoder * (-6)
22:30:12 <esowiki> [[Special:Log/newusers]] create * Amapires * New user account
22:56:07 -!- quintopia has quit (Ping timeout: 255 seconds).
23:03:39 -!- quintopia has joined.
23:03:39 -!- tromp has quit (Remote host closed the connection).
23:34:06 <esowiki> [[Special:Log/upload]] upload * Lartu * uploaded "[[File:Ldpl-logo.png]]": LDPL Programming Language Logo
23:39:07 -!- tromp has joined.
23:58:07 <esowiki> [[LDPL]] https://esolangs.org/w/index.php?diff=60816&oldid=60283 * Lartu * (+2311)
23:58:27 -!- Phantom_Hoover has quit (Remote host closed the connection).