「Haskell は徐々に依存型言語になりつつある」という意見を繰り返す情報源をいくつか見てきました。その意味するところは、言語拡張が増えるにつれて Haskell は全体的にその方向に向かいつつあるが、まだそこまでには至っていないということのようです。
基本的に知りたいことは2つあります。1つ目は、単純に「依存型言語である」とは実際何なのかということです。平均? (あまり技術的な話にならないことを祈ります。)
2 番目の質問は... 欠点は何ですか? つまり、私たちがその方向に向かっていることは誰もが知っているので、何らかの利点があるはずです。しかし、まだそこに到達していないので、人々が最後まで進むのを妨げる何らかの欠点があるはずです。問題は複雑さが急激に増加することであるという印象を受けます。しかし、依存型付けが何であるかを本当に理解していないので、確かなことはわかりません。
私がする私が知っているのは、依存型プログラミング言語について読み始めるたびに、そのテキストがまったく理解できないということです... おそらくそれが問題です。(?)
ベストアンサー1
依存型 Haskell って今何？
Haskell は、ある程度は依存型言語です。型レベルデータの概念があり、 のおかげでより合理的に型付けされ、型レベルデータに実行時の表現を与えるDataKinds手段 ( ) があります。したがって、GADTs実行時の値は型に効果的に現れるつまり、言語が依存的に型付けされるということです。
単純なデータ型は昇進した種類レベルまで拡張し、その値を型で使えるようにする。そのため、典型的な例は次のようになる。
data Nat = Z | S Nat
data Vec :: Nat -> * -> * where
VNil :: Vec Z x
VCons :: x -> Vec n x -> Vec (S n) x
可能になり、それに伴い、次のような定義も可能になります。
vApply :: Vec n (s -> t) -> Vec n s -> Vec n t
vApply VNil VNil = VNil
vApply (VCons f fs) (VCons s ss) = VCons (f s) (vApply fs ss)
これは素晴らしいことです。長さはnその関数内では完全に静的なものであり、その長さは の実行では役割を果たさないにもかかわらず、入力ベクトルと出力ベクトルが同じ長さになることを保証します。対照的に、与えられた のコピーを作成する関数(のへのコピー) を実装するのははるかに難しい (つまり不可能)vApplyです。nxpurevApply<*>
vReplicate :: x -> Vec n x
実行時にいくつのコピーを作成するかを知ることは非常に重要だからです。そこでシングルトンの出番です。
data Natty :: Nat -> * where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
昇格可能な型であれば、昇格した型をインデックスとして、その値の実行時複製を含むシングルトンファミリを構築できます。は、Natty n型レベルの実行時コピーの型ですn :: Nat。次のように記述できます。
vReplicate :: Natty n -> x -> Vec n x
vReplicate Zy x = VNil
vReplicate (Sy n) x = VCons x (vReplicate n x)
つまり、実行時の値に結び付けられた型レベルの値があります。実行時のコピーを検査すると、型レベルの値の静的な知識が洗練されます。用語と型は分離されていますが、シングルトン構造を一種のエポキシ樹脂として使用し、フェーズ間の結合を作成することで、依存的に型付けされた方法で作業できます。これは、型で任意の実行時式を許可することとは程遠いですが、まったく問題はありません。
何が汚いのか？何が足りないのか？
この技術に少し圧力をかけ、何が揺れ始めるかを見てみましょう。シングルトンはもう少し暗黙的に管理できるべきだという考えが浮かぶかもしれません。
class Nattily (n :: Nat) where
natty :: Natty n
instance Nattily Z where
natty = Zy
instance Nattily n => Nattily (S n) where
natty = Sy natty
例えば、
instance Nattily n => Applicative (Vec n) where
pure = vReplicate natty
(<*>) = vApply
これは機能しますが、元のNat型が 3 つのコピー (種類、シングルトン ファミリ、シングルトン クラス) を生成することを意味します。明示的なNatty n値とNattily n辞書を交換するプロセスがかなり不格好になります。さらに、NattyではありませんNat。実行時の値に何らかの依存関係がありますが、最初に考えていた型ではありません。完全に依存型化された言語では、依存型がこれほど複雑になることはありません。
一方、Nat昇格はできますが、Vecできません。インデックス付き型でインデックスすることはできません。完全な依存型言語にはそのような制限はありません。依存型を自慢する私のキャリアでは、1 層のインデックスを困難ではあるが可能なものにした人々に、私がトランプの家のように崩壊することを期待しないように教えるために、2 層のインデックスの例を講演に含めることを学びました。何が問題なのでしょうか。それは、等式です。GADT は、コンストラクターに特定の戻り値の型を与えるときに暗黙的に達成する制約を、明示的な等式要求に変換することで機能します。次のようになります。
data Vec (n :: Nat) (x :: *)
= n ~ Z => VNil
| forall m. n ~ S m => VCons x (Vec m x)
2 つの方程式のそれぞれにおいて、両辺の種類は ですNat。
次に、ベクトルにインデックス付けされたものに対して同じ変換を試みます。
data InVec :: x -> Vec n x -> * where
Here :: InVec z (VCons z zs)
After :: InVec z ys -> InVec z (VCons y ys)
なる
data InVec (a :: x) (as :: Vec n x)
= forall m z (zs :: Vec x m). (n ~ S m, as ~ VCons z zs) => Here
| forall m y z (ys :: Vec x m). (n ~ S m, as ~ VCons y ys) => After (InVec z ys)
そして、as :: Vec n xとの間に等式制約を形成しますVCons z zs :: Vec (S m) x。ここで、両側は構文的に異なる (ただし、等しいことが証明できる) 種類を持ちます。GHC コアは現在、このような概念に対応していません。
他に何が足りないでしょうか？Haskellのほとんどは型レベルから欠落しています。実際には、昇格できる項の言語には変数と非 GADT コンストラクタしかありません。これらがあれば、このtype family仕組みで型レベルのプログラムを記述できます。これらの一部は、項レベルで記述することを検討する関数と非常によく似ているかもしれませんが (たとえば、Natに加算を装備して、 に追加するための適切な型を与えるなどVec)、それは単なる偶然です。
もう一つ、実際には欠けているのは図書館これは、値によって型をインデックスする新しい機能を活用します。このすばらしい新世界では、何が行われFunctor、Monad何になるのでしょうか? 私はそれについて考えていますが、まだやるべきことがたくさんあります。
型レベルプログラムの実行
Haskellは、他の依存型プログラミング言語と同様に、二操作的意味論。ランタイムシステムがプログラムを実行する方法（閉じた式のみ、型消去後、高度に最適化）と、型チェッカーがプログラムを実行する方法（型ファミリ、開いた式を含む「型クラス Prolog」）があります。Haskell では、実行されるプログラムが異なる言語であるため、通常、この 2 つを混同することはありません。依存型言語には、実行時と静的実行のモデルが別々にあります。同じプログラムの言語ですが、心配しないでください。実行時モデルでは、型の消去や証明の消去が可能です。それがCoqの抽出メカニズムがあなたに与えるのは、少なくともエドウィン・ブレイディのコンパイラが行うことです（エドウィンは、型や証明だけでなく、不必要に重複した値も削除しますが）。フェーズの区別は、統語的カテゴリもうありませんが、元気に生きています。
依存型言語は完全であるため、型チェッカーは長時間待機するよりも悪いものを恐れることなくプログラムを実行できます。Haskell が依存型になるにつれて、その静的実行モデルはどうあるべきかという問題に直面します。1 つのアプローチは、静的実行を完全関数に制限することです。これにより、実行の自由度は同じになりますが、データとコデータを区別する必要があります (少なくとも型レベルのコードの場合)。これにより、終了を強制するか生産性を強制するかを判断できます。ただし、これが唯一のアプローチではありません。計算だけで出てくる方程式が少なくなるという代償を払って、プログラムを実行することを躊躇する、はるかに弱い実行モデルを自由に選択できます。実際、それが GHC が実際に行っていることです。GHC コアの型付けルールでは、ランニングプログラムに制約ソルバーがありますが、方程式の証拠をチェックするだけです。コアに翻訳するとき、GHC の制約ソルバーは型レベルのプログラムを実行しようとし、特定の式がその通常の形式に等しいという証拠の小さな銀色の痕跡を生成します。この証拠生成方法は少し予測不可能で、必然的に不完全です。たとえば、恐ろしく見える再帰を避けますが、それはおそらく賢明です。心配する必要がないことの 1 つは、タイプチェッカーでの計算の実行です。タイプチェッカーはランタイム システムと同じ意味IOを与える必要はないことを覚えておいてください。launchMissiles
ヒンドリー・ミルナー文化
Hindley-Milner 型システムは、4 つの異なる区別の本当に素晴らしい一致を実現しますが、多くの人々がそれらの区別の違いを見分けることができず、一致は必然であると想定するという残念な文化的副作用があります。私は何を言っているのでしょうか。
- terms vs types
- explicitly written things vs implicitly written things
- presence at run-time vs erasure before run-time
- non-dependent abstraction vs dependent quantification
We're used to writing terms and leaving types to be inferred...and then erased. We're used to quantifying over type variables with the corresponding type abstraction and application happening silently and statically.
You don't have to veer too far from vanilla Hindley-Milner before these distinctions come out of alignment, and that's no bad thing. For a start, we can have more interesting types if we're willing to write them in a few places. Meanwhile, we don't have to write type class dictionaries when we use overloaded functions, but those dictionaries are certainly present (or inlined) at run-time. In dependently typed languages, we expect to erase more than just types at run-time, but (as with type classes) that some implicitly inferred values will not be erased. E.g., vReplicate's numeric argument is often inferable from the type of the desired vector, but we still need to know it at run-time.
Which language design choices should we review because these coincidences no longer hold? E.g., is it right that Haskell provides no way to instantiate a forall x. t quantifier explicitly? If the typechecker can't guess x by unifiying t, we have no other way to say what x must be.
More broadly, we cannot treat "type inference" as a monolithic concept that we have either all or nothing of. For a start, we need to split off the "generalisation" aspect (Milner's "let" rule), which relies heavily on restricting which types exist to ensure that a stupid machine can guess one, from the "specialisation" aspect (Milner's "var" rule) which is as effective as your constraint solver. We can expect that top-level types will become harder to infer, but that internal type information will remain fairly easy to propagate.
Next Steps For Haskell
We're seeing the type and kind levels grow very similar (and they already share an internal representation in GHC). We might as well merge them. It would be fun to take * :: * if we can: we lost logical soundness long ago, when we allowed bottom, but type soundness is usually a weaker requirement. We must check. If we must have distinct type, kind, etc levels, we can at least make sure everything at the type level and above can always be promoted. It would be great just to re-use the polymorphism we already have for types, rather than re-inventing polymorphism at the kind level.
We should simplify and generalise the current system of constraints by allowing heterogeneousとa ~ bの種類が構文的に同一ではない (ただし、等しいことが証明できる)方程式。これは古い手法 (前世紀の私の論文で使用) であり、依存関係の処理がはるかに簡単になります。GADT の式に制約を表現できるため、昇格できるものに関する制限が緩和されます。ab
依存関数型を導入することで、シングルトン構築の必要性を排除する必要がありますpi x :: s -> t。このような型の関数は、明示的にsそこに生息するあらゆる表現に交差点型と項の言語（つまり変数、コンストラクタ、さらに後ほど追加）のラムダと適用は実行時に消去されないので、次のように書くことができます。
vReplicate :: pi n :: Nat -> x -> Vec n x
vReplicate Z x = VNil
vReplicate (S n) x = VCons x (vReplicate n x)
Natを で置き換えずに記述しますNatty。 のドメインはpi任意の昇格可能な型にすることができるため、GADT が昇格できる場合は、従属量指定子シーケンス (または de Briuijn が「望遠鏡」と呼んだもの) を記述できます。
pi n :: Nat -> pi xs :: Vec n x -> ...
必要な長さに。
これらのステップのポイントは複雑さを排除する脆弱なツールや扱いにくいエンコーディングで間に合わせるのではなく、より一般的なツールを直接操作することによって。現在の部分的な導入では、Haskell の依存型の利点が必要以上に高価になっています。
あまりにもハード？
依存型は多くの人を不安にさせます。私も不安になりますが、不安になるのは好きです。少なくとも、不安にならないのは難しいと思います。しかし、このトピックの周囲に無知の霧が漂っていることは、助けにはなりません。その理由の一部は、私たち全員がまだ学ぶべきことがたくさんあるという事実によるものです。しかし、それほど過激ではないアプローチの支持者は、常に事実を完全に確認することなく、依存型に対する恐怖をかき立てることで知られています。名前は挙げません。これらの「決定不可能な型チェック」、「チューリング不完全」、「フェーズの区別がない」、「型の消去がない」、「どこでも証明できる」などの神話は、ナンセンスであるにもかかわらず、根強く残っています。
依存型プログラムが常に正しいと証明されなければならないというわけではない。完全な仕様まで行かなくても、型に追加の不変条件を適用することで、プログラムの基本的な衛生状態を改善できる。この方向への小さなステップは、追加の証明義務をほとんどまたはまったく必要とせずに、はるかに強力な保証をもたらすことが多い。依存型プログラムが必然的に正しいというのは真実ではない。満杯証明については、実際私は自分のコードに証明が存在することを、私の定義に疑問を抱く。
なぜなら、表現力が増すと、私たちは正しいことだけでなく、汚いことを言う自由も得られるようになるからです。例えば、二分探索木を定義するには多くの下手な方法がありますが、だからといって、良い方法たとえそれを認めることが自尊心を傷つけるとしても、悪い経験は改善できないと思い込まないことが重要です。依存定義の設計は学習を要する新しいスキルであり、Haskell プログラマーだからといって自動的にエキスパートになるわけではありません。また、一部のプログラムが不正だとしても、他の人が公平である自由をなぜ否定するのでしょうか。
なぜ今でも Haskell を使う必要があるのでしょうか?
私は依存型が本当に好きですが、私のハッキング プロジェクトのほとんどはまだ Haskell で行われています。なぜでしょうか。Haskell には型クラスがあります。Haskell には便利なライブラリがあります。Haskell には、効果のあるプログラミングをうまく処理する機能があります (理想からは程遠いですが)。Haskell には産業用コンパイラがあります。依存型言語は、コミュニティとインフラストラクチャの成長のかなり初期の段階にありますが、メタプログラミングやデータ型ジェネリックなどの方法で、可能なことの実際の世代交代により、私たちはそこに到達するでしょう。しかし、依存型に向かう Haskell のステップの結果として人々が何をしているかを見回すだけで、現在の世代の言語を前進させることによっても多くのメリットが得られることがわかります。