3 ms·
You’ve invented lisp. The issue with meta programming is that it’s too powerful, in the sense that the transformations can’t be statically checked for typing r
by amw-zero 3y ago
You’ve invented lisp.
The issue with meta programming is that it’s too powerful, in the sense that the transformations can’t be statically checked for typing rules.
- 3cats-in-a-coat 3y agoI clearly haven't invented LISP, because the limitations you mention are not inherent to what I'm describing. LISP (and SmallTalk, and Erlang) had many correct ideas, but drastically underperformed in others. Unfortunately we threw out the baby with the bathwater. It doesn't matter how flexible the macro programming is, if it reduces statically to something you can typecheck, therefore this artificial segregation of syntax and rules (and mental models) represents us solving a problem superficially, in an almost cargo-cult way, because we never stopped long enough to think about at depth.
- amw-zero 3y agoI agree with the premise - type-level logic is still just logic, so why not unify the syntax? There's a specification / model checking system called TLA+. This is exactly how you specify types - just as predicates in the same logic as the behavior is defined in. The issue is, it's not statically checkable. I think the issue is that the vast minority of logic is statically checkable, so your type-level logic would have so many weird restrictions that you couldn't use the full syntax anyway. So it's actually beneficial to keep them separate.