I may have come up with a new syntax for the lambda calculus? I call it stitch notation. λx. x = : 0 λx. λy. x = :: 0 λx. λy. x y = :: 0 1 λx. x (λy. x y) = : 0 (: ^0 0) It’s nothing groundbreaking and my explicit intention was to make something very similar to what’s come before, just hopefully easier for people to read and work with. Specifically I wanted bound variables to be nameless and use indices like De Bruijn notation, but I wanted to make functions easier to understand at a glance and reductions more straightforward for people to do. Each colon introduces an argument, numbers select arguments starting from zero, and each caret reaches out one enclosing argument group. Has anyone seen this particular approach before?

Seems like a rite of passage to explain Monads when you think you finally get them. So here goes for me... Monads aren't a concrete thing, they're a pattern for chaining operations on values that live in some context. Two functions are paramount, and their type signatures tell you almost everything you need to know: return and bind. Return's type is (a -> M a). It puts a raw value, a, into a context, M. That's it. Bind's type is (M a -> (a -> M b) -> M b). So it takes two arguments, a value already in context, M a, and a next-step function, (a -> M b). Bind lets the context determine how to feed an a into that function, and gives you the resulting M b in the same kind of context M.

Is it better to study with an LLM-crafted curriculum than reading books or courses? I would assume so. I’m having Claude write me a type theory curriculum now.

Damn. How it begins!