4 ms·

We do a lot of this in computing and engineering. Reinventing the same thing under different names. A JIT is nothing but "compiler at runtime". And a compiler,

We do a lot of this in computing and engineering. Reinventing the same thing under different names. A JIT is nothing but "compiler at runtime". And a compiler, parser, tokenizer are all converting one representation into another. Compile-time and run-time are completely nominal, there's no reason why we should not start reducing terms as we type, with the "run-time" engine (of course the runtime should know what causes side-effects and stop there). Eventually we need to make type systems just metaprogramming using the primary language that they're intended for. There's no reason for those to be two languages.

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 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 ago
    I 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.
arc619 3y ago
> Eventually we need to make type systems just metaprogramming using the primary language Nim is like this and its fantastic. None of the weird special rules for metaprogramming, just Nim code manipulating ASTs at compile time procedurally. Can even use standard library.
- arc619 3y ago
  I should add that Nim still still has a 'separate language' for types, so doesn't quite fit OP's bill. Nevertheless, it's quite easy to build type constructs using statically resolvable expressions. I'd love to know if anyone could reproduce the N-queens example in Nim: https://www.richard-towers.com/2023/03/11/typescripting-the-technical-interview.html https://www.richard-towers.com/2023/03/11/typescripting-the-... I believe it is possible, but don't have the time to try it out. > The Nim compiler includes a simple linear equation solver, allowing it to infer static params in some situations where integer arithmetic is involved. From: https://nim-lang.org/docs/manual_experimental.html#concepts-generic-concepts-and-type-binding-rules https://nim-lang.org/docs/manual_experimental.html#concepts-...

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 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 ago
  I 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.

arc619 3y ago

> Eventually we need to make type systems just metaprogramming using the primary language Nim is like this and its fantastic. None of the weird special rules for metaprogramming, just Nim code manipulating ASTs at compile time procedurally. Can even use standard library.

arc619 3y ago
I should add that Nim still still has a 'separate language' for types, so doesn't quite fit OP's bill. Nevertheless, it's quite easy to build type constructs using statically resolvable expressions. I'd love to know if anyone could reproduce the N-queens example in Nim: https://www.richard-towers.com/2023/03/11/typescripting-the-technical-interview.html https://www.richard-towers.com/2023/03/11/typescripting-the-... I believe it is possible, but don't have the time to try it out. > The Nim compiler includes a simple linear equation solver, allowing it to infer static params in some situations where integer arithmetic is involved. From: https://nim-lang.org/docs/manual_experimental.html#concepts-generic-concepts-and-type-binding-rules https://nim-lang.org/docs/manual_experimental.html#concepts-...