25

Scala と Haskell には「チューリング完全型システム」があります。通常、チューリングの完全性は計算と言語を指します。型のコンテキストでは、それは実際には何を意味するのでしょうか?

プログラマーがそれからどのように利益を得ることができるかの例を挙げてもらえますか?

PS Haskell の型システムと Scala の型システムを比較したくありません。それは一般的な用語についてです。

PSS 可能であれば、より多くの Scala の例を提供してください。

4

1 に答える 1

31

型のコンテキストでは、それは実際には何を意味するのでしょうか?

これは、型システムが任意の計算を表すのに十分な機能を備えていることを意味します。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 プロンプトで実際に確認できます。たとえば、SK微積分では、項SKSKは (最終的に) に還元されますK。

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

こちらも試してみるのが楽しいものです：

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

楽しみを台無しにするつもりはありません。自分で試してみてください。ただし、最初に極度の偏見を持ってプログラムを終了する方法を知っておいてください。

プログラマーがそれからどのように利益を得ることができるか、誰かが例を挙げてもらえますか?

任意の型レベルの計算により、型の任意の不変条件を表現し、それらが保持されていることを (コンパイル時に) コンパイラーに検証させることができます。赤黒の木が欲しいですか？コンパイラがチェックできる赤黒木が赤黒木の不変条件を保持していることはどうですか? 実装のバグのクラス全体を除外するので、それは便利ですよね? 特定のスキーマに一致することが静的にわかっている XML 値の型はどうでしょうか。実際、さらに一歩進んで、パラメーターがスキーマを表すパラメーター化された型を書き留めてみませんか? 次に、実行時にスキーマを読み取り、コンパイル時のチェックで、パラメーター化された値がそのスキーマの適切な形式の値のみを表すことができることを保証できます。良い！

または、おそらくもっと平凡な例: 存在しないキーで辞書にインデックスを付けていないことをコンパイラにチェックさせたい場合はどうなるでしょうか? 十分に高度な型システムがあれば、それが可能です。

もちろん、常に価格があります。Haskell (そしておそらく Scala?) では、非常にエキサイティングなコンパイル時のチェックの代償は、プログラマーが多大な時間と労力を費やして、チェックしていることが真であることをコンパイラーに納得させることです。初期費用だけでなく、継続的なメンテナンス費用も高額です。

于 2015-11-30T16:44:54.257 に答える