Scalaは、システムFωに基づくタイプシステムを使用します。これは、通常、強く正規化されていると言われています。強く正規化することは、非チューリングの完全性を意味します。Scalaの型システムのうち、チューリングが完了したのはどのプロパティですか？
それにもかかわらず、ScalaのタイプシステムはTuring-completeです。
正式なアルゴリズムやシステムと比較してScalaの型システムTuring-completeが変更/追加/変更されましたか？
これは包括的な答えではありませんが、の再帰的なタイプを定義できるからです。
私は（about what a non-Turing complete language might look like）以前に同様の質問をしました。答えは次の形式のものでした：チューリング完全言語は任意のループまたは再帰をサポートする必要があります。 Scalaの型システムは後者をサポートします
再帰的JavaやPascalを含むほとんどの言語に型が存在します。リンクされたリストのような、それ自身を参照するすべての型は再帰的です。タイプアプリケーションなど、タイプレベルでの計算を実行する方法が必要です。 Scalaでは、タイプエイリアスに型メンバーと部分型アプリケーションがあります。 –
私はpeanoエンコーディングの意味で再帰型を意味していました。http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/ 'class'や'形質」。私はそれが文脈を考えれば合理的に明らかだと思った。私が言ったように、私はここで、私は完全性のチューリングについて語られているとエコーしています。 –
[再帰型]（http://en.wikipedia.org/wiki/Recursive_data_type）は、あなたが言うように数字をエンコードするために使用できますが、チューリングの完全性のためには十分ではありません。必要なのは、この場合はタイプアプリケーション（代わりに置換を使用する）を使用して計算する方法です。 Scalaの型メンバーはそれをやや簡単にしますが、Javaはジェネリックの同様の置換を実行します。 –
リンク/参照がありますか？ （私のような観客のために:-) –
システムFが強く正規化しているという事実は、システムFがチューリングが完了していないことを意味します。それは型システムがそうではないことを意味するものではない。実際、[無制限のシステムFの型チェックは決めることができません]（http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.6.6483） – sepp2k
@ sepp2k - yikes、 Turing-completenessに関する最悪の事は、それを持っています。 – Malvolio