alt Hacker NewsI've had some of the same ideas, I would love a full macro system on a dependently typed language. My stab at it earlier in January was not quite the right thing, but I do think this is the way. Weirdly enough concision is even more important in LLM context than in regular human context.
Replies
One thing that has surprised me is how good LLMs are writing Lisp macros. All the annoying boilerplate and backtick-comma arithmetic (',' anyone?) that has ground my gears over the years, they cheerfully churn out correctly. I still review it to make sure they haven't done it in a needlessly complicated way, but I wonder if that is just me being superstitious.
I shouldn't have been surprised, because that part of macro writing is purely mechanical syntax transformation—just a "take these tokens and return those tokens" function that one should expect LLMs to be good at. But I was surprised, because for me that was always the hard part.
So now I can think up new macros to abstract over patterns in my code—the part of macro-writing that I enjoy—and then push a magic "implement this" button to make it work.
What I'm not sure of yet is whether this is an evolutionary dead end—a train stop on the way to "you'll never look at code again, so what does it matter what programming language you used to use". Yes, I still look at my code, and this is a pretty nice train stop, wherever the tracks lead to.
Lean is the dependently typed language with a SotA metaprogramming system. Lean itself is a language written using this system.
Have you looked into tree calculus at all?
You might be interested in Lean. It's my favorite lisp, even though it's really not at all a lisp. It's a nice programming language, and it lets you really hack on commands, macros, syntax, and elaboration.