チューリング完全型システムの理由

Question

ScalaとHaskellには「チューリング完全型システム」があります。通常、チューリングの完全性はcomputations and languagesを指します。タイプの文脈ではどういう意味ですか？

プログラマがどのように恩恵を受けるかの例を挙げてください。

PSハスケル対スカラの型システムを比較したくありません。それは一般的にこの用語の詳細です。

PSS可能であれば、より多くのScalaの例があります。

Answer 1

タイプのコンテキストではどういう意味ですか？

これは、タイプシステムに、任意の計算を表すのに十分な機能があることを意味します。非常に短い証拠として、以下ではSK計算のタイプレベルの実装を紹介します。この微積分のチューリング完全性とその意味について議論する場所がたくさんあるので、ここでそれを再ハッシュしないでください。

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE UndecidableInstances #-} 
{-# LANGUAGE TypeOperators #-} 

infixl 1 `App` 
data Term = S | K | App Term Term 

type family Reduce t where 
    Reduce S = S 
    Reduce K = K 
    Reduce (S `App` x `App` y `App` z) = Reduce (x `App` z `App` (y `App` z)) 
    Reduce (K `App` x `App` y) = Reduce x 
    Reduce (x `App` y) = Reduce (Reduce x `App` y) 

これはghciプロンプトで確認できます。

> :kind! Reduce (S `App` K `App` S `App` K) 
Reduce (S `App` K `App` S `App` K) :: Term 
= 'K 

ここに1つは、同様に試して楽しい： -

> type I = S `App` K `App` K 
> type Rep = S `App` I `App` I 
> :kind! Reduce (Rep `App` Rep) 

私は楽しみを台無しにしません例えば、SK微積分では、用語SKSKはちょうどKする（最終的に）減少し - 自分で試してみてください。しかし、最初に極端な偏見を持ってプログラムを終了させる方法を知っている。

プログラマがどのように恩恵を受けることができるのかを示す例がありますか？

任意の型レベル計算を使用すると、型に任意の不変量を表現でき、コンパイラで（コンパイル時に）それらが保持されていることを確認させることができます。赤黒の木が欲しいですか？コンパイラがチェックできる赤黒の木は、赤黒の木の不変量を保持していますか？それは実装バグ全体のルールを排除するので、便利でしょう。特定のスキーマに一致することが静的に分かっているXML値の型はどうですか？実際に、さらに進んで、パラメータがスキーマを表すパラメータ化された型を書き留めてみませんか？次に、実行時にスキーマを読み込み、コンパイル時のチェックによって、パラメータ化された値がそのスキーマ内の整形式の値のみを表すことが保証されるようにします。ニース！

または、おそらくより賢明な例：コンパイラで、辞書にインデックスが存在しないことをチェックしないようにするにはどうすればよいでしょうか？充分に進んだタイプのシステムでは、可能です。

もちろん、常に価格があります。 Haskell（おそらくScala？）では、非常にエキサイティングなコンパイル時のチェックの価格は、コンパイラがあなたがチェックしていることが真実であることを確信させる多くのプログラマーの時間と労力を費やしています。先行コストと高い継続的なメンテナンスコストの両方を提供します。