00:03:38 <int-e> Sgeo: "it's not enforcing which player can move which pieces" -- that sounds like a problem :P
00:04:30 <int-e> (it's good for a laugh in tic-tac-toe)
00:08:53 <b_jonas> Sgeo: what language is that written in?
00:09:12 <b_jonas> I mean the basic simulator
00:16:32 -!- lynndotpy60 has quit (Quit: bye bye).
00:17:40 -!- lynndotpy60 has joined.
00:19:21 -!- lynndotpy60 has quit (Client Quit).
00:20:28 -!- lynndotpy60 has joined.
00:27:28 <Sgeo> b_jonas, TUTOR
00:30:03 <Sgeo> The code might look a bit weird because I only know how to get source code out by "printing" it, printers of the day were limited in character sets, so the system faked some characters by overlapping. Also alternate fonts were allowed in source code, and basim apparently decided to use that to make fancy NEXT and BACK graphics
00:30:32 <Sgeo> Also because TUTOR is a bit of a weird language
00:33:50 <Sgeo> Here's one fun oddity... conditional statements
00:34:00 <Sgeo> command expression,tagneg,tag0,tag1...
00:34:20 <Sgeo> expression is rounded, if it's negative command uses tagneg, if it's 0 command uses tag0, etc
00:34:36 <Sgeo> Comparison operators use -1 as a true value, so that's convenient
01:24:28 -!- amby has quit (Remote host closed the connection).
02:21:49 -!- ^[ has quit (Quit: ^[).
02:52:07 -!- ^[ has joined.
05:07:58 <korvo> ais523: This was a good blog post. I'd like to share it with Lobsters, if that's alright. I noticed that you don't appear to have a handle there; LMK if you'd like an invite.
05:09:19 <korvo> It was quite interesting to see a presentation without negation or linear implication. I suppose that Rust would not have a reasonable use for negation, and also that the self-duality of linear logic would not correspond to the ability to run Rust code backwards.
05:12:18 <korvo> It's kind of surprising that ? is not a functor. I would normally expect it to carry a (IIRC) monad, actually; there should be natural T -o ?T and ??T -o ?T for all T. But I suppose that Rust has other plans. After all, type negation isn't how Rust represents holes, so why-not doesn't have to be how Rust represents piracy.
05:14:33 <korvo> I really like the idea of ⅋ as collating an object with many methods, of which the caller may use exactly one. That's new to me. It also gives an idea of interpreting negation as stronger-than-necessary preconditions.
05:16:16 <korvo> BTW I don't think ⅋ has a standard name. I call it "paramends". It's got "par" like Girard would want, and a couple other puns, like being an anagram of "ampersand".
05:18:36 <korvo> As I'm sure you know, ! embeds intuitionistic logic; whenever X -> Y, also !X -o Y. This suggests a kind of grand compilation scheme from Cartesian-closed to compact-closed categories which is fairly low-level: negation is allocated memory, why-not is piracy, of-course is ROM or defunctionalized constants, linear implication is mutation.
05:21:03 <korvo> I'm not sure exactly *what* the mutator looks like, though. To use an analogy, when linear logic says X -o Y, it means that we can take an X and chop off one arm and get a Y; the contraposition ~Y -o ~X means that we can take a Y-shaped hole and dig a fourth arm and make an X-shaped hole. (Your font may vary.) So a mutation has to represent both the forwards chop-off-an-arm and backwards dig-a-trench actions simultaneously.
05:21:31 <b_jonas> Sgeo: so you can use that as either a two-way true/false conditional, a three-way negative/zero/positive conditional, or an on-goto with an enumeration
05:22:02 <b_jonas> probably useful for an interpreter like this that needs to have a few long ones to switching on statements and switch on built-in functions or other keywords
05:23:32 <korvo> ais523: I dunno. In summary, this was rad. This was the first time in a long time that I've believed that linear logic is ever a correct choice for computers; I'm normally in the Cartesian-closed/multicategory/operad camp. But you're absolutely right about the naturality of this ? piracy.
05:38:09 <korvo> Oh, one more thought. ! acts like a source and ? acts like a sink; for !T we may obtain as many T as we like, while ?T lets us discard as many extra T as we have. If ! is for things that can be copied, is ? for things that can be...destroyed? Sent? Something might be going on there.
05:38:28 <korvo> Alright, sleep time. Peace.
07:09:21 <esolangs> [[Special:Log/newusers]] create * Geno * New user account
07:31:09 -!- tromp has joined.
07:47:42 -!- Sgeo has quit (Read error: Connection reset by peer).
07:50:58 -!- ais523 has joined.
08:01:13 <ais523> korvo: feel free to post the link on sites like lobste.rs – blog posts are generally intended to be shared
08:02:14 <ais523> I was surprised at linear logic being this relevant too (which is partly why it took me so long to think of it) – every other use of it that I've seen has just been as a method of defining the particular substructural type system that you actually wanted to use (which is often but not always intuitionistic logic)
08:03:29 <ais523> (part of the reason that the blog post took so long to write was that I was trying to understand ⅋ well enough to be able to explain it to other people)
08:04:14 <ais523> fwiw, in terms of standard names, I might be unusual in that i don't need to name symbols at all if there's a standard way of writing/typing them
08:05:08 <ais523> writing about Rust is difficult because the borrow operator & is to me just a symbol, I can use it just fine, but when I try to use it in a sentence it's sometimes preceded by a/an and then I get stuck because I don't know whether or not it starts with a vowel (I don't have a mental pronunciation of it)
08:07:21 <ais523> also, the ! / ? duality is that a ! is a resource that can be used an arbitrary number of times, whereas processing a ? may require an arbitrarily large amount of resources (thus, anything you might use to process the ?, you need an infinite supply of)
08:19:47 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
08:27:26 <ais523> returning a ?T is like saying "I have extra T and I am going to make *you* deal with them"
08:28:03 <ais523> so a ?T isn't a T sink, it's the converse of a T sink – you don't use it to get rid of a T, you return it to get rid of a T
08:49:33 -!- fungot has quit (Ping timeout: 252 seconds).
08:57:32 -!- tromp has joined.
09:18:09 -!- tromp has quit (Ping timeout: 265 seconds).
09:59:04 -!- fungot has joined.
09:59:11 <fizzie> Our internet service was down.
10:00:05 <fizzie> It'd be nice if the ISP had a proper outage status thing, they've got a "checker" but all it ever says is "service may be disrupted", with no details about whether they know what the problem is or if they might have an estimate for when it's fixed.
10:03:29 <fungot> ais523: what's ml good for business apps?" at http://paste.lisp.org/ display/ 2832 files for each target basically, i try to build ccbi
10:09:56 <esolangs> [[Chicken you too beautiful]] https://esolangs.org/w/index.php?diff=164637&oldid=137884 * Kaveh Yousefi * (+234) Added a hyperlink to my implementation of the Chicken you too beautiful programming language on GitHub and supplemented page category tag Implemented.
10:40:21 -!- Everything has joined.
10:45:24 -!- tromp has joined.
11:12:17 -!- Everything has quit (Quit: leaving).
11:21:24 <esolangs> [[User talk:PrySigneToFry]] https://esolangs.org/w/index.php?diff=164638&oldid=164631 * I am islptng * (+175) /* I saw your message */
11:30:09 -!- Lord_of_Life_ has joined.
11:30:34 -!- Lord_of_Life has quit (Ping timeout: 256 seconds).
11:32:59 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
11:50:16 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
11:56:52 -!- amby has joined.
12:00:03 -!- tromp has joined.
12:17:14 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
12:28:51 <esolangs> [[Special:Log/newusers]] create * AUnitSquare * New user account
12:33:09 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=164639&oldid=164636 * AUnitSquare * (+306)
13:30:45 -!- tromp has joined.
15:00:55 <korvo> ais523: Oh, that's an interesting way of thinking of things. I normally think of ?T as an endpoint, not a thing that can be passed around. Good food for thought.
15:02:18 <korvo> https://lobste.rs/s/ccy3b6/pirate_based_logic_rust_shared
15:58:27 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
16:18:06 -!- tromp has joined.
16:19:17 -!- impomatic has joined.
16:28:50 <esolangs> [[Game:Esochain]] https://esolangs.org/w/index.php?diff=164640&oldid=164610 * Hotcrystal0 * (+36)
16:41:19 <esolangs> [[Game:Esochain]] https://esolangs.org/w/index.php?diff=164641&oldid=164640 * Aadenboy * (+42) kill server 2 + replace non-esolang on server 5
16:41:29 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
17:34:48 -!- tromp has joined.
17:53:57 -!- Lord_of_Life has quit (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine).
17:56:21 -!- Lord_of_Life has joined.
18:03:26 -!- JGardner has joined.
18:24:13 -!- ais523 has quit (Quit: quit).
18:30:06 -!- impomatic has quit (Quit: Client closed).
18:42:59 -!- trumae has joined.
20:21:49 -!- trumae has quit (Remote host closed the connection).
20:52:13 <esolangs> [[User:Iloveunicorns]] N https://esolangs.org/w/index.php?oldid=164642 * Iloveunicorns * (+573) Created page with "<p>I love unicorns. Esolangs too.<br> Im learning CSS, HTML and MediaWiki for decorating this page<br><br>I using Python for my interpreters, but i can tell ChatGPT write me interpreter on HTML or JS/Java.<br><br>I remember I made a visual interpreter fo
21:43:06 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
21:58:00 -!- efrain has quit (Quit: efrain).
22:21:42 -!- Sgeo has joined.
23:40:14 <esolangs> [[Il]] N https://esolangs.org/w/index.php?oldid=164643 * Iloveunicorns * (+2192) Created page with "{{infobox proglang | name = Il | paradigms = Imperative, Accumulator-based | author = [[User:Iloveunicorns]] | year = 2025 | class = Total | majorimpl = Python | influenced = [[BittyLang]], [[Deadfish]], etc. }} '''Il''' is an esolang was