Hacker News new | past | comments | ask | show | jobs | submit login

> 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), C# (https://blog.hediet.de/post/how-to-stress-the-csharp-compile...), Scala (https://michid.wordpress.com/2010/01/29/scala-type-level-enc...), Haskell, Rust (https://sdleffler.github.io/RustTypeSystemTuringComplete/), Typescript (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.




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.


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


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


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).




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: