00:03:01 <tswett[m]> Now I have left turning and right turning. I've implemented...
00:03:28 <tswett[m]> It's capable of facing any direction that any turning machine can face.
00:28:55 <tswett[m]> So, shoot, I might be nearly done implementing my rule. I think I have enough stuff to make an almost-replicator now.
00:52:14 <zzo38> shachaf: What features is that that ALGOL 68 has and is not present in many or any modern languages?
01:55:57 <esowiki> [[User talk:A]] https://esolangs.org/w/index.php?diff=65389&oldid=65388 * Areallycoolusername * (+313) Ask User: A for info on String Compression
01:57:35 <shachaf> https://en.m.wikipedia.org/wiki/Comparison_of_ALGOL_68_and_C%2B%2B talks about some features
01:57:58 <shachaf> I think distinguishing values from memory locations is pretty unusual.
02:00:57 -!- MDude has joined.
02:05:31 -!- MDude has quit (Ping timeout: 246 seconds).
02:16:31 <zzo38> Some of the features seem like good. Some seem like should be implemented by macros instead, perhaps.
02:37:57 -!- xkapastel has quit (Quit: Connection closed for inactivity).
02:41:54 <zzo38> Is there a implementation of Haskell in JavaScript that can interface Haskell codes with JavaScript codes?
02:49:35 <tswett[m]> Dang, I successfully built an almost-replicator.
02:50:13 <tswett[m]> Let's see if I can upload some pictures.
02:50:35 * tswett[m] uploaded an image: image.png (82KB) < https://matrix.org/_matrix/media/v1/download/matrix.org/jCTRLEizSoOEpqnHMyfvfNFQ >
02:51:16 * tswett[m] uploaded an image: image.png (137KB) < https://matrix.org/_matrix/media/v1/download/matrix.org/pNIJWOGhAgTGjPJQkIAUumtf >
02:53:04 <tswett[m]> So, this is essentially a Langton's loop... more or less.
02:53:37 <tswett[m]> The genome consists of five segments, separated by orange signals.
02:56:04 <tswett[m]> Segment 1 extends the construction arm and puts filter data along it using teal and cyan signals. Segment 2 simply extends forward a bunch of times using cyan segments. Segment 3 makes a single left turn, then moves forward 5 times. Segment 4 turns left, moves forward 4 times, and turns left again. Segment 5 turns right, moves forward 5 times, and turns right again.
02:58:05 <tswett[m]> Ummmm, a video would make this a lot clearer. Maybe.
03:06:52 -!- tromp has quit (Read error: Connection reset by peer).
03:07:28 -!- tromp has joined.
03:24:15 <tswett[m]> Okay, have a very smol animated GIF which shows how it works.
03:24:26 * tswett[m] uploaded an image: radiator2.mc-2.gif (383KB) < https://matrix.org/_matrix/media/v1/download/matrix.org/ubOayEqlZPdhljpZLpbVdZCe >
03:25:49 <tswett[m]> The first segment writes a data tape along the construction arm. That data tape is then read in order to determine which segments of the program to pass through to the daughter, and which segments to suppress.
03:26:31 <tswett[m]> Although the mother creates a near-copy of itself, and then sends its complete genome into the daughter, neither the mother nor the daughter is capable of reproducing afterwards.
04:16:59 <Sgeo_> I am getting the impression that there are multiple versions of Retroforth, mostly unrelated except in name and creator
04:32:26 <zzo38> Do you know about compiling LLVM into new targets?
04:36:43 <Sgeo_> Awezoome did a Pachelbel Canon in D
04:37:26 <Sgeo_> https://modarchive.org/module.php?34369
04:38:47 <Sgeo_> Canon of the Three Stars?
04:42:10 <Sgeo_> tswett[m], huh, Mirek's cellebration came with Langton's
04:42:31 <kmc> it comes with a lot of things
04:43:12 <Sgeo_> (Or something similar. The website doesn't say Langton's, hmm)
04:45:44 <Sgeo_> http://www.mirekw.com/ca/rullex_udll.html#DNA
04:48:22 <Sgeo_> https://gist.github.com/Sgeo/ead48728917153cb8fe2c2c2221f2e75
04:48:55 -!- MDude has joined.
05:10:25 <tswett[m]> So, it should be "pretty easy" for me to implement full self-replication in my CA.
05:10:59 <tswett[m]> I can just imitate exactly what Langton's Loops does.
05:12:23 <tswett[m]> But I'd also like to try to think of a better way.
05:52:33 <esowiki> [[User talk:A]] M https://esolangs.org/w/index.php?diff=65390&oldid=65389 * A * (+290) /* Concern */
05:53:52 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)).
06:46:55 -!- cpressey has joined.
06:51:02 <cpressey> Good morning. I am happy to say that I was wrong a few days ago. It does in fact appear possible to build arbitrary control structures directly in a second-order concatenative language.
07:05:57 <cpressey> I should have an esolang around this soon. Maybe not today though.
07:11:45 <int-e> cpressey: Do you have a viable definition of the concept? I imagine "concatenative" translates to composition of functions, and second-order means that those functions have shape (p -> q) -> (p -> q) for some (non-functional, but perhaps algebraic) types p and q?
07:13:18 <cpressey> int-e: Basically exactly that, yes.
07:13:38 <cpressey> "Program states to program states"
07:13:59 <cpressey> They happen to be stacks on unbounded integers in the esolang.
07:16:37 <int-e> I guess I can always replace (p -> q) by ((p,q) -> (p,q)) :)
07:22:52 -!- Sgeo__ has joined.
07:24:00 <int-e> Hmm, but I guess you have an informal naturality condition in there as well... something that prevents the translation of, say } (end of block) to embed a full interpreter of your language...
07:25:55 -!- Sgeo_ has quit (Ping timeout: 248 seconds).
07:26:47 <int-e> (Otherwise we can just enter a "recording" program state on encountering the first '{', collect the program source including nested '{','}' pairs, and execute it upong the final '}', possibly in a loop.)
07:30:06 <cpressey> int-e: Yes. Or if the function being composed can be examined, } could examine it and look for the { and copy the contents -- basically equivalent to what you just said.
07:30:45 <cpressey> I guess my use of "directly" is trying to suggest that the program doesn't have to examine itself like this.
07:31:54 <cpressey> (Functions aren't ordinarily considered something you can examine the structure of, but... you could just say you're concatenating a monoid and later on you'll interpret it so for now you could examine it. Or something.)
08:08:25 <cpressey> Grr. I think I have to downgrade "arbitrary" to "More arbitrary than I thought, but not totally arbitrary"
08:14:02 -!- Lord_of_Life has quit (Ping timeout: 268 seconds).
08:15:34 -!- Lord_of_Life has joined.
08:23:18 -!- Phantom__Hoover has joined.
09:51:38 <cpressey> I agree with shachaf that exceptions can be kind of awful. But handling possible error returns in every single place a function is called (and every place *that* function is called etc) is also awful.
09:51:55 <cpressey> If you think of them as "non-local exits" they don't seem as bad.
09:52:13 <shachaf> Exceptions are an unusual kind of non-local exit because they don't specify where the exit goes to.
09:52:25 <shachaf> Compared to setjmp or continuations or whatever.
09:55:39 <cpressey> You have to think about where they're catched. The type of exception usually suggests some kind of interface, or at least convention, for where it should be catched. But it's very difficult to formalize it, and raising exceptions at every opportunity makes it that much harder.
09:56:07 <cpressey> I mean, seriously, `car` in Scheme can throw. `[]` in Python can throw.
09:56:12 <kmc> shachaf: is 'try' like capturing a continuation and then assigning it to a dynamically-scoped variable?
10:02:11 <cpressey> Often (sorry, just ranting here) I catch an exception only to throw a different exception. I've done this enough that in my head I call this the "exception translation antipattern".
10:03:10 <shachaf> kmc: Yes, I think it's a bit like a dynamic vs. lexical scope thing.
10:03:41 <shachaf> cpressey: I started writing a bit about error handling at http://slbkbs.org/tmp/5.error.handling.txt though I never finished it.
10:05:27 <cpressey> Java's attempt to build an effect system around exceptions feels like an attempt to make it more like lexical scope. Thing is, Java programmers tell me they hate it and they just end up using unchecked exceptions instead.
10:05:53 <cpressey> shachaf: Will give it a look, thx
10:06:07 <shachaf> cpressey: Later I found out that Zig has almost the same system I came up with.
10:06:47 <shachaf> Checked exceptions doesn't seem like the same sort of thing.
10:08:08 <cpressey> "If I raise X I want to know that I've been called by someone that is prepared to catch X" sounds, okay maybe not "lexical", but a lot less "dynamic" in scope
10:08:35 <cpressey> "someone", there I go personifying things again. Dijkstra would not approve
10:09:18 <shachaf> What's wrong with personifying things?
10:10:12 <shachaf> Exceptions try to do a lot of things and they don't seem to do any of them that well.
10:10:37 <cpressey> I should try to find the note where he blames a lot of problems in software on people's tendency to anthropomoriphize it
10:10:41 <int-e> You should never anthropomize computers. They hate it when you do that.
10:11:02 <shachaf> If I write "foo() raises XError { bar(); vaz(); }" and I expect vaz to fail with XError, it becomes invisible to me that bar might also do that.
10:11:54 <int-e> [second correction elided]
10:12:17 <shachaf> do not antwerpomorphize the dutch hth
10:16:18 <cpressey> https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html
10:16:40 <cpressey> "My next linguistical suggestion is more rigorous. It is to fight the "if-this-guy-wants-to-talk-to-that-guy" syndrome: *never* refer to parts of programs or pieces of equipment in an anthropomorphic terminology, nor allow your students to do so."
10:17:54 <shachaf> What about "if you give me an epsilon I give you a delta"
10:18:11 <cpressey> I acknowledge that Dijkstra held opinions, I don't necessarily agree with them, nor always understand the reasons for them
10:18:19 <Taneb> shachaf: what if I don't give you an epsilon
10:19:32 <shachaf> This reminds me, I have an ill-formed question about models of computation that I don't remember whether I asked in here before.
10:19:49 <int-e> cpressey: meh I think of programs as actors that modify some virtual world... personification is just a tiny step further.
10:20:32 <esowiki> [[Foo machine]] N https://esolangs.org/w/index.php?oldid=65391 * A * (+1670) Created page with "[[Foo machine]] is a hypothetical machine created by [https://codegolf.stackexchange.com/questions/189572/does-this-foo-machine-halt Leo Tenenbaum] in order to demonstrate tha..."
10:20:41 <int-e> (I also allow "worlds" to be terribly abstract)
10:20:54 <shachaf> There are some facts, like "seemingly impossible functional programs" (equality of total predicates over infinite streams of bits is decidable, etc.) and the fact that integration is computable, that seem pretty mysterious at first when you look at them from the standard perspective.
10:20:58 <esowiki> [[Foo machine]] M https://esolangs.org/w/index.php?diff=65392&oldid=65391 * A * (+4)
10:21:09 <shachaf> Or even if they don't seem mysterious, the implementation details tend to be fairly convoluted.
10:22:01 <shachaf> In fact the actual idea of the implementation is very simple so it's annoying that it has to be expressed the way it does.
10:22:56 <shachaf> I'd much rather see e.g. the integration thing described as an explicit non-nested dialog between two parties.
10:23:18 -!- wob_jonas has joined.
10:23:50 <kmc> shachaf: can you give an example of that?
10:23:59 <kmc> maybe for impossible functional programs
10:24:04 <kmc> how is that expressed as a dialog?
10:24:05 <shachaf> Something like, we have a single communication channel, and you can send me questions about the function, and I can ask you questions about the arguments, and so on.
10:24:28 <kmc> these sorts of things are also v. important in complexity theory and cryptography, of course
10:24:32 <kmc> arthur-merlin classes, etc
10:24:45 <shachaf> kmc: Let's see, what are the existing ways of expressing it?
10:24:46 <int-e> kmc: http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
10:25:02 <shachaf> I know two ways which are kind of different.
10:25:06 <kmc> int-e: I've seen the article; I was wondering specifically how to express it as a dialog
10:25:12 <kmc> but also I don't recall how any of it works at all
10:25:41 <shachaf> OK, I'll give a simpler version of it than the one in that post so we can talk about how it works.
10:26:05 <shachaf> data Conat = Z | S Conat is either a natural number or infinity (disallowing bottoms).
10:27:06 <shachaf> find :: (Conat -> Bool) -> Conat is a function that either returns the smallest conat that matches the predicate, if one exists, or returns infinity.
10:27:44 <shachaf> find pred = if pred Z then Z else S (find (pred . S))
10:28:17 <shachaf> This function works by asking pred Z, pred (S Z), pred (S (S Z)), etc., and outputting a single S each time it gets a no answer.
10:28:52 <shachaf> Then you can use "exists pred = pred (find pred)" to see if any conat matches the predicate.
10:29:26 <shachaf> Since pred is total, this is guaranteed to give an answer, and pred will only ask for some finite prefix of your conat.
10:29:52 <kmc> pred is total by assumption?
10:30:05 <shachaf> Right, this whole thing only works for total predicates.
10:30:19 <cpressey> shachaf: Is this all lead-up to your ill-formed question?
10:30:27 <shachaf> (Totality is a very strong condition here.)
10:30:53 <shachaf> I mean, now I'm just explaining this thing because it's neat, to discuss other ways of framing it.
10:31:42 <shachaf> You could say, you're my counterparty, and you give me a predicate, call it p. I can ask p questions by passing you a handle to a conat, call it n.
10:31:51 <shachaf> Then you can send me questions about n, and so on.
10:33:03 <shachaf> In the end the dialog between us will look like "<- here's p, -> here's n, <- is n > 0?, -> yes, <- is n > 1?, -> no", etc.
10:33:48 <shachaf> This is a flat thing rather than a sneaky recursive structured thing. "totality" means that you'll only ask me a finite number of questions about n, and I can just look at the questions and see what the largest number you asked about is.
10:34:56 <cpressey> I am sorely tempted to claim all flat things are recursively structured (you just can't usually see the recursion because it's VERY sneaky)
10:35:45 <shachaf> I mean, sure, you can specify things with recursive structure.
10:35:55 <shachaf> I think almost everyone who sees "seemingly impossible functional programs" is confused at first.
10:36:22 <int-e> there's a wonderful impure way to do the ((Nat -> Bool) -> Bool) -> Nat -> Bool thing... you're given an interrogator (Nat -> Bool) -> Bool that interrogates a subject Nat -> Bool and comes up with a boolean answer in finite time. So you send in subjects that remember the questions they were asked... the first question will always be the same, the second depends on the first, and so on; so you...
10:36:28 <int-e> ...can reconstruct the whole tree of question this way. The mind-boggling thing is that you can do basically the same thing in a pure function.
10:36:39 <shachaf> One thing I can tell them is, "imagine you pass me a Turing machine that specifies the predicate. Then I pass that machine a Turing machine that specifies a conatural, and I can simulate it to see what it does, and so on"
10:37:01 <shachaf> int-e: I think we were just typing a similar kind of thing there.
10:37:26 <shachaf> This is yet another model of computation.
10:38:21 <shachaf> But I'd like to see something that makes the dialog explicit. There are only two parties, the exists player and the forall player or whatever you call them.
10:38:34 <wob_jonas> kmc: on random graphs => I was thinking you should use something like the delaunay triangulation of the poisson process ("http://math.bme.hu/~ambrus/pu/randvoronoi.html") to get a planar grid of cells that is isotropic
10:38:34 <wob_jonas> only you'd probably have to modify it somewhat to make the degree bounded, perhaps by turning it to 3-regular by replacing each node by a loop
10:38:51 <shachaf> If you write "((a -> b) -> c) -> d" it doesn't change the fact that b/d are one player's and a/c are the other's.
10:39:53 <wob_jonas> shachaf: "I've never even thought about cellular automata on non-planar graphs." => wait really? because Game of Life uses king neighbourhood, and that's not planar
10:40:11 <shachaf> Oh, maybe I meant something stronger than non-planar.
10:40:14 <kmc> hm, so it's not
10:40:33 <int-e> what about non-euclidean geometry
10:41:40 <shachaf> Part of the point is, if you say "forall epsilon, exists delta, forall x, ...", the person making the epsilon and x decisions is the same person.
10:42:17 <shachaf> To require them to phrase it in terms of "manufacturing a special sub-person who can make x-choices and passing that sub-person to you" is a complex and bizarre restriction.
10:43:57 <cpressey> I'd say something but tbh I've never understood what corecursion is so I'll not say anything
10:44:15 <int-e> Ehrenfeucht–Fraïssé games for programming, hmm.
10:45:15 <shachaf> I think there's a separate programming thing where APIs that are defined in terms of callbacks are sometimes much more awkward than APIs that aren't, because they restrict your flow control to happening in particular ways.
10:45:26 <shachaf> (Rather than just passing events or something.)
10:46:48 <shachaf> cpressey: I think there are probably versions of this that aren't as explicitly about corecursive structures, though maybe it's always implicit in some way.
10:47:06 <shachaf> (I mean, in the sense that functions are codata rather than data, or something.)
10:49:51 <shachaf> Here's one of the things that's usually confusing about seemingly-impossible-functional-programs:
10:50:34 <shachaf> People say "I don't see how it's possible, because I can ask pred infinity, and I can ask pred 0,1,2,3,...,n, but that doesn't tell me anything about pred n+1"
10:51:14 <shachaf> The answer is that you have to pass pred a conatural that's itself expressed in terms of pred. That's the sneaky recursive thing I was referring to.
10:52:45 <wob_jonas> cpressey: "I catch an exception only to throw a different exception. I've done this enough that in my head I call this the "exception translation antipattern"." => you mean, you make your program print sensible error messages that tell what the user did wrong, rather than some nonsense about where the error was detected like "NullPtrException in me
10:52:45 <wob_jonas> ssage.java:418", and it's an antipattern because it hurts your job security if other people can use your program?
10:53:38 <wob_jonas> shachaf "What's wrong with personifying things?" => the computers don't like when you do that
10:53:41 <cpressey> wob_jonas: It's an antipattern only in the sense that different modules define sets of exceptions that are only meaningful to them, and any time an exception crosses those boundaries, you have to "translate" it to make it meaningul
10:53:52 <shachaf> wob_jonas: You know perfectly well that's not what cpressey mean and you're not being helpful or nice when you phrase it like that.
10:54:34 <shachaf> ...That was probably an overstatement to something that was a harmless joke.
10:54:35 <cpressey> shachaf: By the part where people find this thing about Cantor space any more impossible than, say, the claim that there is no greatest even integer
10:55:18 -!- Phantom__Hoover has quit (Ping timeout: 258 seconds).
10:55:19 <cpressey> I mean, I just universally quantified over an infinite set there in claiming that, pretty spooky huh
10:55:41 <shachaf> You mean you don't see why people are confused?
10:56:05 <cpressey> Well, people are confused about a lot of things.
10:56:30 <shachaf> This is a computational question so I don't the connection to there being no greatest even integer.
10:57:12 <cpressey> A big problem here is that I don't know what a conatural is
10:57:35 <shachaf> Oh, it's an element of the one-point compactification of the naturals, if that helps.
10:57:49 <shachaf> If not: It's a monotonic function : N -> 2
10:57:52 <kmc> cpressey: do you know how inductive codata works?
10:58:14 <kmc> shachaf: there sure are a lot of ways to define the same thing, eh?
10:58:20 <shachaf> Or: It's a Turing machine that either prints some number of 1s and then halts, or keeps printing 1s forever.
10:58:30 <wob_jonas> "There are only two parties, the exists player and the forall player or whatever you call them." => I heard they were called Adam and Eve, Adam for the forall quantifiers and Eve for the exists quantifiers
10:58:48 <kmc> shachaf: but it will always print the next 1 within finite time, right?
10:59:37 <kmc> cpressey: well do you know what people mean when they say haskell has 'infinite data structures'?
10:59:47 <shachaf> i,i I guess cpressey only learned the counterexamples and not the topology
11:00:23 <cpressey> kmc: Well, I know what they *mean*, but I try not to use that term myself, if that makes sense
11:00:36 <kmc> cpressey: if you want a better term you could call them codata ;)
11:00:48 <shachaf> Haskell people are often very confusil about which things are data and which things are codata.
11:01:10 <kmc> in Haskell all 'data' structures are codata
11:01:28 <kmc> if you write data Nat = Z | S Nat
11:01:37 <kmc> then you actually defined conats
11:01:54 <kmc> because you can construct the value S (S (S (S ... to infinity
11:02:09 <cpressey> I don't see why people are surprised that you can apply one lazy thing to another lazy thing and conclude it will be true for all instances of the thing
11:02:33 <cpressey> "Every integer is either odd or even"
11:02:33 <shachaf> cpressey: Wait, which lazy thing?
11:02:46 <cpressey> If you prefer that terminology
11:03:02 <shachaf> People are confused because they can't think of an actual algorithm to compute it.
11:03:26 <shachaf> I don't think the algorithm is obvious.
11:03:52 <shachaf> (Or even the fact that it could exist.)
11:04:12 <cpressey> checking whether a total predicate holds for all elements of a set doesn't even sound like an algorithm to me, it sounds like a proof
11:04:20 <cpressey> and proofs are programs, thanks Curry, thanks Howard
11:04:43 <shachaf> Now I'm not even sure whether we're talking about the same thing.
11:05:08 <shachaf> forAll :: (Conat -> Bool) -> Bool is certainly not a proof that Bool is inhabited.
11:05:13 <lambdabot> kmc says: "Haskell is great, because Curry-Howard! Proving things in the type system. We can prove that, uh, Ints exist, unless they're ⊥."
11:05:38 <cpressey> OK, well, I'm probably talking nonsense
11:05:50 <cpressey> Still, it doesn't surprise *me*, and I'd like to know why that is
11:06:50 <shachaf> The claim is: I can write a program that takes a predicate (over the conaturals, or the Cantor set), and decides whether the predicate holds for every input.
11:07:14 <shachaf> The set is infinite, so you can't just try every input.
11:07:44 <shachaf> You're saying it's not surprising which probably means you have some model for what inputs can be exhaustively searched by an algorithm, and you think these things match that model?
11:09:06 <shachaf> (I mean, obviously it's not surprising to me now because I know how it works, but it was surprising to me until I thought about it carefully.)
11:09:30 <kmc> shachaf: I used to be a snarky little shit, eh?
11:09:30 <cpressey> I can write a proof that takes a predicate, shows that it holds for a base case, and shows that it holds for succ(x) if it holds for x, and conclude from that that it holds for all x. Does that surprise you?
11:09:34 <kmc> I mean I still do, but I used to, too.
11:09:51 <esowiki> [[Binerdy]] https://esolangs.org/w/index.php?diff=65393&oldid=49903 * YamTokTpaFa * (+84) +CATs
11:10:03 <shachaf> cpressey: Hmm, the claim I'm making holds for the conaturals (with infinity), but it certainly doesn't hold for the naturals.
11:10:21 <esowiki> [[English Binerdy]] https://esolangs.org/w/index.php?diff=65394&oldid=55887 * YamTokTpaFa * (+72)
11:10:40 <shachaf> So if the thing you're saying works for the naturals then it's probably not the thing I'm talking about.
11:10:50 <cpressey> shachaf: I'm not thinking about a thing!
11:11:15 <shachaf> OK, maybe I was extrapolating too far. Induction doesn't surprise me.
11:11:26 <shachaf> (Induction on the naturals, I mean.)
11:12:17 <esowiki> [[Darmok]] https://esolangs.org/w/index.php?diff=65395&oldid=43237 * YamTokTpaFa * (+37) +WIP +CATs
11:12:40 <esowiki> [[Forth]] https://esolangs.org/w/index.php?diff=65396&oldid=63187 * YamTokTpaFa * (+24) +CAT languages
11:13:07 <esowiki> [[Mishmash]] https://esolangs.org/w/index.php?diff=65397&oldid=54590 * YamTokTpaFa * (+9) +WIP
11:13:16 <cpressey> Cantor space may be infinite, but it has a finite description. How do you traverse an infinite thing, whether in a proof or in a program? By traversing all cases of its finite description.
11:13:51 <cpressey> That's why it doesn't surprise me.
11:14:05 <shachaf> But N also has a finite description.
11:14:09 <esowiki> [[IBNIZ]] https://esolangs.org/w/index.php?diff=65398&oldid=40608 * YamTokTpaFa * (+10)
11:14:36 <cpressey> Right, that's why I can say things like "Every integer is either odd or even" without testing every integer
11:15:21 <shachaf> OK, but you can't write a program that takes an arbitrary predicate, such as "is either odd or even", and tells you whether every natural satisfies it.
11:15:29 <shachaf> You can prove it for that specific predicate.
11:15:57 <cpressey> shachaf: I can certainly write a program that tries to prove it or refute it...
11:16:08 <shachaf> Yes, and the program might not halt.
11:16:19 <shachaf> Whereas for the Cantor set you can write the program, and it'll always halt and give you the correct answer.
11:16:42 <shachaf> (Assuming the predicate itself is total.)
11:17:11 <cpressey> The program will halt if certain conditions are met. The predicate must be total. The infinite set must have some properties that (presumably) being Cantor space gives it. Not surprising.
11:17:25 <esowiki> [[B-tapemark]] https://esolangs.org/w/index.php?diff=65399&oldid=38916 * YamTokTpaFa * (+68)
11:18:02 <cpressey> If there's something surprising, it's that being Cantor space, gives it that property.
11:18:10 <esowiki> [[Pieces]] https://esolangs.org/w/index.php?diff=65400&oldid=13796 * YamTokTpaFa * (+12)
11:18:15 <cpressey> I'm sure it doesn't hold for some other spaces.
11:18:19 <shachaf> Yes, that's the surprising thing.
11:18:34 <cpressey> But to me that's something surprising about Cantor space, not the program!
11:18:44 <esowiki> [[Hyperfunge]] https://esolangs.org/w/index.php?diff=65401&oldid=46445 * YamTokTpaFa * (+23)
11:18:48 <shachaf> I think "exhaustive search of the Cantor set is possible" is the surprising statement here.
11:19:07 <shachaf> The program shows that it's possible.
11:19:40 <shachaf> For what it's worth I still don't know exactly what the properties that make it possible are.
11:20:13 <shachaf> I know it has to do with compactness, but I'm not sure exactly what the computational content of compactness is, and how it's being used here. I only know how to write it for specific compact spaces.
11:20:43 <shachaf> I feel like "whether this fact is surprising or not" is quite a detour from the original question anyway.
11:21:03 <cpressey> Yeah, I don't know much topology, so I guess I don't officially know if it should surprise me or not?
11:21:41 <cpressey> I'm quite resigned to the fact that there are a lot of topologies with weird properties, so when someone says "Hey! Did you know that you can show X for all of Cantor space" it's not like I'm "REALLY?"
11:22:02 <cpressey> shachaf: What was the original question
11:22:33 <cpressey> shachaf: The one where you wanted to tail-call optimize Arthur and Merlin?
11:23:57 <shachaf> The Arthur-Merlin thing seems to be about computationally bounded agents whereas I was just talking about computability for now.
11:24:17 <wob_jonas> it's about one computationally bound agent, Arthur, and one unbound, Merlin
11:24:20 <cpressey> shachaf: Something like that? You wanted to flatten the conversation between two parties in... one of those things.
11:24:36 <shachaf> Yes, I'm curious about flattened conversations, sure.
11:24:54 <wob_jonas> although there are twisted versions with more than one Merlins
11:25:01 <shachaf> cpressey: Do you find it surprising that integration of computable functions on computable reals is computable?
11:27:16 <cpressey> shachaf: Ehm. Not sure. The thing that surprises me there is, you have a function and its range is computable reals and you can integrate it at all?
11:27:47 <cpressey> Isn't that, like, discontinuous?
11:28:26 <cpressey> It's a bit like saying you have a function on the rationals and you can integrate it. I suck at analysis, but I didn't think that was even valid?
11:28:32 <shachaf> Hmm, you can say it's a function that works on every real.
11:28:46 <shachaf> It can't distinguish the computable ones from the uncomputable ones, of course.
11:29:49 <wob_jonas> shachaf: I already don't understand why algebraic complex numbers form a field, despite that I was supposedly taught enough Galois theory in the university courses to have to know the proof.
11:30:01 <wob_jonas> Computable numbers are way worse than that, they have very surprising properties that are impossible to guess.
11:30:36 <wob_jonas> And like lots of different definitions that sound similar but are actually different, so you have to be careful what you use in which statement.
11:31:16 * shachaf mumbles something about the effective topos.
11:31:45 <shachaf> I feel like nothing is materially different if you just say "reals" instead. If you have an oracle for an uncomputable real, your computable function will work fine with it.
11:32:00 <Cale> wob_jonas: Wait, what's hard about those things? Where do you get stuck?
11:32:36 <Cale> Or are you just saying that you haven't thought about it recently enough to know for sure
11:33:02 <cpressey> shachaf: OK, I'll rephrase. I'm surprised that integration of *any* functions is possible *at all*.
11:33:07 <wob_jonas> Cale: for the computable reals, I definitely haven't tought much about it ever, because it seems so theoretical and I never really needed it
11:34:01 <wob_jonas> I do care a little about the practical side, as in specific algorithms that are either useful in real life or close to useful, but not the abstract stuff
11:34:03 <Cale> wob_jonas: To say that computable reals are a field is basically saying that the field operations are computable.
11:34:09 <shachaf> OK, that's reasonable enough.
11:34:50 <wob_jonas> Cale: yeah, that in particular isn't too hard, but there are other questions you can ask
11:38:42 <cpressey> shachaf: Gabriel's Horn surprises me.
11:39:12 <cpressey> I mean, I don't doubt that integration is a valid concept and all, but, damn.
11:42:05 <wob_jonas> For the algebraic numbers, I think I understood enough about that at one point (even if I didn't understand all of Galois theory), but has forgotten how it works since.
11:43:08 <wob_jonas> These days, all that stuff I hear from algebraic geometers on the internet just scares me away.
12:14:27 -!- Vorpal has quit (Ping timeout: 248 seconds).
12:43:31 -!- xkapastel has joined.
13:23:27 <cpressey> I could start talking about codata, but if I start it could just go on forever
13:24:30 <cpressey> I daresay I have distinct finitist and formalist leanings
13:42:29 <esowiki> [[Logical/Interpreter]] https://esolangs.org/w/index.php?diff=65402&oldid=53265 * YamTokTpaFa * (+30)
13:43:48 <esowiki> [[QuineLang]] https://esolangs.org/w/index.php?diff=65403&oldid=59404 * YamTokTpaFa * (+23)
14:16:21 <esowiki> [[Hello world program in esoteric languages]] https://esolangs.org/w/index.php?diff=65404&oldid=64910 * A * (+60) /* Grin */
14:16:56 <esowiki> [[Hello world program in esoteric languages]] https://esolangs.org/w/index.php?diff=65405&oldid=65404 * A * (+28) /* Gulp */
14:30:17 -!- unlimiter has joined.
14:38:50 -!- MDude has joined.
14:43:43 -!- unlimiter has quit (Quit: kthxbye).
14:57:19 -!- Sgeo_ has joined.
14:58:24 -!- cpressey has quit (Quit: A la prochaine.).
15:01:02 -!- Sgeo__ has quit (Ping timeout: 268 seconds).
15:07:23 -!- Sgeo__ has joined.
15:10:36 -!- Sgeo_ has quit (Ping timeout: 258 seconds).
15:19:13 -!- Sgeo has joined.
15:21:46 -!- Sgeo__ has quit (Ping timeout: 246 seconds).
15:23:13 <esowiki> [[Special:Log/newusers]] create * ZSwifty * New user account
15:23:22 -!- Sgeo_ has joined.
15:26:44 -!- Sgeo has quit (Ping timeout: 258 seconds).
15:55:54 -!- ais523 has joined.
15:56:11 -!- wob_jonas has quit (Remote host closed the connection).
15:56:21 <ais523> <cpressey> Java's attempt to build an effect system around exceptions feels like an attempt to make it more like lexical scope. Thing is, Java programmers tell me they hate it and they just end up using unchecked exceptions instead. ← this problem arises in Java almost entirely as a result of checked exceptions that you know statically can never occur, but still exist in the signature
15:59:46 <ais523> a simple example is «string.getBytes("UTF-8")» which according to the type system can throw a checked exception (because the type system can't see that "UTF-8" is a literal string and thus always names a valid character set), the checked exception would be necessary if the "UTF-8" were a string specified by the user
16:01:14 <ais523> meanwhile, «string.getBytes(Charset.forName("UTF-8"))» doesn't throw checked exceptions (because for some reason, Charset#forName uses an unchecked exception if the charset name is unrecognised)
16:02:06 <ais523> and «string.getBytes(StandardCharsets.UTF_8)» is a workaround for the whole mess that only became available fairly recently
16:02:28 <ais523> I don't think any of this is an argument against checked exceptions, but I do think it's an argument for doing constant-folding before type-checking
16:03:24 <ais523> fwiw, this issue isn't specific to checked exceptions, it happens with other forms of error handling too
16:03:47 <ais523> e.g. in Rust you need to explicitly convert errors to panics with «unwrap» in cases where you know they can't possibly happen, and yet that removes some of the static safety guarantees of the language
16:04:34 <ais523> after programming in Java seriously for months, I ended up in favour of checked exceptions (or at least, explicitly enumerated error cases) and against the way Java treates checked exceptions
16:05:50 <ais523> that said, I see very little difference between Java and Rust error handling, the only difference is a minor syntactic one (Java propagates exceptions by default and requires try…catch to convert them to return values, Rust treats errors as return values by default and requires ? to propagate them, but in either case the only difference is the syntax at the call site)
16:05:51 -!- Sgeo__ has joined.
16:09:01 -!- Sgeo_ has quit (Ping timeout: 246 seconds).
16:12:35 <HackEso> automatic squirrel feeder:Automatic squirrel feeders are just feeders in the category of automatic squirrels. Taneb invented them. \ bureaucracy:Bureaucracy (from French bureau, "burrow") is a political system in which squirrels rule the nation, and burrow their nuts. \ nutella:Nutella is a nutty substance. Taneb invented it for use in his automatic squirrel feeders. \ squirrel:A squirrel is a small nut-harvesting unit frequently deployed all over the worl
16:13:07 <HackEso> A squirrel is a small nut-harvesting unit frequently deployed all over the world. They are popular due to their usefulness in distracting dogs.
16:13:24 <Taneb> `? automatic squirrel
16:13:25 <HackEso> automatic squirrel? ¯\(°_o)/¯
16:15:14 <int-e> Taneb: I didn't expect to get *two* T-ventions.
16:19:17 <Taneb> int-e: automatic squirrel feeders were the first I believe
16:19:21 <Taneb> I hadn't seen nutella before
16:22:41 <Taneb> Well, I've seen the spread, just not the wisdom entry
16:22:50 <Taneb> I'm not a huge fan
16:23:00 <Taneb> (of the spread, the wisdom entry's OK)
16:23:31 -!- ais523 has quit (Ping timeout: 248 seconds).
16:29:46 <esowiki> [[AutoColdKey]] N https://esolangs.org/w/index.php?oldid=65406 * A * (+210) Midnight creation
16:33:13 <esowiki> [[AutoColdKey]] https://esolangs.org/w/index.php?diff=65407&oldid=65406 * A * (+123) Now it is a stub.
16:34:52 -!- Sgeo_ has joined.
16:35:45 -!- andrewtheircer has joined.
16:37:43 -!- Sgeo__ has quit (Ping timeout: 246 seconds).
16:43:16 -!- xkapastel has quit (Quit: Connection closed for inactivity).
16:45:36 -!- xylochoron[m] has quit (Read error: Connection reset by peer).
16:45:40 -!- wmww has quit (Read error: Connection reset by peer).
16:45:47 -!- ivzem[m] has quit (Remote host closed the connection).
16:45:49 -!- tswett[m] has quit (Write error: Connection reset by peer).
16:47:53 <andrewtheircer> smaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
16:53:55 -!- wmww has joined.
17:07:03 <esowiki> [[EPARM]] https://esolangs.org/w/index.php?diff=65408&oldid=16949 * YamTokTpaFa * (+24) /* More ideas */ +CAT
17:11:20 -!- xkapastel has joined.
17:12:24 -!- Sgeo_ has quit (Read error: Connection reset by peer).
17:12:50 -!- Sgeo_ has joined.
17:16:13 -!- xylochoron[m] has joined.
17:16:13 -!- tswett[m] has joined.
17:16:22 -!- ivzem[m] has joined.
17:20:43 <int-e> andrewtheircer: Look if you want to strike up a conversation here, you need to try a little harder. Drop an interesting idea (programming language or computation related preferrably), be articulate, and be prepared to wait minutes to hours for a reply (if any). What you're doing is making you come across stupid and obnoxious.
17:24:39 -!- b_jonas has joined.
17:26:38 <HackEso> olist 1174: shachaf oerjan Sgeo FireFly boily nortti b_jonas
17:28:22 <andrewtheircer> i heard this idea from another person: an eso where you can change the speed delta but not overwrite it
17:28:40 <andrewtheircer> you need to tuuuurn slowly until you get to face right
17:29:03 <andrewtheircer> the main storage of this eso *is* the speed delta (velocity)
17:30:26 <andrewtheircer> the initial tape is set to (0,0)(1,0)(0,0) where the first set of 0,0 is position and all the ones after (1,0) are speed delta deltas
17:31:36 <andrewtheircer> there is an integer called the "meta-level" of the delta you are manipulating
17:32:24 <andrewtheircer> to say again: this idea is not mine, it originated from reconcyl#4042 on the esolangs discord
17:38:19 -!- Phantom__Hoover has joined.
17:42:31 -!- andrewtheircer has quit (Remote host closed the connection).
17:44:59 -!- unlimiter has joined.
17:49:10 -!- unlimiter has quit (Client Quit).
18:24:29 -!- Sgeo__ has joined.
18:28:15 -!- unlimiter has joined.
18:28:15 -!- Sgeo_ has quit (Ping timeout: 264 seconds).
18:33:15 -!- unlimiter has quit (Quit: WeeChat 2.5).
18:40:51 -!- Sgeo_ has joined.
18:43:47 -!- Sgeo__ has quit (Ping timeout: 245 seconds).
19:26:27 <HackEso> Morphology is the theory that you can never have enough phở. boily invented it.
19:26:38 <HackEso> The second wisdom is that wisdom can never be complete or consistent.
19:31:52 <HackEso> 57) <fungot> ehird: every set can be well-ordered. corollary: every set s has the same diagram used from famous program talisman with fnord windows to cascade, someone i would never capitalize " i"
19:52:19 -!- Phantom__Hoover has quit (Ping timeout: 246 seconds).
20:01:30 -!- Phantom__Hoover has joined.
20:12:43 -!- Lord_of_Life_ has joined.
20:15:21 -!- Lord_of_Life has quit (Ping timeout: 258 seconds).
20:15:36 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
20:16:52 <zzo38> Glulx has a frame pointer, but it points to an address space that you cannot read from or write into.
20:53:15 -!- xkapastel has quit (Quit: Connection closed for inactivity).
20:58:22 -!- FreeFull has joined.
21:00:37 -!- MDead has joined.
21:01:13 -!- MDude has quit (Read error: Connection reset by peer).
21:01:18 -!- MDead has changed nick to MDude.
21:30:10 -!- ivzem[m] has quit (Quit: Idle kick: User has been idle for 23+ days.).
22:05:54 -!- Sgeo_ has quit (Read error: Connection reset by peer).
22:06:22 -!- Sgeo_ has joined.
22:28:40 -!- xkapastel has joined.
22:42:21 -!- Sgeo__ has joined.
22:46:00 -!- Sgeo_ has quit (Ping timeout: 258 seconds).
22:53:33 -!- Xunie has joined.
23:36:46 <esowiki> [[Keg]] https://esolangs.org/w/index.php?diff=65409&oldid=65033 * JonoCode9374 * (+45) /* External Resources / Reference Implementation */
23:48:59 -!- unlimiter has joined.