This and the other comment under this seem to be talking about the work the computer is doing at runtime. I believe the point is about the developer's work in implementing this. (For example, renaming potentially conflicting variables is clearly _less_ work than renaming only the actually conflicting variables, in this framing.) This kind of work is important for (1) compilers whose bugs are potentially very financially expensive, and (2) compilers with very intentionally-portable implementations (including but not limited to educational implementations)
Variables are uniquely named at parse time, but after one beta step, you have two distinct instances each of x and y, albeit in different scopes, and after a second beta step, you have two distinct variables named y in the same scope.
"
This doesn't come up in most mainstream languages, but Zig and Jai are getting people excited about comptime evaluation, and dependent types need comptime evaluation as well. Uniqueness is fine until you're doing higher-order evaluation in your compilation pipeline like this, which will be more and more desirable in the future, at least if the current trends are any indication.
An accessible introduction to the infamous Par operator, with a focus on intuition. Notably, this is on the broader concept of multiplicative disjunction, which appears even outside of linear logic!
Alternative title: Par and Constructive Classical Logic.
I've finally rounded out the Par trilogy, on sequent calculus, linear logic, and continuations! This post was the point of the whole series, and the most likely to contain things you haven't already heard. I really love par and the theory around it; the elegance is incredibly satisfying. I hope I can share that with you!
A new guide on linear logic! Much deeper than the usual "imagine a vending machine" guide, though I do mention the connection to that at the end lol. This is great for getting an intuition for substructural logics in academic papers, as well as the notorious multiple-conclusion sequents used in, say, type systems for safe parallelism. The post prior gives the necessary background on sequent calculus, if needed. This series is on much of the most beautiful theory ever, and I hope you enjoy!!
I'm glad you liked it! I have one more post planned for this series, on par and using continuations for classical logic proof terms. I have two other posts in the works but they aren't part of this series, which will only have that one more post.
Much of what I learned was from blog posts like this one, or at least they got me to the point where I could understand the papers on my own. Blog posts, YouTube, reddit, discord, all helped me a ton. Originally I just wanted to make a cool programming language, but the more research I learned the more my interest shifted to the research, because it's just so unbelievably gorgeous and elegant!
A new guide on linear logic! Much deeper than the usual "imagine a vending machine" guide, though I do mention the connection to that at the end lol. This is great for getting an intuition for substructural logics in academic papers, as well as the notorious multiple-conclusion sequents used in, say, type systems for safe parallelism. The post prior gives the necessary background on sequent calculus, if needed. This series is on much of the most beautiful theory ever, and I hope you enjoy!!
Oh yeah I'm well aware of the meme haha. I just wanted to show that I'm conscious of these things in my writing. My dedicated entry on monads (https://ryanbrewer.dev/wiki/monad) alludes to the meme in the first sentence :)
You probably mean set theory instead of graph theory, since set theory and category theory are kind of seen as two foundations for math.
Both category theory and set theory use sets. But set theory tries to make absolutely everything into a set. It takes on a little complexity in this quest, because of Russel's paradox. Category theory can be seen as studying set theory, among other things, so it is "bigger" or more all-encompassing than set theory. Many things studied in category theory aren't possibly sets.
Set theory is more immediately intuitive, but category theory organizes things in a way that are ultimately more insightful, I think. Meaning that once you can get into the category theory headspace and learn to navigate it, it becomes a much better environment for thinking without mistakes. In my personal opinion.
Hey there! I'm the author, so I suppose I ought to address this :)
First I'll say that I absolutely get this head-banging-on-desk feeling of no progress. Monads got me like that for a while but F-Algebras/recursion schemes got me like that much more, so make sure you keep your distance from them haha. I'm sorry to have contributed to your frustration.
It actually sounds like you've grasped monads quite well. flatMap is the essence. I won't try to explain it though, because I know that's not what you're looking for, and I don't want to contribute to your frustration even more!
I will say that my usual readership includes a lot of people who like designing type systems for programming languages. Category theory helps make sure you don't make mistakes in this process, though there are other techniques of course. I also find it helps my ability to think formally a lot, which has helped me a ton in studying and discussing philosophy, a separate interest of mine. Hopefully you can see from my post that I didn't really make an effort to justify or explain category theory for regular programmers much. Category theory is overhyped for that use case. I personally really hate reading overly mathematical Haskell code!! But if you just enjoy math or philosophy or learning or thinking, I hope you can have some fun with the beauty of these ideas. And since authoring the post I've added a wiki https://ryanbrewer.dev/wiki that can give more accessible background on things like monoids.
I could be wrong but I don't think I mentioned a monoid of endofunctors or flatMap a single time in the post. I did mention monads, as an example of natural transformations, but completely from the perspective of beautiful math, not from a programming perspective at all. And once you learn about adjunctions, monads get even more gorgeous! https://ryanbrewer.dev/wiki/adjunction
But all of this math takes a ton of patience. I'm someone who loves programming because the feeling of solving a hard bug is exhilarating and satisfying. The emotional payoff is bigger the longer it takes, and math is the same way for me. Don't beat yourself up about it, and don't feel bad if category theory just isn't helpful or enjoyable for you and your particular way of thinking! :)
Author here. It's a linked list, which is a tree, so post-order here means "recurse, then operate on the result" as opposed to "operate on something and then recurse on the result." So `f(head, r(tail))` instead of `r(f(head, tail))`. This post-order-ness can make it appear strange because first we go to the end of the list and produce the type String, then we process the second-to-last to get, say, the type Int->String, and so on until the first element, adding something to the front each time instead of to the back. The final result still has the parameters listed in the right order, as you mentioned, it's just that the order of operations to get there feels weird, where we're prepending to the return type instead of appending to the first parameter type. Sorry that was poorly written!
Author here. I originally wrote this about printf, but changed it because I wanted to stay away from any discussion of side effects. The rewrite wasn't perfect! In my head, a printf that returns the new string instead of printing it is called "sprintf," and I know others have this impression in a culture that is more general than just C. But you're absolutely right!
Author here, thanks for pointing that out! It was a mistake on my part (: I originally wrote this about printf, but decided I should include the section where I implement it, and I decided I didn't want to say anything about side effects, so I changed everything to a version that just returns the new string. In my head this is called "sprintf" (and the notes I based this on, linked in the post, did the same thing) though I can see now how this was confusing to people. Especially since I didn't rewrite it perfectly!
I wrote a little post about the typechecking algorithm I devised for SaberVM, a typed stack-based bytecode language like Web Assembly, designed from the ground up for being the target of functional programming languages. Typechecking stack-based bytecode is extremely pretty and elegant, and not talked about very much!
I wrote a little post about the typechecking algorithm I devised for SaberVM, a typed stack-based bytecode language like Web Assembly, designed from the ground up for being the target of functional programming languages
I wrote a post cataloguing my experience reading papers on programming language things.
These are things I wish I'd been aware of when I just started out; I hope this can make the ivory tower of PL theory a little more accessible to other self-taught langdev people (:
In this post I talk about Crary et al.'s Calculus of Capabilities, how it can be used for safe manual memory management without requiring values be used linearly in any way, and why I chose it for SaberVM.
Mostly right. We're still in a prototyping phase for sure. The verifier is still in progress, the execution will follow. That said, the main method of the program reads from a file called `bin.svm` which has the bytecode, and which could be generated by any language that can do binary file I/O. There will be more ways to hook into the VM in the future, as well as other SaberVM implementations that compile the bytecode to native binary or Wasm.
Yeah there are a number of successful compilers from functional languages to Wasm. It's definitely doable. I just wanted a backend that was more focused on being a portable target for functional languages. Throughout these comments I list a number of issues I take with Wasm. It's cool and I want a SaberVM->Wasm transpiler soon but the Wasm spec definitely doesn't look like something I want to be tied to in the long run.
To answer your question more specifically, I've heard from a number of people that the structured control flow of Wasm is pretty painful to deal with when writing a compiler. Doing a relooper pass over a CPS or even SSA IR should not be a necessary step. I get the sense that many compromises are made for Wasm to work.
Wasm has a lot of great proposals that excite me but has other disqualifying factors for me. I don't want to be required to use garbage collector, I'm concerned about how much Wasm is growing in scope with all the proposals, I'm (relatedly) concerned about portability and my ability to write my own runtime for Wasm that stays compatible in the long run, and I want a runtime that isn't browser-first, merely browser-supporting.
That's true, mostly because of the JVM's garbage collection. SaberVM also hopes to be a good way to run untrusted code, like the JVM, but it can run much lower level, higher performance code safely, using arenas and the theory powering Vale. AOT compiled SaberVM bytecode can have optimization passes that remove many of the checks, like Vale has now, and that can still be done on the client's computer in a safety-preserving way.
The JVM also comes from an era of OOP being a very pervasive norm, which helped Java's popularity a lot. My impression is that the JVM is seen by many as an annoying bottleneck and massive dependency that's the cost of using Java, a language they enjoy.
The type system is stolen from some of the work on TAL (typed assembly language), by Greg Morrisett and others. In my implementation at the moment it's linear first in the size of the program and then there's a little more checking that's linear in the number of functions. The design is still settling, and it very well might be just linear in the future.
Your point about garbage collection is very fair. For some reason in my head when I wrote that I thought of null pointer exceptions, but that is indeed a different thing.