00:30:40 [[Special:Log/newusers]] create * PrecognizantWaffles * New user account 00:35:02 [[Esolang:Introduce yourself]] M https://esolangs.org/w/index.php?diff=159648&oldid=159639 * PrecognizantWaffles * (+180) /* Introductions */ 00:55:07 -!- amby has quit (Quit: so long suckers! i rev up my motorcylce and create a huge cloud of smoke. when the cloud dissipates im lying completely dead on the pavement). 00:58:57 [[Special:Log/upload]] upload * PrecognizantWaffles * uploaded "[[File:Order of operations example.png]]" 01:02:10 [[Special:Log/upload]] upload * PrecognizantWaffles * uploaded "[[File:Hello world example.png]]" 01:03:53 [[Special:Log/upload]] upload * PrecognizantWaffles * uploaded "[[File:Factorial example.png]]" 01:13:27 [[User:PrecognizantWaffles/Sandbox]] N https://esolangs.org/w/index.php?oldid=159652 * PrecognizantWaffles * (+4319) Created page with "Calcu-less 2 is a language built around integrals. Programs are made up of nested integrals, with the bounds and functions as inputs, and the differential as the command instruction. The end result should be one giant integral that c 01:16:05 [[User:PrecognizantWaffles/Sandbox]] M https://esolangs.org/w/index.php?diff=159653&oldid=159652 * PrecognizantWaffles * (-4) /* Fractions as Input */ 01:19:07 [[User:PrecognizantWaffles/Sandbox]] https://esolangs.org/w/index.php?diff=159654&oldid=159653 * PrecognizantWaffles * (+169) 01:21:17 [[Calcu-less 2]] N https://esolangs.org/w/index.php?oldid=159655 * PrecognizantWaffles * (+4484) Created page with "Calcu-less 2 is a language built around integrals. Programs are made up of nested integrals, with the bounds and functions as inputs, and the differential as the command instruction. The end result should be one giant integral that can be calculated to 02:15:25 -!- ais523 has quit (Quit: quit). 02:15:40 [[Special:Log/newusers]] create * Wilber * New user account 02:19:49 [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=159656&oldid=159648 * Wilber * (+160) 02:28:09 [[GameState]] N https://esolangs.org/w/index.php?oldid=159657 * Wilber * (+7843) Created page with " = GameState = == Introduction == '''GameState''' is an esolang inspired by classic video game mechanics created by Wilber Escobar in 06/2026.
The core idea behind this language is to simulate a video 02:39:36 [[Tiny]] https://esolangs.org/w/index.php?diff=159658&oldid=159121 * Ron.hudson * (-2032) Announcing Newtiny V0.0100 02:50:13 [[Tiny]] https://esolangs.org/w/index.php?diff=159659&oldid=159658 * Ron.hudson * (+133) 03:47:28 -!- Lord_of_Life has quit (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine). 03:49:23 -!- Lord_of_Life has joined. 05:00:09 -!- Lord_of_Life has quit (Ping timeout: 260 seconds). 05:02:11 -!- Lord_of_Life has joined. 05:36:51 [[~ATH implementation attempt]] N https://esolangs.org/w/index.php?oldid=159660 * TheMCoder * (+823) Created page with "This is my attempt at making ~ATH via python. === My Code === import psutil import argparse import string command = "" parser = argparse.ArgumentParser() parser.add_argument("file", type=str) parser.parse_args() file = open(parser.parse_args().fil 05:39:51 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159661&oldid=159660 * TheMCoder * (+80) My attempted implementation of ~ATH 05:42:52 [[User:TheMCoder]] https://esolangs.org/w/index.php?diff=159662&oldid=135139 * TheMCoder * (+114) 05:45:17 [[~ATH implementation attempt]] M https://esolangs.org/w/index.php?diff=159663&oldid=159661 * TheMCoder * (+96) /* My Code */ 05:47:30 [[User talk:/w/wiki/index.php/Talk:index.php/Main page]] https://esolangs.org/w/index.php?diff=159664&oldid=159439 * None1 * (+63) 05:53:21 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159665&oldid=159663 * TheMCoder * (+530) 05:54:00 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159666&oldid=159665 * TheMCoder * (-6) 05:54:20 [[~ATH implementation attempt]] M https://esolangs.org/w/index.php?diff=159667&oldid=159666 * TheMCoder * (+0) 05:56:27 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159668&oldid=159667 * TheMCoder * (+146) /* Examples */ 06:02:45 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159669&oldid=159668 * TheMCoder * (+275) /* My Code */ 06:02:54 -!- Sgeo has quit (Read error: Connection reset by peer). 06:03:23 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159670&oldid=159669 * TheMCoder * (+1) /* My Code */ 06:03:37 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159671&oldid=159670 * TheMCoder * (+2) /* My Code */ 06:03:49 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159672&oldid=159671 * TheMCoder * (+1) /* My Code */ 06:09:11 [[~ATH implementation attempt]] M https://esolangs.org/w/index.php?diff=159673&oldid=159672 * TheMCoder * (-2) /* My Code */ 06:12:11 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159674&oldid=159673 * TheMCoder * (+48) /* My Code */ 06:18:29 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159675&oldid=159674 * TheMCoder * (+18) 06:18:42 [[Sixtyfeetunderassembly]] https://esolangs.org/w/index.php?diff=159676&oldid=135068 * TheMCoder * (-15) 06:28:57 [[~ATH implementation attempt]] https://esolangs.org/w/index.php?diff=159677&oldid=159675 * TheMCoder * (+146) /* My Code */ 06:46:17 -!- tromp has joined. 06:58:54 -!- chiselfuse has quit (Remote host closed the connection). 06:59:10 -!- chiselfuse has joined. 08:20:29 -!- Everything has joined. 08:56:20 [[GameState]] https://esolangs.org/w/index.php?diff=159678&oldid=159657 * Stkptr * (-194) 2026?? 08:57:00 [[Calcu-less 2]] https://esolangs.org/w/index.php?diff=159679&oldid=159655 * Stkptr * (+53) 09:04:36 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 09:56:25 Hi * 10:02:49 [[Talk:WhatLang]] M https://esolangs.org/w/index.php?diff=159680&oldid=159550 * UrnEn * (+145) /* whatlang with six kinds of symbols is tc too! */ 10:27:52 [[User talk:YufangTSTSU]] https://esolangs.org/w/index.php?diff=159681&oldid=158520 * None1 * (+373) 10:28:26 [[User talk:YufangTSTSU]] M https://esolangs.org/w/index.php?diff=159682&oldid=159681 * None1 * (+7) 11:03:08 -!- amby has joined. 11:39:22 [[UE1]] https://esolangs.org/w/index.php?diff=159683&oldid=150869 * B jonas * (+90) links 12:11:04 -!- wib_jonas has joined. 12:12:20 zzo38: you asked about UE-1 earlier. https://github.com/Nakazoto/UEVTC/blob/main/UE1/Software/Emulator/UE1E_BINARY.BAS has an emulator with mostly readable source code, so you can read that if you want to figure out what the computer can do. I'm trying to read it right now. the same repository has some other potentially useful info, mostly about 12:12:20 the hardware implementation. 12:13:29 also Usagi Electric has declared the computer as complete and working, and it seems he might be planning to make a second vaccum tube homebrew computer using the experienced that he got from learning this first one 12:21:08 [[User:I am islptng/Sandbox]] https://esolangs.org/w/index.php?diff=159684&oldid=159635 * Hotcrystal0 * (+56) 12:24:07 [[User:Hotcrystal0/My esolang ideas]] https://esolangs.org/w/index.php?diff=159685&oldid=152948 * Hotcrystal0 * (+0) 12:27:19 [[List of ideas]] https://esolangs.org/w/index.php?diff=159686&oldid=159641 * Hotcrystal0 * (+145) /* Partially Silly Ideas */ 12:41:23 [[Python is Magic/Constants]] https://esolangs.org/w/index.php?diff=159687&oldid=141303 * PkmnQ * (+373) Finally rework 13:00:12 -!- wib_jonas has quit (Quit: Client closed). 13:21:30 [[FrainBuck--]] https://esolangs.org/w/index.php?diff=159688&oldid=115337 * Kaveh Yousefi * (+455) Introduced an examples section which comprehends as its incipial members a letter output program and a bouncing printer. 13:23:15 [[FrainBuck--]] https://esolangs.org/w/index.php?diff=159689&oldid=159688 * Kaveh Yousefi * (+214) Added a hyperlink to my implementation of the FrainBuck-- programming language on GitHub. 13:44:07 [[User talk:Gilbert189]] https://esolangs.org/w/index.php?diff=159690&oldid=155188 * Hotcrystal0 * (+272) 14:04:15 -!- b_jonas has quit (Ping timeout: 252 seconds). 15:10:03 -!- ais523 has joined. 16:02:44 -!- Everything has quit (Quit: leaving). 16:10:24 -!- impomatic has joined. 16:27:09 -!- impomatic has quit (Quit: Client closed). 16:40:39 -!- impomatic has joined. 17:01:18 -!- b_jonas has joined. 17:02:26 -!- Raoof has joined. 17:08:50 hello all again. I came up with an early prototype of my language here https://raoofha.github.io/r/r.html (it's a simple text editor with a run button and error reporting) I appreciate your feed back. I'm interested to know whether you can write a loop with this language 17:13:29 Fun. FWIW it looks like the Node script isn't being run server-side; I get a glitchy page with some broken text. 17:15:18 korvo only test it on chromium, firefox ignore line break 17:16:38 there is no server it's all offline, you can save the file and run it by "node r.html arg1 arg2 arg3 ...." 17:27:31 I didn't realise node could run HTML files 17:28:40 ais523 it's not html, I used some trick and commented the html tags 17:34:10 korvo have you test it out ? what browser are you using ? 17:34:37 Raoof: I'm using Firefox. I looked at the source and it looks alright. Where are you headed with this language? 17:35:06 -!- Raoof has quit (Quit: Client closed). 17:35:25 -!- Raoof has joined. 17:37:33 it is my practical model of computation that you can teach to kids or adults 17:40:39 It's just primitive recursive functions, right? It's not Kleene's style, but it's using the tower of hyperoperators. 17:45:35 korvo I believe (I don't have any proof yet because a self-interpreter takes a lot of time to write) it can compute all total computable functions, but you might disagree I guess ? 17:48:11 -!- impomatic has quit (Quit: Client closed). 17:52:17 Raoof: Yeah. Kleene would disagree too. Diagonalization should apply here. 18:00:29 korvo what is the set of functions that this language can compute ? it is not the set of primitive recursive functions because it can compute 'hyp' 18:05:46 Raoof: Probably primitive recursive functionals, also called higher-order primitive recursive functions. Not sure though. The corresponding class sits between PR and R; it's not complete, but it's very powerful. 18:06:18 My language Cammy has that class, for example. 18:07:14 I'm pretty sure there are computable functions that are total, but can't be proven to be total 18:08:44 or, you can look at concrete examples like this Turing machine: https://bbchallenge.org/1RB2LC1RC_2LC---2RB_2LA0LB0RA 18:08:45 Yeah, in the sense that they can be expressed in a Turing machine but not by mere composition of Kleene's functions. 18:09:25 it is currently believed that it probably halts when executed, but runs for too long to simulate with current hardware and CS knowledge, so we don't know how long it runs for or even whether the suspicion that it halts is correct 18:09:59 say it is total, how do you express it in a provably total programming language without first executing it to see when it stops? 18:11:32 Oh, it's Bigfoot. Yeah, Bigfoot "probviously" halts (JH Conway's word for it); we have good evidence that it ought to halt, but no formal proof. 18:12:51 korvo: that isn't Bigfoot 18:12:58 Bigfoot probviously doesn't halt, this is one that probviously does 18:13:20 -!- impomatic has joined. 18:14:26 Ah, whoops. I should have read more carefully. 18:16:05 Speaking of reading carefully, I can't actually find the statement "there is a total computable function which can't be expressed with Kleene's first PCA". It's neither a corollary of Kleene's Parameter nor Recursion theorems. It's not equivalent to Gödel's First Incompleteness either. 18:17:46 But it's an example of a diagonal argument, IIRC. But it's not in any of the lists of diagonal arguments. Maybe I've hallucinated it. 18:18:17 I think the usual diagonal argument doesn't work 18:18:31 there might be an unusual one, though 18:20:23 ...Wait, Kleene's first PCA isn't Kleene's PRFs. I've made the same mistake as nLab, which calls their page "partial recursive function" and only discusses PRFs as a special case. 18:21:53 Found a copy of the argument. It has no citations, so I don't know who it comes from, but I think it's part of Kleene's proof of Gödel's Incompleteness. https://en.wikipedia.org/wiki/Primitive_recursive_function#Limitations 18:23:02 Consider PRFs of one argument. Use Gödel numbering to encode them as numbers. Define an evaluator function of two arguments: a number, and a PRF encoded as a number, s.t. the evaluator does Gödel evaluation. Then diagonalize to show that the evaluator isn't PRF. 18:26:17 Oh! I recognize this proof. It's the proof that total self-interpreters don't occur. Raoof, this is probably what you wanted. 18:38:13 korvo I believe Diagonalization is a mistake that we all should put a side. (I have an argument for my view if you are interested) 18:38:46 Raoof: Well, I believe in Lawvere's fixed-point theorem, so we're not likely to agree there. Diagonalization is an inevitable feature of Cartesian closed categories. 18:40:34 Also I believe that the folklore about total self-interpreters is wrong, or at least badly phrased. There was a paper in 2016 that challenged the lore and refined exactly what is possible: http://compilers.cs.ucla.edu/popl16/popl16-full.pdf 18:42:01 ais523: your statement sounds wrong. if that Turing machine (without input) halts then of course it can be proven to halt, we just don't have a short enough proof. 18:43:03 now you could construct a turing-machine that takes input and halts on all inputs but can't be proven to halt on all inputs, but you need to quantify on more than finitely many possible inputs for that 18:44:35 Raoof: Okay, I am interested though. What's your thought? 18:49:24 I believe there is a total and sound but [maybe] not knowably sound turing machine that solves the halting problem because if you put the diagonal machine 'd1(n)=1+u(n,n)' or 'd2(n)=if h(n,n) then loop else 1' into this equation 't(m,n)=h(m,n)*u(m,n)' (t is a total Universal Turing Machine, u is a UTM and h is a halting decider) you don't get a 18:49:25 contradiction, in another words ... 18:50:07 Raoof: nice, looks like you're proposing a specific and implemented programming language now, that's definitely an improvement over the underspecified statement that you brought last time 18:50:13 b_jonas: it has to take input for the statement to be correct I think 18:50:22 otherwise, yes, there is a proof that simply specifies the expected running time of the program 18:51:48 ais523: yes, or a full execution trace depending on what kind of proof you allow 18:52:35 meanwhile, I've been having a bit of a crisis with my Rust scoped generics thing after unexpectedly realising that they have to be Sync in order to work properly 18:53:29 Raoof: You'd have to get rid of one of the structural assumptions of Turing machines. (1) Tapes can encode single bits; tapes can encode natural numbers. (2) Everything computable is enumerable; we're only working with countable infinity at most. These two seem inarguable. 18:53:33 the idea is that you can send a *type* to another thread without sending any values of that type (by mentioning the type in a way that doesn't impact Send-ness), and then calling `default` or the like on the type to get at a value 18:54:05 ais523: that doesn't sound like too big a restriction given the restrictions that you already have 18:54:09 and if you combine this with scoped generics it lets you send values between threads without doing anything that looks like you're sending the value to the type system 18:54:37 (3) is Gödel encoding. (4) says that every computable function is represented by a set of Turing machines. 18:55:01 it already has to be Copy or possibly a shared reference, right? 18:55:04 b_jonas: it's a bigger restriction than I thought it was going to be, even for immutable things – lots of the cases where I practically want to use this are shared references that contain Cells 18:55:15 err, that reference things that contain Cells 18:55:18 those are Copy but not Send 18:55:18 Raoof: Under these four assumptions, Halting is a theorem; it's an instance of Lawvere's fixed-point. See p11-12 of https://arxiv.org/abs/math/0305282 for the diagram. 18:55:55 and of course you can use the same sort of trick to split a mutable reference between threads, which isn't allowed 18:58:07 like, a good way to think about this is that say you want to have a scoped generic that references the allocator you're using, that has to be either a mutable reference, or else the allocator has to use cells to be able to allocate through a shared reference, and neither shares between threads well (you would need to have some sort of lock around the allocator, losing considerable performance in the process) 18:58:21 Raoof: I agree with you that it would be *consistent* if there were a machine that solved Halting. It would redefine quite a bit of what we mean by "machine" and "halting" in the first place. But that would require either removing one of the four assumptions, redefining the essentials of Turing machines, or disproving Lawvere's theorem. 19:01:39 "send a *type* to another thread without sending any values of that type" => but doesn't Rust already stop that with the lifetime system, like you can't send a *type* with a limited lifetime to another thread this way, only a type that is 'static ? 19:01:39 korvo (... I think MRDP theorem implies that R = {f| y=f(x) iff ∃y[E(y,x)=0]} so if we can isolate y in E(y,x)=0 then every partial function can be made total) my problem with all theorems, arguments or proofs of undecidability of halting problem is that they all implicitly use a total universal function instead of a partial function 19:02:38 b_jonas: so this is true with lifetimes, but doesn't apply to other correctness mechanisms like Send and Sync 19:03:17 well, it's probably true with lifetimes, at least – my attempt to make a type that mentioned a type with a lifetime but didn't have any dependence on that type at all failed, but there may be other attempts that work 19:05:48 so is it not possible to prove that sending just a type with a limited lifetime would make the Rust thread library unsound even without scoped generics? 19:06:06 this sounds like something we could ask about Rust even without defining scoped generics and the Rust folks could tell 19:06:21 b_jonas: I was able to prove a race condition issue but can't prove a temporal safety issue 19:06:48 a race condition issue with what? 19:06:48 Rust seems to consider types with lifetime parameters to not be 'static even if they're contravariant or don't mention the lifetime parameter at all 19:07:04 b_jonas: scoped generics that aren't Send/Sync as appropriate 19:07:36 the other interesting type that works like that is Unpin but I suspect that one's probably OK 19:07:46 Raoof: (3) and (4) don't mind if the function is partial. They only care that it is computable in the sense that we can write down an algorithm for it, and a Gödel number for that algorithm. 19:07:55 to be honest I never looked at the details of how the Rust thread library works and how it uses Send/Sync to avoid problems 19:08:37 you'd have to make it so that a type that even mentioned a non-Send scope generic isn't Send, but that contradicts how Rust works at the moment 19:08:41 * scoped generic 19:09:20 it doesn't even need unsafe code (or indirect unsafe code from the standard library) 19:09:44 pub trait UseGenericParameters { type Unit; } impl UseGenericParameters for T { type Unit = (); } struct Useless(::Unit); 19:10:11 Useless is just a newtype on () that mentions T, but it takes its sendness/syncness from () 19:10:50 and this is pure language-Rust without any dependency on std/alloc/core 19:16:06 korvo I don't see the point of Godel numbers when you are modeling computation why not model the actual computers and use ASCII/binary string 19:16:39 a Gödel number is just a way of interpreting an ASCII/binary string in such a way that you can prove things about it 19:17:22 Raoof: We can use any encoding that has the same properties that made Gödel encoding useful. I think that ASCII with a dedicated end marker would work, for example, but that would require writing a parser with PRFs. 19:18:50 One must keep in mind that Gödel and Kleene were writing a decade before EBCDIC and several decades before ASCII. 19:21:23 ais523 what do you mean exactly by 'prove' ? are you referring to Peano Arithmetic ? 19:22:25 Raoof: no, just regular mathematical proofs – we want to prove things about programs, and do that by saying that the programs can take other programs as input; but the programs are defined to take numbers as input, so we prove that programs can be represented as numbers (and thus can be taken as input by other programs) 19:24:12 Indeed, under the hood, a Turing system is a set of numbers (usually the natural numbers) and a collection of partial rules for decoding those numbers into various types: numbers, bits, functions on various types, ... 19:25:49 And when we say that the decoding is "Gödel", we just mean that the corresponding encoders satisfy the obvious laws. In particular we mean that encoding then decoding is like doing nothing; decode(encode(X)) == X. 19:28:22 [[User:GreenThePear/Sandbox]] https://esolangs.org/w/index.php?diff=159691&oldid=155041 * GreenThePear * (-14) nicer to code stdin like this 19:33:26 I have to go now, I have a lot more to say but it gets philosophical. thank you all for your feedback, if you are interested in my language and my idea that it is total and turing complete please reach me at my github 19:33:33 No worries. Peace. 19:34:26 bye 19:34:33 -!- Raoof has quit (Quit: Client closed). 19:36:56 I feel for Gödel deniers, but mostly I wish that I could understand their intuition so that I could address it directly. 19:37:51 -!- sprock has quit (Ping timeout: 276 seconds). 19:38:02 There's no surjection from 3 to 3 → 2 because the latter has cardinality 8. Indeed, there's no surjection from 4 to 4 → 2, etc. So why expect that there's a surjection from N to N → 2? 19:38:50 -!- sprock has joined. 19:40:31 -!- Everything has joined. 19:41:14 I guess it really does go along with denying Cantor's discovery that there are multiple infinite cardinalities. But a computer scientist isn't really harmed by working with finite sets and finite functions, so it's still a workable perspective. 19:49:54 cu 20:03:49 korvo: There's no surjection from 3 to 3+1 or from 4 to 4+1, but there is a surjection from N to N+1. I think it's reasonable to expect infinite things to behave differently. 20:05:44 shachaf: Sure, that's fair. I guess it just feels regressive to me. Infinite things have to be *proven* to behave differently; I didn't believe N covers N + 1 in grade school at first. 20:06:46 Hilbert's Hotel always seemed like a "just-so" story: a story that we tell ourselves in order to justify something that we don't understand. 20:08:32 ais523: ok, I don't understand how you could smuggle the type to another thread. if you try to call default you have to be able to name the type (even if you don't explicitly write the name), and if your type mentions a const generic then you can only name it where it's in the dynamic scope, eg. you can't name it in an inner lambda that could escape from the dynamic scope. 20:09:08 it seems like even if you can make a type that's supposedly Send, you can't actually use that type in the wrong place 20:19:39 -!- Everything has quit (Quit: leaving). 20:21:55 b_jonas: the point is that the other thread *can* name the type, you just create a Send type that names it and send that 20:22:18 it is possible to have a Send type that names a non-Send type 20:25:05 ais523: but how do you send the type? the program still has to typecheck so you can only send a value of a specific type named both where you send and where you receive 20:25:28 eg. you could send a value of type T in a static Mutex 20:25:59 but you can't declare a static as Mutex if T depends on a const generic because there's no const generic in scope in the top level where you declare the static 20:26:32 b_jonas: it doesn't have to be a static Mutex, you can just provide the Mutex as an argument to the thread creation call 20:26:56 either by limiting the lifetime of the thread to shorter than the lifetime of the mutex, or Box::leak-ing the mutex so that it lives for the rest of the program duration 20:27:39 alternatively, you can send, e.g., a Useless by value, avoiding lifetime issues, and then get at the type T by pattern-matching against Useless in a blanket trait definition 20:28:01 impl UselessArg for UselessArg { type Arg = T: }, that sort of thing 20:30:01 what do you do with the Box::leaked mutex? 20:30:19 give it to the thread you're creating as, e.g., a closure capture 20:30:31 err, give a reference to it, you don't move it 20:31:14 actually I think that doesn't work because you can't leak a mutex unless it contains a 'static value 20:31:25 but the Useless-by-value technique would still work 20:32:07 (it would, however, need scoped rather than regular threads in order to weaponise it into undefined behaviour, because scoped generics can't have a 'static lifetime) 20:39:59 ais523: I don't think this can work. if your closure captures something then the type of the closure will mention the type of that capture. If you could somehow erase that from the type of the closure and assign it to a global variable with a fixed type then, even without involving threads at all, you could leak a reference to a local variable in that closure. 20:41:26 b_jonas: my point is that type of a closure to mention something that isn't Send, but the closure itself can still be Send 20:41:44 and if you combine that with scoped generics, you can send the value of the scoped generic that way even if it isn't actually Send 20:42:01 ais523: hold on, do you think it should be possible to get unsoundness this way without starting a new thread inside the scope? 20:42:02 *the type of a closure can mention something that isn't Send 20:42:13 s/should/would/ 20:43:30 I think some sort of multithreading that works on non-'static things is probably necessary (the Send implementaitons being wrong probably doesn't matter without multithreading or async signals, and scoped generics cannot be 'static so they can't be mentioned by anything that only works on 'static things) 20:43:42 I think it's not a problem in itself that you can use a type for the closure starting type that is Send but mentions a type that isn't Send inside type parameters. 20:43:48 I suspect it wouldn't be limited to specifically the std scoped threads mechanism, though 20:44:05 As in that should be possible but doesn't alone mean you can use that for unsoundness. 20:44:06 right, you can do that in current Rust without issue and it's even useful 20:44:50 scoped generics introduce an unsoundness because you can use, say, an implementation of Default on the non-Send type you sent and get at the same value that was used to create the scoped generic on another thread 20:45:05 without scoped generics, you can't do that because Default would necessarily create a new object rather than reusing an existing one 21:02:18 -!- tromp has joined. 21:03:06 this still feels like you can get unsoundness this way only if you can also get unsoundness without threads or Send involved at all. like if you could start a thread this way then you could also just leak a Box from your scope with a method that calls default, and the method table in that would reference your const generic. but if you try this the lifetimes will stop you, no matter whether you try 21:03:12 with dyn or a closure. you can erase the non-Send-ness but you can't erase the lifetime. 21:04:57 I was aware of the dyn issue earlier 21:06:09 I guess one way to think about it is this: one potential view of a scoped generic is as a lifetime that has a value – so this is basically changing things so that lifetimes themselves can be !Send or !Sync, which isn't possible currently 21:08:06 can't you use dyn to implement a type eraser similar to C++ std::function, so you can leak a Fn() closure wrapped as a fixed type box regardless of the original type of the closure, right? and then you can call that closure even if it captures a value with a type that is scoped. but if you try this with const generics then rust should stop you by making it impossible to erase the lifetime from the type 21:08:12 of the closure, so the type eraser wrapper will require that your closure is 'static, and the rules of your const generic extension will be such that if the closure has to capture the virtual method table for Default that references your stack then the closure will have a lifetime restricted to your scope. 21:08:53 no, I still don't think Send or threads is relevant here, and if this is unsound then it's unsound without threads or Send 21:09:14 with scoped threads the trick is that the starting function of the thread has to be 'static 21:09:51 you can make the type Send but you won't be able to make it 'static and still leak a type that needs to reference your reference scoped generic 21:09:52 that isn't true for scoped threads, the whole point of scoped threads is that you can have a non-'static starting closure 21:10:23 which library function starts such a scoped thread? 21:10:33 pub fn std::thread::scope<'env, F, T>(f: F) -> T where F: for<'scope> FnOnce(&'scope Scope<'scope, 'env>) -> T 21:10:59 which creates a Scope which can do this: 21:11:22 pub fn spawn(&'scope self, f: F) -> ScopedJoinHandle<'scope, T> where F: FnOnce() -> T + Send + 'scope, T: Send + 'scope 21:11:30 ah, advanced type magic 21:11:49 this is only intermediate type magic I think 21:11:55 I think that's similar advanced type magic to what Haskell ST uses 21:12:08 ok fine, if it were advanced I couldn't even conceive it 21:12:30 right, I can mostly follow this one, there is some type magic I struggle with 21:14:20 I'll have to look at how the heck that works because I really haven't payed attention to scoped threads 21:14:27 @type runST 21:14:28 (forall s. ST s a) -> a 21:14:30 they didn't sound like something I wanted to do 21:14:44 that 'scope is similar to the s in ST s a 21:15:14 oh wait, this is a permaborrow isn't it 21:15:20 so quite advanced on the level of type magic 21:15:57 I have been meaning to learn more about permaborrows and write more about them, too 21:16:24 I feel like I understand them much better than the average Rust dev – I've answered Stack Overflow questions that turned out to be about them, and written code that makes use of them intentionally 21:16:36 but they're still one of the most confusing areas of Rust and have bad compiler diagnostics 21:18:05 this is the sort of situation where a permaborrow would make sense 21:19:20 fwiw, I suspect that if permaborrows were more widely understood, then pinning wouldn't be necessary 21:19:31 but I'm not totally sure 21:46:40 [[Language list]] M https://esolangs.org/w/index.php?diff=159692&oldid=159422 * Buckets * (+11) 21:47:22 [[User:Buckets]] M https://esolangs.org/w/index.php?diff=159693&oldid=159423 * Buckets * (+10) 21:47:40 [[Talk:Calcu-less 2]] N https://esolangs.org/w/index.php?oldid=159694 * Anthonykozar * (+728) Two questions. 21:47:50 [[Beef]] N https://esolangs.org/w/index.php?oldid=159695 * Buckets * (+2367) Created page with "Beef is an Esoteric programming language created by [[User:Buckets]] in 2021. At the Start, It will Spiral Outwards in a Clockwise Manner Coming out From the Right. {| class="wikitable" |- ! Commands !! Instructions |- | < || Move left once. |- | > || Change the movment 21:52:58 -!- impomatic has quit (Quit: Client closed). 22:10:13 [[Sleep.]] M https://esolangs.org/w/index.php?diff=159696&oldid=154760 * Buckets * (-350) 22:33:05 anyway, if you figure out whether this can break something without scoped threads I'll be interested, because that would localize the problem. 22:33:43 also whether it could break anything without closures, because maybe you have to clarify the interaction of scoped generics and closures 22:39:14 -!- tromp has quit (Quit: My iMac has gone to sleep. ZZZzzz…). 23:15:30 well, a closure is just sugar for an anonymous struct that implements FnOnce/FnMut/Fn 23:16:37 the current scoped thread APIs requires closures to be able to pass any data to it, but this seems like a coincidental/inessential detail rather than something that it would make sense to rely on 23:22:18 -!- Sgeo has joined.