Feel like you want to sneer about something but you donāt quite have a snappy post in you? Go forth and be mid!
Any awful.systems sub may be subsneered in this subthread, techtakes or no.
If your sneer seems higher quality than you thought, feel free to cutānāpaste it into its own post, thereās no quota here and the bar really isnāt that high
The post Xitter web has spawned soo many āesotericā right wing freaks, but thereās no appropriate sneer-space for them. Iām talking redscare-ish, reality challenged āculture criticsā who write about everything but understand nothing. Iām talking about reply-guys who make the same 6 tweets about the same 3 subjects. Theyāre inescapable at this point, yet I donāt see them mocked (as much as they should be)
Like, there was one dude a while back who insisted that women couldnāt be surgeons because they didnāt believe in the moon or in stars? I think each and every one of these guys is uniquely fucked up and if I canāt escape them, I would love to sneer at them.
can you please talk more about your lambda calculus projects?
sure! there was a little bit about it in the first stubsack and I posted a bit more about it in this thread on masto (with some links to papers Iāve been reading too, if youād like to dig into the details on anything)
overall what Iām working on is a hardware implementation of a Krivine machine, which uses Trompās prefix code bitstream representation of binary lambda calculus as its machine language and his monadic IO model to establish a runtime environment. it isnāt likely to be a very efficient machine by anyoneās standard, but I really like working with BLC as a pure (and powerful) form of computational math, and thereās something pleasant about the way it reduces down to a HDL representation (via the Amaranth HDL in this case). thereās a few subprojects Iāve been working on as part of this:
Iāve been working on some of this on paper as a sleep aid for a while, but Iām finally starting on whatās feeling like a solid HDL implementation. let me know if you want more details on any of it! some of the more far off stuff is really just a mental sketch, but writing it out will at least help me figure out what ideas still make sense when theyāre explained to someone else
for anyone whoās fucking lost reading the above (I canāt blame ya), lambda calculus is the mathematical basis behind functional programming. this is a fun introduction. the only things you can do in lambda calculus are define functions, name variables, and apply functions to other functions or variables (which substitutes the variables for whatever theyāre being applied to and eliminates the function). thatās all you need to represent every possible computer program, which is amazing
a Krivine machine is a machine for doing what the alligators in that intro are doing, automatically ā that is, reducing down lambda functions until they canāt be reduced anymore and produce a final value. that process is computation, so a Krivine machine is a (rather strange) computer
I have a scattered interest in lambda calculus too so Iād love to follow this project. Trompās BLC definitely hits a sweet spot of complexity/size when it comes to describing computation in a way thatās deeply satisfying.
Have you looked into interaction nets/other optimal beta-reduction schemes (thereās a project out there called HVM)? Probably way too high level for now though. I am fascinated by the possibility of these algorithms making church-representations more asymptotically efficient (or even balanced ternary)
exactly! itās such a cool way to write a program, and itās so much more satisfying than writing assembly for a von Neumann (or any load/store) machine. have you checked out LambdaLisp? itās one of my inspirations for this project ā itās amazing that you can build a working Lisp interpreter out of BLC, and understanding how that was done taught me so much about Lispās relationship with lambda calculus.
I plan to release my HDL as a collaborative project once Iāve got enough done to share out. currently Iāve got the HDL finished for the combinational circuit that makes bitstream BLC processing efficient with word-oriented memory hardware, and Iām doing debugging on the buffer that grabs words from memory and offsets them if they represent a term that isnāt word-aligned (which is a pretty simple circuit so Iām surprised Iāve managed to implement so many bugs). thereās quite a bit left to go! IO is still a sticking point ā I know how I want to do it, but I canāt quite imagine how memory and runtime state will look after the machine reads or writes a bit.
that seems awesome! I really like that it can do auto-parallelization, and I want to check out how it optimizes lambda terms. for now my machine model is a pretty straightforward Krivine machine with some inspiration taken from the Next 700 Krivine Machines paper, which seems likely to yield a machine that can be implemented as circuitry. that paper decomposes Krivine-like machine models down into combinators, which can be seen as opcodes, microinstructions, or (in my case) operations that that need to be performed on memory during a particular machine state.
once Iāve got the basic machine defined, Iād like to come back to something like HVM as a higher performance lambda calculus machine and see what can be adopted. one of their memory invariants in particular (the guarantee that each closure is only used once) maps really well to my mental model of what I imagine a hardware parallel lambda calculus machine would be like
I found LambdaLisp from your mastodon post and was immediately intrigued. Iām going to try and run it to get a better understanding of how the IO system works, and maybe even cook up my own BLC interpreter to run it! The hardware stuff is definitely out of my depth, but this may be a great chance to learn.
thatās a great idea! the only BLC VMs I know of are written in a very obscure style (Trompās especially ā his first interpreter was an entry into the International Obfuscated C Code Contest and he only posted the (relatively) unobfuscated one later) and I think thereās plenty of room for something written to be more comprehensible. Iām also not aware of any VM that implements
call-ccfrom Krivineās original paper, which has interesting applications. and of course, all the Krivine machines I know are relatively slow and very memory-inefficient ā but thereās low hanging fruit here that can make things better.one thing I might take on is implementing a visual krivine machine ā something with a GUI that shows its current state and a graph of all the closures in memory. that would be a big boon for my current work, and I might see if I could graft something like that onto the simulation testbench for my HDL implementation.