4 ms·
I 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
by 3cats-in-a-coat 3y ago
I 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.