5 ms·

Proof that type systems are nothing else that domain-specific languages that run at compile time. When seen like that, it should be no surprise that they can be

Proof that type systems are nothing else that domain-specific languages that run at compile time. When seen like that, it should be no surprise that they can be coerced to do general computation.

vore 3y ago
That’s not universally true, and indeed some languages (e.g. Haskell without extensions) have explicitly designed decidable type systems.
- slaymaker1907 3y ago
  That just means that it isn’t Turing complete which is true of many DSLs.
  - formulathree 3y ago
    Which means you can't to general computation with it. You're just reiterating his point.
    - slaymaker1907 3y ago
      Regex (at least most implementations) isn't Turing complete, but you can still do a lot of stuff with it and I think most type systems go far beyond regex in expressive power. Unless you're trying to write quines, you probably don't need Turing completeness.
marton78 3y ago
Yes. We have known this since C++ template metaprogramming.
paganel 3y ago
> else that domain-specific languages that run at compile time. Probably stupid question, but that probably means that one could, theoretically, implement a type system for any one of those DSL(-like) type systems, isn't that correct? And so on and so forth, we could have, theoretically, DSL-like type systems all the way down.
- mejutoco 3y ago
  The difference between regular languages and "type system languages" (at least well designed ones) is that the latter are decidable. In that sense another typesystem lang for the typesystem lang would still be a decidable one. The most generic one I know of is Idris. It uses some heuristics to make some functions decidable that in theory should not be.
- cnity 3y ago
  Welcome to Lisp.
3cats-in-a-coat 3y ago
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.
weinzierl 3y ago
Some languages have type systems like that, either deliberately as in the case of Idris and Agda or accidentally as in C++ or Typescript. It doesn't have to be that way and in my opinion for general purpose languages it shouldn't. The type system should be about constraints that facilitate reasoning about your code - reasoning by machine and human. Compile time computation should be a separate facility.
- WorldMaker 3y ago
  It wasn't an accident in Typescript. Each step along the way seemed well deliberated and to facilitate reasoning about someone's code, despite the computational complexity trade-offs. (That a lot of that was to facilitate reasoning about nearly untyped JS code doing a lot of dynamic code things is, depending on which side of the deliberation you are on: 1] a sign that dynamic code has always been that complex and developers have had to do all that sort of "compile time logic" in their own heads for so long, and/or 2] a sign that Typescript's "flaws" come from trying to be too supportive of existing bad JS code.)
bmacho 3y ago
Indeed, type systems are domain-specific languages, that run at compile time or runtime, and specify constraints about values. Most of them can be coerced to do general computation, especially if they have things like if-branch, and some sort of self-reference.
- formulathree 3y ago
  Most of them can't be coerced like this. Typescript is one of the few that can be.
  - bmacho 3y ago
    The type systems of C++, C#, Java, Scala, Rust, Haskell, Swift etc all Turing complete/undecidable, aren't they?
formulathree 3y ago
It is no surprise. They can be coerced to prove your program correct, negating the need to do unit tests. But this is only true for certain languages. Overall most type systems are not Turing complete and therefore not suited for general computation

Proof that type systems are nothing else that domain-specific languages that run at compile time. When seen like that, it should be no surprise that they can be coerced to do general computation.

vore 3y ago

That’s not universally true, and indeed some languages (e.g. Haskell without extensions) have explicitly designed decidable type systems.

slaymaker1907 3y ago
That just means that it isn’t Turing complete which is true of many DSLs.
- formulathree 3y ago
  Which means you can't to general computation with it. You're just reiterating his point.
  - slaymaker1907 3y ago
    Regex (at least most implementations) isn't Turing complete, but you can still do a lot of stuff with it and I think most type systems go far beyond regex in expressive power. Unless you're trying to write quines, you probably don't need Turing completeness.

marton78 3y ago

Yes. We have known this since C++ template metaprogramming.

paganel 3y ago

> else that domain-specific languages that run at compile time. Probably stupid question, but that probably means that one could, theoretically, implement a type system for any one of those DSL(-like) type systems, isn't that correct? And so on and so forth, we could have, theoretically, DSL-like type systems all the way down.

mejutoco 3y ago
The difference between regular languages and "type system languages" (at least well designed ones) is that the latter are decidable. In that sense another typesystem lang for the typesystem lang would still be a decidable one. The most generic one I know of is Idris. It uses some heuristics to make some functions decidable that in theory should not be.
cnity 3y ago
Welcome to Lisp.

3cats-in-a-coat 3y ago

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.

weinzierl 3y ago

Some languages have type systems like that, either deliberately as in the case of Idris and Agda or accidentally as in C++ or Typescript. It doesn't have to be that way and in my opinion for general purpose languages it shouldn't. The type system should be about constraints that facilitate reasoning about your code - reasoning by machine and human. Compile time computation should be a separate facility.

WorldMaker 3y ago
It wasn't an accident in Typescript. Each step along the way seemed well deliberated and to facilitate reasoning about someone's code, despite the computational complexity trade-offs. (That a lot of that was to facilitate reasoning about nearly untyped JS code doing a lot of dynamic code things is, depending on which side of the deliberation you are on: 1] a sign that dynamic code has always been that complex and developers have had to do all that sort of "compile time logic" in their own heads for so long, and/or 2] a sign that Typescript's "flaws" come from trying to be too supportive of existing bad JS code.)

bmacho 3y ago

Indeed, type systems are domain-specific languages, that run at compile time or runtime, and specify constraints about values. Most of them can be coerced to do general computation, especially if they have things like if-branch, and some sort of self-reference.

formulathree 3y ago
Most of them can't be coerced like this. Typescript is one of the few that can be.
- bmacho 3y ago
  The type systems of C++, C#, Java, Scala, Rust, Haskell, Swift etc all Turing complete/undecidable, aren't they?

formulathree 3y ago

It is no surprise. They can be coerced to prove your program correct, negating the need to do unit tests. But this is only true for certain languages. Overall most type systems are not Turing complete and therefore not suited for general computation