57

Scalaの型システムはチューリング完全であるという主張があります。私の質問は次のとおりです。

  1. これの正式な証明はありますか？

  2. Scala型システムでの単純な計算はどのようになりますか？

  3. これはScala（言語）にとって何かメリットがありますか？これにより、チューリング完全型システムのない言語と比較して、Scalaは何らかの形でより「強力」になりますか？

これは一般的に言語と型システムに当てはまると思います。

4

2 に答える 2

39

チューリング完全であることが知られている SKI コンビネータ計算の型レベルの実装に関するブログ投稿がどこかにあります。

チューリング完全型システムには、チューリング完全言語と基本的に同じ長所と短所があります。何でもできますが、証明できることはほとんどありません。特に、実際に最終的に何かを行うことを証明することはできません。

型レベルの計算の一例は、Scala 2.8 の新しい型保持コレクション トランスフォーマーです。Scala 2.8 では、 などのメソッドはmap、filter呼び出されたのと同じ型のコレクションを返すことが保証されています。したがって、あなたがfilteraなら a をSet[Int]返し、あなたがaSet[Int]ならaを返します。mapList[String]List[Whatever the return type of the anonymous function is]

ご覧のとおり、map実際に要素の型を変換できます。では、新しい要素の型が元のコレクションの型で表現できない場合はどうなるでしょうか? 例: a にBitSetは、固定幅の整数のみを含めることができます。では、 があり、BitSet[Short]各数値をその文字列表現にマップするとどうなるでしょうか?

someBitSet map { _.toString() }

結果はになりますがBitSet[String]、それは不可能です。そのため、Scala は、BitSetを保持できるの最も派生したスーパータイプ (Stringこの場合は ) を選択しSet[String]ます。

この計算はすべて、コンパイル時、またはより正確には型チェック時に、型レベル関数を使用して行われます。したがって、型が実際に計算され、設計時に不明であっても、型安全であることが静的に保証されます。

于 2010-10-28T22:44:22.467 に答える
34

Scala型システムでのSKI微積分のエンコードに関する私のブログ投稿は、チューリング完全性を示しています。

いくつかの単純な型レベルの計算では、自然数と加算/乗算をエンコードする方法に関する例もいくつかあります。

最後に、Apocalispのブログに、タイプレベルのプログラミングに関するすばらしいシリーズの記事があります。

于 2010-10-29T10:02:55.743 に答える