There is nothing inherently bad with turing complete type systems aka allow powerful logic but aren't total (there are ways to avoid proof inconsistency). Other

There is nothing inherently bad with turing complete type systems aka allow powerful logic but aren't total (there are ways to avoid proof inconsistency). Other than the risk of non terminating type checking/compilation, the issue is a matter of difficulty (hard to do right) not principle (bad to do). The problem with C++ templates is not that they are turing complete. Versus Haskell, it is the difference between one day waking up and finding out that layer upon layer of unspeakable ad-hocery have suddenly yielded a deranged spam bot suffering from a severe case of logorrhea that can pass the turing test, given a patient examiner.. And an AI designed from first principles using an elegant theory - even if messy in implementation from unforeseen expectations requiring a patchwork of (still principled) extensions. An approachable language with a particularly interesting type system that compiles to prologish: http://www.shenlanguage.org/learn-shen/types/types_sequent_calculus.html http://www.shenlanguage.org/learn-shen/types/types_sequent_c...