00:15:49 -!- Artea has joined.
01:19:04 <esolangs> [[User:Hotcrystal0/Chess piece strength]] https://esolangs.org/w/index.php?diff=161029&oldid=161021 * PrySigneToFry * (+35)
01:20:14 <esolangs> [[User:PrySigneToFry/Silicon dioxide in a polypropylene box/Chess between HCr0 and PSTF]] https://esolangs.org/w/index.php?diff=161030&oldid=160928 * PrySigneToFry * (+124)
01:22:07 -!- moony has quit (Quit: leaving).
01:22:34 -!- iovoid has quit (Quit: iovoid has quit!).
01:22:34 -!- Bowserinator has quit (Quit: Blame iczero something happened).
01:44:53 -!- Bowserinator has joined.
01:44:59 -!- moony has joined.
01:49:03 -!- iovoid has joined.
02:12:49 <esolangs> [[Mint remake]] https://esolangs.org/w/index.php?diff=161031&oldid=161010 * Hajunsheng * (+82)
02:59:16 <esolangs> [[Smotslang]] M https://esolangs.org/w/index.php?diff=161032&oldid=160989 * Clover-not-used * (+106) sync
04:26:50 <esolangs> [[User:Tommyaweosme]] https://esolangs.org/w/index.php?diff=161033&oldid=161013 * Tommyaweosme * (-2886) ~ placeholder for phase 2 message! its 11:26 am! ~
04:35:22 <esolangs> [[Smotslang]] M https://esolangs.org/w/index.php?diff=161034&oldid=161032 * Aadenboy * (+39) link
05:00:25 <esolangs> [[Semi-serious language list]] https://esolangs.org/w/index.php?diff=161035&oldid=161020 * None1 * (+13) /* R */ Record definitely fits the constraints
05:35:31 <esolangs> [[Kolakoski sequence]] https://esolangs.org/w/index.php?diff=161036&oldid=155833 * PkmnQ * (+387) Add Sceql
05:49:50 <esolangs> [[User:I am islptng]] https://esolangs.org/w/index.php?diff=161037&oldid=159547 * I am islptng * (+247)
05:50:53 <esolangs> [[User:I am islptng]] https://esolangs.org/w/index.php?diff=161038&oldid=161037 * I am islptng * (+20)
05:54:00 <esolangs> [[Semi-serious language list]] https://esolangs.org/w/index.php?diff=161039&oldid=161035 * PkmnQ * (+24) Qdeql and Sceql (they seem distinct enough to be separately listed)
05:54:06 <esolangs> [[]] https://esolangs.org/w/index.php?diff=161040&oldid=160132 * PkmnQ * (+28) Type 39 (and probably more) is self-modifying
06:07:42 -!- tromp has joined.
06:18:33 -!- Sgeo has quit (Read error: Connection reset by peer).
06:37:19 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
06:44:43 -!- tromp has joined.
08:33:10 -!- chomwitt_alt has joined.
08:41:21 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
09:48:30 -!- tromp has joined.
09:50:41 <esolangs> [[User:Pifrited]] N https://esolangs.org/w/index.php?oldid=161041 * Pifrited * (+15) Created page with "<pre> :P </pre>"
10:25:02 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=161042&oldid=160998 * Dmitry samorodyuk * (+300)
10:30:46 <esolangs> [[Boringscript]] N https://esolangs.org/w/index.php?oldid=161043 * Dmitry samorodyuk * (+86) Created page with "{{wip}} Boringscript - is a maximally boring esolang, developed by Dmitry Samorodyuk."
10:30:55 -!- ais523 has joined.
10:34:33 <ais523> korvo: that helped, I think – I was mixing levels and interpreted ? as not-a-monad because I thought it was not-a-functor, but it is a functor on *pure* functions and forgot at the time hat linear logic rules had to be applied to the capabilities of impure functions
10:35:10 <ais523> then later on I remembered that impure functions do have to follow linear logic rules with how they used their capabilities, but by then I'd forgotten that this would make it a functor
10:35:40 -!- Lord_of_Life_ has joined.
10:35:42 -!- Lord_of_Life has quit (Ping timeout: 265 seconds).
10:36:29 <ais523> (or another way to put it is that in order to produce a ?T -o ?U, you need a !(T -o U), not just a T -o U)
10:37:00 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
10:53:45 <ais523> the thing I'm dealing with definitely does "pure" (although that's a misleading name in this case) and flatten, it's just the map operation that's suspect
10:53:53 <ais523> but ? is in the same situation
11:06:18 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
11:11:16 -!- tromp has joined.
11:30:40 <esolangs> [[User talk:/w/wiki/index.php/Talk:index.php/Main page]] https://esolangs.org/w/index.php?diff=161044&oldid=159778 * PrySigneToFry * (+70)
11:53:26 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
12:19:40 -!- amby has joined.
12:36:49 -!- moony has quit (Quit: leaving).
12:37:07 -!- Bowserinator has quit (Quit: Blame iczero something happened).
12:37:07 -!- iovoid has quit (Quit: iovoid has quit!).
12:37:32 -!- moony has joined.
12:37:40 -!- Bowserinator has joined.
12:41:13 -!- iovoid has joined.
12:52:00 -!- chomwitt_alt has quit (Ping timeout: 265 seconds).
12:57:07 <esolangs> [[Special:Log/newusers]] create * Aquafishy7 * New user account
13:04:49 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=161045&oldid=161042 * Aquafishy7 * (+90)
13:06:23 <esolangs> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=161046&oldid=161045 * Aquafishy7 * (+58)
13:06:52 <esolangs> [[HQ9~]] https://esolangs.org/w/index.php?diff=161047&oldid=149166 * Aquafishy7 * (-895)
13:06:59 <esolangs> [[HQ9~]] https://esolangs.org/w/index.php?diff=161048&oldid=161047 * Aquafishy7 * (+0)
13:13:06 -!- tromp has joined.
13:17:38 <ais523> in any case, one thing that I'm now trying to work out is whether linear logic's ? is a "modality" or not, in the sense of modal logic – I'm having trouble working this out primarily due to not being able to find a clear definition of what a modality is or isn't (and it may be that no agreed-on definition exists?)
13:26:58 <esolangs> [[Sceql]] https://esolangs.org/w/index.php?diff=161049&oldid=72629 * PkmnQ * (+389) /* Example programs */ Add Kolakoski sequence to examples
14:20:50 <esolangs> [[Special:Log/move]] move * Pifrited * moved [[User:Pifrited/Simple2DMachine]] to [[Simple2DMachine]]
14:20:50 <esolangs> [[Special:Log/move]] move * Pifrited * moved [[User talk:Pifrited/Simple2DMachine]] to [[Talk:Simple2DMachine]]
14:43:03 <korvo> ais523: A modality is merely a functor, FWIW.
14:43:30 <ais523> OK – I'm still not convinced ? is a functor in the traditional sense
14:43:45 <ais523> but I guess it depends on how you convert the signature of fmap from classical logic to linear logic
15:08:10 <korvo> Doesn't have to be a Functor exactly, but it (Cheng-)morally ought to be. nLab says, roughly, a modal operator ♯ merely sends propositions X to propositions ♯X such that some reasonable properties are satisfied.
15:08:44 <korvo> If you assume that X can be any prop, including e.g. an internal hom Y -o Z, then it follows that ♯ is a functor.
15:10:14 <korvo> Actually phrasing a functor within linear logic is tricky. In general, anything intuitionistic with shape X -> Y needs to become either X -o !Y or !(X -o Y) in the linear world in order to have equivalent functionality.
15:14:18 <esolangs> [[User talk:I am islptng]] https://esolangs.org/w/index.php?diff=161054&oldid=160857 * Cycwin * (+256) /* Nooooooooooooooooooooo */ new section
15:15:49 <esolangs> [[User talk:I am islptng]] https://esolangs.org/w/index.php?diff=161055&oldid=161054 * Cycwin * (+0) /* Nooooooooooooooooooooo */ (
15:21:48 <esolangs> [[GebAuI]] https://esolangs.org/w/index.php?diff=161056&oldid=160313 * Tommyaweosme * (+10)
15:22:16 <esolangs> [[GebAuI]] https://esolangs.org/w/index.php?diff=161057&oldid=161056 * Tommyaweosme * (+0)
15:27:24 <esolangs> [[User:Tommyaweosme]] https://esolangs.org/w/index.php?diff=161058&oldid=161033 * Tommyaweosme * (+639)
15:39:14 <ais523> korvo: right – if you convert (X → Y) to !(X -o Y) then ? is a functor
15:40:44 <korvo> ais523: FWIW the underlying semantics have a *very* natural mapping explaining this. Every adjunction gives a monad and comonad. Sets and vector spaces (over some fixed field K) are adjoint. ? and ! are precisely the monad and comonad from that adjunction.
15:41:10 <korvo> (One must accept that classical logics are interpreted in sets and linear logics are interpreted in vector spaces, I suppose.)
15:43:09 <ais523> this makes sense and is consistent with what I've been discovering
15:45:21 <korvo> Decoding https://ncatlab.org/nlab/show/%21-modality a bit, ? : Set -> Set sends a set X to the function set Hom(1, Lin(X)) where Lin(X) is linear combinations of X.
15:46:38 <korvo> Specifically, each element x in X is sent to a naming function \() -> {x: 1} that selects the linear combination which is 100% x (and 0% any other element in X)
15:49:21 <korvo> I guess that the monadic join is Bayes' rule for finite X. I know enough probability theory to imagine that it's not so simple for infinite X.
15:54:57 <korvo> ais523: Okay, actually, this now makes sense for refs, at least in the finite case. Suppose we have a ref to some enum type. As a matter of probability, I suppose that we can describe *which* enum it points to as a linear span.
15:56:36 <korvo> As expected from having our semantics actually in sets, we only have refs that 100% point to a single case; there's no actual superpositions in memory. Nonetheless we still have the idea that we can take a ref to a ref and that they can be flattened down with a monadic join.
15:57:07 <ais523> yes – the "I am borrowing this and I can copy the borrow" aspect of references clearly flattens perfectly
15:58:15 <korvo> Borrowing a bit from QM, the PBR theorem says that we can't avoid excess baggage when doing this modeling; even though we only use the non-superpositions, we have to pay for the superpositions too.
15:59:07 <korvo> So when we store refs as pointers, and do pointer-chasing, we're actually implementing a very fast algorithm for finding representatives of those refs. It's a classic one, too: union/find!
16:00:26 <korvo> ...Maybe that was a big leap, sorry. PBR says that if we want to faithfully implement the monadic join then we'd better implement it for all superpositions *or* we have to carry information about how each state was prepared.
16:00:50 <korvo> So, let's take that second branch. Modern pointers have provenance.
16:01:06 <ais523> yes – I've spent a while thinking about how to formalise provenance
16:04:41 <ais523> @hoogle Either x y -> (x -> z) -> (y -> z) -> z
16:04:41 <lambdabot> Overhang onRight :: Either a b -> (a -> c) -> (b -> c) -> c
16:05:37 <ais523> @hoogle Either x y -> (x -> a) -> (y -> b) -> Either a b
16:05:38 <lambdabot> Overhang onBimapSecond :: Bifunctor t => t a c -> (a -> b) -> (c -> d) -> t b d
16:05:57 <lambdabot> Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d
16:06:39 <korvo> e'e iu Happy to help.
16:06:41 <ais523> this is so much easier in classical logic :-D
16:07:26 <ais523> @hoogle Either a a -> a
16:07:27 <lambdabot> Data.Either.Utils fromEither :: Either a a -> a
16:07:27 <lambdabot> Data.Either.Extra fromEither :: Either a a -> a
16:07:27 <lambdabot> Extra fromEither :: Either a a -> a
16:07:39 <korvo> Yeah, linear logic is very tricky. I had started working on foundations in linear logic, but gave up because there's no clear set of axioms for it and one ends up having to put ! onto every theorem anyway.
16:10:31 <ais523> the thing I was thinking about is that "a -> X a", "b -> X b", and "X a b -> (a -> c) -> (b -> c) -> c" collectively imply X = Either, and this lets you define your own Eithers even if the language doesn't have enums
16:11:10 <ais523> err, "a -> X a b", "b -> X a b", and "X a b -> (a -> c) -> (b -> c) -> c"
16:12:12 <ais523> but, if you translate that definition into linear logic naively, you get ⅋ rather than the expected ⊕
16:24:55 <ais523> (well, not quite – you end up with (c⅋c) at the end rather than c)
16:27:47 <korvo> Right, the categorical product and sum are given by the additive connectors. (BTW, did you know that ⅋ doesn't have a standard name? I call it "paramends", an anagram of "ampersand".)
16:28:54 <korvo> There is a perspective that makes this natural, although it's jargon-dense: https://ncatlab.org/nlab/show/linear%2Blogic#polycategories
16:29:34 <ais523> Wikipedia calls it "par"
16:30:21 <ais523> which after thinking about it for a while, I decided might stand for "parallel" (the Rust approximation seems to be "you can consume an 'A⅋B' only via the use of code which could consume an A and a B in parallel")
16:32:08 <korvo> I'm not sure if Rust can internalize it properly. The idea is that A ⅋ B ≈ ~A -o B; linear logic is aggressively De Morgan. Symmetrically, we also have ~B -o A. It's like two transformations in a single bundled object.
16:33:48 <ais523> very few programming languages can internalize it properly, I think
16:34:14 <ais523> but I'm starting to understand it intuitively even though it doesn't translate very easily to useful programming concepts
16:34:50 <korvo> Even in vending-machine semantics it's tricky. X ⅋ Y means that you may engage the vending machine in a Socratic dialogue about the meaning of life, including the concept that X doesn't exist and never made sense as a concept. The machine accepts your proof and emits a can of Y.
16:35:06 <APic> This Chan pwns
16:35:17 <ais523> (the other three connectives translate easily: ⊗ is tuples/structs, ⊕ is disjoint union (which Rust calls "enum"), and & is a type that can be coerced into either of two types, `impl Into<A>+into<B>` in Rust)
16:35:26 <APic> Sadly i do not have enough Intelligence to understand most of it
16:35:33 <APic> But i still enjoy reading it
16:35:33 <korvo> Also, technically, you may prove that Y doesn't exist, in which case it will vend a can of X. How? I don't know, and this is part of why QM is so mysterious.
16:36:00 <korvo> APic: <3 Thanks. I know I'm a grump, but I appreciate you.
16:37:42 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
16:52:48 -!- tromp has joined.
17:22:26 <esolangs> [[JollyScript]] https://esolangs.org/w/index.php?diff=161059&oldid=148912 * IntGrah * (-45) /* Computational class */
17:42:56 -!- chomwitt_alt has joined.
19:08:20 -!- ais523 has quit (Quit: quit).
19:12:15 -!- Guest95 has joined.
19:21:15 -!- Guest95 has quit (Quit: Client closed).
20:04:14 -!- chomwitt_alt has quit (Ping timeout: 260 seconds).
20:12:09 -!- moony has quit (Quit: leaving).
20:12:35 -!- iovoid has quit (Quit: iovoid has quit!).
20:12:35 -!- Bowserinator has quit (Quit: Blame iczero something happened).
20:19:43 -!- ais523 has joined.
20:20:12 <ais523> esolangs: how would one write an interpreter for But Is It Art?
20:20:32 <esolangs> ais523: Writing an interpreter for But Is It Art (BIA) is a fascinating challenge! Here's a simplified approach: 1. **Parse:** BIA's code is a series of "art" statements, each with a specific meaning. You'd need a parser to break down the code into its components. 2. **Interpret:** BIA's "art" statements are interpreted based on their meaning. This could...
20:20:32 <esolangs> involve logic, data manipulation, and potentially even visual rendering. 3. **Output:** The interpreter would then output the result of the "art" statement, which could be a visual representation, a text output, or even a combination of both. Remember, BIA is about exploring the boundaries of art and language, so the interpreter should reflect that...
20:20:34 <esolangs> [[!Frontal Lobe Lobotomy]] https://esolangs.org/w/index.php?diff=161060&oldid=161005 * Stkptr * (+6) explicitly finite, but feasibly infinite
20:21:57 -!- Bowserinator has joined.
20:21:57 -!- moony has joined.
20:22:48 <ais523> my expectations were low, and the result nonetheless still failed to live up to them
20:23:00 <korvo> That almost seems like a RAG miss.
20:23:48 <ais523> what does RAG stand for here?
20:25:31 -!- iovoid has joined.
20:25:41 <korvo> Retrieval-Augmented Generation. Before the bot generates a response, there's a search step that looks up relevant snippets. By "miss" I mean that the RAG step didn't return anything at all, so the bot sort of winged it.
20:26:21 <korvo> esolangs: Who designed the language But Is It Art? and when did they publish it?
20:26:25 <ais523> I did write the name of an esolang literally, but it is possible that the retriever nonetheless failed to find the right page
20:26:42 <korvo> I'm wondering if the ? character got stripped somewhere in the pipeline.
20:27:04 <ais523> but, the response arrived "too quickly" which is evidence of the search missing
20:27:30 <esolangs> korvo: But Is It Art? was designed by User:ais523 in 2017.
20:28:11 <ais523> the wiki agrees that it was 2017 (I couldn't remember the exact year), so that looks like the correct page was found
20:29:02 <korvo> There's also the generic shape of the response. "X is a fascinating challenge! Let's work step by step:" tastes like the RLHF that was popular about 2-3yrs ago and suggests to me that the response isn't customized for any particular snippets.
20:30:00 <ais523> yes, it's a very LLVM sort of answer
20:30:10 <ais523> LLVM is a compiler backend
20:32:06 * ais523 reflects that the typo is probably an indication of having their priorities in the right place
20:33:16 <korvo> esolangs: How would one write an interpreter for the language But Is It Art?
20:33:32 <esolangs> korvo: Writing an interpreter for But Is It Art (BIA) is a fascinating challenge! Here's a simplified approach: 1. **Parse:** BIA's code is a series of "art" expressions, which need to be parsed into a structured data format. 2. **Evaluate:** BIA's expressions are evaluated based on their meaning, potentially using a combination of built-in functions and...
20:33:32 <esolangs> custom logic. 3. **Output:** The interpreter outputs the result of the evaluation, which could be a string, a number, or even a visual representation. Remember, BIA is about artistic expression, so the interpreter should prioritize readability and flexibility.
20:34:02 <korvo> Cached? So I'd guess that something's not hitting.
20:34:14 <ais523> in the original question, it did seem to recognise that I was talking about a programming language, despite the question not stating htat
20:34:24 <ais523> I guess "write an interpreter" is a sufficiently loaded phrase to suggest it
20:34:29 <korvo> esolangs: What is the recommended approach for implementing the language But Is It Art?
20:34:42 <ais523> (with the verb "write" ruling out the other possible meanings of "interpreter")
20:34:43 <korvo> Oh, yeah, that could definitely be a factor.
20:34:46 <esolangs> korvo: Implementing "But Is It Art?" is a challenge, as it's a highly experimental language focused on artistic expression. **Recommended approach:** 1. **Embrace ambiguity:** Don't focus on strict syntax. Allow for unconventional code structures and interpretations. 2. **Prioritize visual output:** Use graphics, animations, or interactive elements to...
20:34:46 <esolangs> showcase the "art" aspect. 3. **Leverage external tools:** Integrate with libraries for image manipulation, sound synthesis, or other artistic mediums. 4. **Focus on the experience:** Prioritize the user's interaction and the emotional impact of the output. Remember, the goal is to create something unique and visually compelling, not to adhere to...
20:34:46 <esolangs> traditional programming paradigms.
20:35:27 <ais523> OK, it clearly recognises that it's an esolang, but it's unclear whether that was done via retrieval or not
20:36:10 <ais523> in a twisted sense, this is a good answer – it is a hard language to implement correctly, so it is trying to persuade me that implementing it incorrectly would be a more aesthetic approach
20:37:31 <ais523> in any case, the whole Claude Plays Pokémon thing convinced me that LLMs are incredibly bad at reasoning about 2D space, so it probably wouldn't be able to draw conclusions from the language specification about how it might be implemented
21:07:45 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…).
21:07:47 -!- FreeFull has joined.
21:38:05 -!- chomwitt_alt has joined.
21:43:10 -!- ais523 has quit (Quit: sorry about my connection).
21:45:46 -!- ais523 has joined.
21:49:05 -!- chomwitt_alt has quit (Ping timeout: 248 seconds).
22:06:13 -!- FreeFull has quit.
22:26:52 -!- Sgeo has joined.
22:52:07 <Sgeo> IBM 305 RAMAC is ... almost ... giving me BytePusher vibes
22:52:38 <Sgeo> Instructions being a source, a destination, and... some control thing
22:57:44 <Sgeo> The control codes are defined by changable hardware wiring
23:01:45 <Sgeo> Ok I need a plugboard tutorial
23:11:39 <Sgeo> There's actually a generic plugboard configuration, so a program can be written entirely as a stored program. But there's a warning that this reduces processing speed
23:45:26 <Sgeo> Things like multiplication are ... memory/mapped IO I think? Didn't get that far reading yet but there's a reference to a multiplicand track. Although maybe that means something else
23:52:19 <ais523> I think there are both esoteric and non-esoteric transport-triggered architectures
23:52:37 <ais523> where every instruction except mov is triggered by writing to or reading from particular addresses
23:53:16 <ais523> I've used a processor where simple arithmetic and conditional instructions existed (including RMW), but everything more complicated was transport-triggered
23:53:39 <ais523> e.g. to do an indirect memory access (the equivalent of a pointer arithmetic), you would write the address to a known memory location and then read or write to address 0
23:54:13 <ais523> and the hardware would intercept attempts to read/write address 0 and instead change the address to match the value in the specific memory location
23:59:30 <Sgeo> "each vertical row of hubs"... that's not what the word row means