3 ms·

> There are exceptions of course for a definition of "exceptions" being "virtually all languages with a non-trivial static type system and non-zero userbase" a

> There are exceptions of course for a definition of "exceptions" being "virtually all languages with a non-trivial static type system and non-zero userbase" as shown in your link. Java (https://arxiv.org/abs/1605.05274 https://arxiv.org/abs/1605.05274), C# (https://blog.hediet.de/post/how-to-stress-the-csharp-compiler https://blog.hediet.de/post/how-to-stress-the-csharp-compile...), Scala (https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/ https://michid.wordpress.com/2010/01/29/scala-type-level-enc...), Haskell, Rust (https://sdleffler.github.io/RustTypeSystemTuringComplete/ https://sdleffler.github.io/RustTypeSystemTuringComplete/), Typescript (https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833) ... Having a type system with generics and not being turing-complete as a result is the exception, not the rule.

arianvanp 5y ago
Haskell's System-F is definitely completely is decidable. You need to opt in to undecidable features like RankNTypes (n>=3) explicitly. (which are GHC; and not Haskell specific). Even then; Undecidability is a bit spectrumy. e.g. RankNTypes become sort of decideable again in the presence of explicit type annotations
- smaddox 5y ago
  AFAIK, Haskell requires explicit types for higher-rank types specifically because inference is decidable for them.
gnulinux 5y ago
For an example of contrary, one can check Agda. It is not Turing complete, but a useful language (I personally wrote many parsers in it and its Haskell FFI is pretty good so you can essentially write unsafe parts of your programs in Haskell, and safe parts in Agda then prove correctness).
octachron 5y ago
Generics is not really the right cutting point: parametric polymorphism is perfectly decidable. However, few languages stop at just parametric polymorphism. For instance, the OCaml issue in the linked blog post happens at the module level, which mixes parametric polymorphism and subtyping. And typically, while SML has parametric polymorphism, it lacks the OCaml extension that makes the module type system undecidable.

arianvanp 5y ago

Haskell's System-F is definitely completely is decidable. You need to opt in to undecidable features like RankNTypes (n>=3) explicitly. (which are GHC; and not Haskell specific). Even then; Undecidability is a bit spectrumy. e.g. RankNTypes become sort of decideable again in the presence of explicit type annotations

smaddox 5y ago
AFAIK, Haskell requires explicit types for higher-rank types specifically because inference is decidable for them.

gnulinux 5y ago

For an example of contrary, one can check Agda. It is not Turing complete, but a useful language (I personally wrote many parsers in it and its Haskell FFI is pretty good so you can essentially write unsafe parts of your programs in Haskell, and safe parts in Agda then prove correctness).

octachron 5y ago

Generics is not really the right cutting point: parametric polymorphism is perfectly decidable. However, few languages stop at just parametric polymorphism. For instance, the OCaml issue in the linked blog post happens at the module level, which mixes parametric polymorphism and subtyping. And typically, while SML has parametric polymorphism, it lacks the OCaml extension that makes the module type system undecidable.