hoping1

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)

See cvoss's comment in another thread:

" What happens in the evaluator when you have

(\ a . a a) (\ x . \ y . x y)

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!

Thanks!

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!!

Fair, I think of this as advanced logic, and those concepts (and that notation) as prerequisite.

Ah heck, I should have added a section on PTSs, maybe I still will or maybe that will be standalone later. It really is gorgeous stuff!!

Extensive and patiently-paced, with many examples, and therefore unfortunately pretty long lol

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 :)

Only in locally-small categories. But yes, category theory often makes use of sets.

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.

Thanks for taking the time haha, let me know if I can improve my exposition!

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!

Where I discuss five specific things that make simple programming languages simple and great.

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 (: