hoping1

8 ms·

1.
by hoping1 1y ago
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
2.
by hoping1 1y ago
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
3.
Linear Logic: Par, a Friendly Explanation(ryanbrewer.dev)
3 points by hoping1 2y ago|1 comments
4.
by hoping1 2y ago
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!
5.
Par Part 3: Par, Continued(ryanbrewer.dev)
2 points by hoping1 2y ago|1 comments
6.
by hoping1 2y ago
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
7.
A Tutorial on Linear Logic(ryanbrewer.dev)
5 points by hoping1 2y ago|1 comments
8.
by hoping1 2y ago
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 pape
9.
by hoping1 2y ago
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 tha
10.
by hoping1 2y ago
Thanks!
11.
Linear Logic – Par Part 2(ryanbrewer.dev)
2 points by hoping1 2y ago|5 comments
12.
by hoping1 2y ago
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 pape
13.
by hoping1 2y ago
Fair, I think of this as advanced logic, and those concepts (and that notation) as prerequisite.
14.
by hoping1 2y ago
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!!
15.
Sequent Calculus and Notation – Par Part 1(ryanbrewer.dev)
38 points by hoping1 2y ago|10 comments
16.
by hoping1 2y ago
Extensive and patiently-paced, with many examples, and therefore unfortunately pretty long lol
17.
by hoping1 2y ago
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 fir
18.
by hoping1 2y ago
Only in locally-small categories. But yes, category theory often makes use of sets.
19.
by hoping1 2y ago
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
20.
by hoping1 2y ago
Thanks for taking the time haha, let me know if I can improve my exposition!
21.
by hoping1 2y ago
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 go
22.
Getting Started with Category Theory(ryanbrewer.dev)
51 points by hoping1 2y ago|32 comments
23.
Getting Started with Category Theory(ryanbrewer.dev)
1 points by hoping1 2y ago|0 comments
24.
by hoping1 2y ago
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
25.
by hoping1 2y ago
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
26.
by hoping1 2y ago
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 effec
27.
The Type of Sprintf(ryanbrewer.dev)
1 points by hoping1 2y ago|0 comments
28.
Simple Programming Languages(ryanbrewer.dev)
1 points by hoping1 3y ago|1 comments
29.
by hoping1 3y ago
Where I discuss five specific things that make simple programming languages simple and great.
30.
Advanced Typechecking for Stack-Based Bytecode(ryanbrewer.dev)
1 points by hoping1 3y ago|1 comments

More ›