3 ms·

Having a Turing complete type system is not what you normally want to have, that (it means to have undecidable type checking) makes tooling (and the compiler) w

Having a Turing complete type system is not what you normally want to have, that (it means to have undecidable type checking) makes tooling (and the compiler) way more complex and difficult. GitHub issue about the Turing completeness: https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833 Proof of Turing completeness: https://gist.github.com/hediet/63f4844acf5ac330804801084f87a6d4 https://gist.github.com/hediet/63f4844acf5ac330804801084f87a...

gpderetta 5y ago
Which widely used statically typed languages do not have a Turing complete type system? C, probably Go?
- ReleaseCandidat 5y ago
  Depends on your definition of 'widely used' ;). Using Tiobe's top 20: I'd guess Swift, Delphi, Fortran and Go C++, Java, Rust, Haskell, Typescript have a Turing complete type system. C#: don't know, could be.
  - gpderetta 5y ago
    Of the list above, I'm most surprised that Swift doesn't have a Turing complete type system.
    - ReleaseCandidat 5y ago
      I wanted to answer with "because Swift's type checking is decidable", but that has changed (with SE-0142 and SE-0157) - allowing recursion. So, it is 'at least' undecidable now. https://forums.swift.org/t/swift-type-checking-is-undecidable/39024 https://forums.swift.org/t/swift-type-checking-is-undecidabl...
      - gpderetta 5y ago
        Yes, I did see that bit. Incidentally google provides terrible results for 'swift type system turing complete'.
deleted 5y ago
[deleted]
jcelerier 5y ago
Thanks but I'll take the ability to write arbitrarily complex type-checks over anything else. As a C++ dev who goes out of his way to express things of the type system this has only ever been a positive for me, the loss in compile-time is more than offset by the ability to eliminate whole classes of bugs in one go.
- bmc7505 5y ago
  If you want arbitrarily complex type-checking, why not just check the property you want at runtime instead using an esoteric typelevel programming language? The whole point of having types in the first place is provable decidability, not universal computation -- that's what the value-level is designed to do.

gpderetta 5y ago

Which widely used statically typed languages do not have a Turing complete type system? C, probably Go?

ReleaseCandidat 5y ago
Depends on your definition of 'widely used' ;). Using Tiobe's top 20: I'd guess Swift, Delphi, Fortran and Go C++, Java, Rust, Haskell, Typescript have a Turing complete type system. C#: don't know, could be.
- gpderetta 5y ago
  Of the list above, I'm most surprised that Swift doesn't have a Turing complete type system.
  - ReleaseCandidat 5y ago
    I wanted to answer with "because Swift's type checking is decidable", but that has changed (with SE-0142 and SE-0157) - allowing recursion. So, it is 'at least' undecidable now. https://forums.swift.org/t/swift-type-checking-is-undecidable/39024 https://forums.swift.org/t/swift-type-checking-is-undecidabl...
    - gpderetta 5y ago
      Yes, I did see that bit. Incidentally google provides terrible results for 'swift type system turing complete'.

deleted 5y ago

[deleted]

jcelerier 5y ago

Thanks but I'll take the ability to write arbitrarily complex type-checks over anything else. As a C++ dev who goes out of his way to express things of the type system this has only ever been a positive for me, the loss in compile-time is more than offset by the ability to eliminate whole classes of bugs in one go.

bmc7505 5y ago
If you want arbitrarily complex type-checking, why not just check the property you want at runtime instead using an esoteric typelevel programming language? The whole point of having types in the first place is provable decidability, not universal computation -- that's what the value-level is designed to do.