「Haskell は徐々に依存型言語になりつつある」という意見を反映する情報源をいくつか見てきました。これは、言語拡張がますます進んでおり、Haskell がその一般的な方向に流されていることを意味しているように思われますが、まだそこにはありません。
私が知りたいことは主に2つあります。1つ目は、非常に簡単に言えば、「依存型言語であること」とは実際には何を意味するのでしょうか? (うまくいけば、あまり技術的ではありません。)
2 番目の質問は... 欠点は何ですか? つまり、人々は私たちがその方向に向かっていることを知っているので、それには何らかの利点があるに違いありません。とはいえ、私たちはまだそこに到達していないので、人々がずっと前に進むのを妨げる何らかのマイナス面があるに違いありません. 問題は複雑さの急激な増加であるという印象を受けます。しかし、依存型入力とは何かをよく理解していないので、よくわかりません。
私が知っていることは、依存型プログラミング言語について読み始めるたびに、テキストがまったく理解できないということです...おそらくそれが問題です。(?)
Haskell は、ある程度、依存型言語です。のおかげでより賢明に型付けされた型レベル データの概念があり、型レベル データにランタイム表現を与えるDataKindsいくつかの手段 ( ) があります。GADTsしたがって、実行時のものの値は効率的に typesに表示されます。これは、言語が依存的に型付けされることを意味します。
単純なデータ型は種類レベルに昇格されるため、それらに含まれる値を型で使用できます。したがって、典型的な例
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。対照的に、与えられた( toの)のnコピーを作成する関数を実装するのは、はるかにトリッキーです (つまり、不可能です)。xpurevApply<*>
vReplicate :: x -> Vec n x
実行時に作成するコピーの数を知ることが重要だからです。シングルトンを入力します。
data Natty :: Nat -> * where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
プロモート可能な型については、プロモートされた型にインデックスが付けられ、その値の実行時の複製が存在するシングルトン ファミリを構築できます。Natty ntype-level の実行時コピーのタイプです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辞書を交換するためのかなり厄介なプロセスがあります。さらに、Nattyis not 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 つの方程式のそれぞれで、両側に kind があり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) 。 、しかしそれはただの偶然です！
もう 1 つ欠けているのは、実際には、型を値でインデックス化する新しい機能を利用するライブラリです。この素晴らしい新しい世界で何をし、何Functor
になるのでしょうか? Monad考え中ですが、まだまだやることはたくさんあります。
ほとんどの依存型プログラミング言語と同様に、Haskell には2 つの 操作上のセマンティクスがあります。ランタイム システムがプログラムを実行する方法 (閉じた式のみ、型消去後、高度に最適化) と、タイプチェッカーがプログラムを実行する方法 (型ファミリ、「型クラス プロローグ」、開いた式) があります。Haskell の場合、実行されるプログラムが異なる言語であるため、通常、この 2 つを混同することはありません。依存型付けされた言語には、同じプログラム言語に対して個別のランタイム モデルと静的実行モデルがありますが、心配する必要はありません。メカニズムはあなたに与えます; これは、少なくとも Edwin Brady のコンパイラが行っていることです (ただし、Edwin は不必要に重複した値や、型や証明を消去します)。フェーズの区別は、もはや構文カテゴリの区別ではないかもしれませんが、 健在です。
依存型付けされた言語は、全体として、タイプチェッカーが長い待ち時間よりも悪いことを恐れずにプログラムを実行できるようにします。Haskell がより従属的に型付けされるにつれて、その静的実行モデルはどうあるべきかという問題に直面します。1 つのアプローチは、静的な実行をすべての関数に制限することです。これにより、同じ自由な実行が可能になりますが、(少なくとも型レベルのコードでは) データと codata を区別する必要が生じる可能性があります。終了または生産性を強制します。しかし、それが唯一のアプローチではありません。計算だけで得られる式が少なくなるという代償を払って、プログラムを実行するのをためらう、はるかに弱い実行モデルを自由に選択できます。実際、それが GHC が実際に行っていることです。GHC コアの型付け規則では、実行について言及されていません
ただし、方程式の証拠をチェックするためだけです。コアに変換するとき、GHC の制約ソルバーは型レベルのプログラムを実行しようとし、与えられた式がその正規形に等しいという証拠の小さな銀色の跡を生成します。この証拠生成方法は少し予測不可能であり、必然的に不完全です。たとえば、恐ろしく見える再帰を恥ずかしがり屋で戦いますが、それはおそらく賢明です。心配する必要のないことの 1 つは、タイプチェッカーでの計算の実行です。タイプチェッカーは、ランタイム システムと同じ意味IO
を与える必要がないことを覚えておいて
ください。launchMissiles
Hindley-Milner 型システムは、4 つの異なる区別の真に驚くべき偶然の一致を実現しますが、残念なことに、多くの人々が区別の違いを認識できず、偶然が必然であると想定するという文化的な副作用があります! 私は何について話しているのですか？
私たちは、用語を書き、型を推論して消去することに慣れています。私たちは、対応する型の抽象化と適用が黙って静的に行われる型変数の量化に慣れています。
これらの区別が一致しなくなる前に、バニラの Hindley-Milner から大きく離れる必要はありません。それは悪いことではありません。手始めに、いくつかの場所に書く気があれば、もっと興味深い型を持つことができます。一方、オーバーロードされた関数を使用する場合、型クラス辞書を作成する必要はありませんが、それらの辞書は実行時に必ず存在 (またはインライン化) されます。依存型付け言語では、実行時に型だけでなくそれ以上のものを消去することを期待していますが、(型クラスと同様に) 一部の暗黙的に推論された値は消去されません。たとえば、vReplicateの数値引数は、多くの場合、目的のベクトルの型から推測できますが、実行時にそれを知る必要があります。
これらの偶然が成り立たなくなったため、どの言語設計の選択を検討する必要がありますか? たとえば、Haskell がforall x. t量指定子を明示的にインスタンス化する方法を提供していないというのは正しいでしょうか? xタイプチェッカーが unifiyingで推測できない場合、t何xが必要かを判断する方法は他にありません。
もっと広く言えば、「型推論」をモノリシックな概念として扱うことはできません。まず、「一般化」の側面 (Milner の「let」規則) を分割する必要があります。これは、「特殊化」の側面 (Milner の「var " ルール) は、制約ソルバーと同じくらい効果的です。トップレベルの型は推測が難しくなると予想できますが、内部の型情報は依然としてかなり簡単に伝播されます。
type と kind のレベルが非常に似通ったものになっているのを私たちは見ています (そして、それらは GHC の内部表現をすでに共有しています)。それらをマージすることもできます。できれば面白いと思います:かなり前に底を許したときに論理的な* :: *健全性を失い
ましたが、型の
健全性は通常、より弱い要件です。確認する必要があります。異なるタイプ、種類などのレベルが必要な場合は、少なくともタイプ レベル以上のすべてを常に昇格できるようにすることができます。種類レベルでポリモーフィズムを再発明するのではなく、型に対してすでに持っているポリモーフィズムを再利用するだけでよいでしょう。
との種類が構文的に同一で
はない (ただし、等しいことが証明できる)異種方程式を許可することにより、現在の制約システムを単純化して一般化する必要があります。これは、依存関係への対処をはるかに容易にする古い手法です (私の論文では、前世紀)。GADT で式に対する制約を表現できるため、昇格できるものに対する制限を緩和できます。a ~ bab
従属関数型 を導入することで、シングルトン構築の必要性を排除する必要があり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 の型クラスとパラメトリック ポリモーフィズムで既に可能)、値の型をパラメーター化できます (厳密に言えば、Haskell ではまだ可能ではありません)。 、DataKinds非常に近くなりますが）。
編集: どうやら、この時点から、私は間違っていたようです (@pigworker のコメントを参照)。この残りの部分は、私が受けた神話の記録として保存します。:P
私が聞いたところによると、完全に依存する型付けに移行する際の問題は、Haskell を消去された型を持つ効率的なマシン コードにコンパイルできるようにする、型レベルと値レベルの間のフェーズ制限が壊れるということです。私たちの現在の技術レベルでは、依存型付き言語は、ある時点で (すぐに、または依存型バイトコードなどにコンパイルされた後に) インタープリターを通過する必要があります。
これは必ずしも根本的な制限ではありませんが、個人的には、この点に関して有望に見えるが、まだ GHC に組み込まれていない現在の研究を認識していません。詳しい方がいらっしゃいましたら、訂正いただけると幸いです。
John 依存型に関するもう 1 つのよくある誤解は、データが実行時にしか利用できない場合には動作しないということです。getLine の例を実行する方法は次のとおりです。
data Some :: (k -> *) -> * where
Like :: p x -> Some p
fromInt :: Int -> Some Natty
fromInt 0 = Like Zy
fromInt n = case fromInt (n - 1) of
Like n -> Like (Sy n)
withZeroes :: (forall n. Vec n Int -> IO a) -> IO a
withZeroes k = do
Like n <- fmap (fromInt . read) getLine
k (vReplicate n 0)
*Main> withZeroes print
5
VCons 0 (VCons 0 (VCons 0 (VCons 0 (VCons 0 VNil))))
編集：うーん、それはピッグワーカーの答えへのコメントであるはずでした。私は明らかにSOで失敗します。
pigworker は、依存型に向かうべき理由について優れた議論を提供しています。(b) Haskell がすでに行っていることの多くを実際に単純化するでしょう。
「どうして？」については。質問、私が思ういくつかのポイントがあります。最初のポイントは、依存型の背後にある基本的な概念は簡単ですが (型が値に依存することを許可する)、その基本的な概念の影響は微妙で深遠です。たとえば、値と型の区別は今も健在です。しかし、それらの違いを議論することは遠くなりますyer Hindley ---Milner や System F よりもニュアンスがあります。これはある程度、従属型が根本的に難しいという事実によるものです (たとえば、一次論理は決定不可能です)。しかし、より大きな問題は、何が起こっているのかを把握して説明するための適切な語彙が不足していることだと思います. 従属型について学ぶ人が増えるにつれて、より良い語彙が開発され、根底にある問題がまだ難しい場合でも物事が理解しやすくなります。
2 つ目のポイントは、Haskell が成長しているという事実に関係しています。依存型に向かって。私たちはその目標に向けて漸進的に進歩していますが、実際にはそこに到達していないため、漸進的なパッチの上に漸進的なパッチを持つ言語に行き詰まっています。新しいアイデアが一般的になるにつれて、同じようなことが他の言語でも起こりました。Java には (パラメトリックな) ポリモーフィズムがありませんでした。彼らが最終的にそれを追加したとき、それは明らかにいくつかの抽象化リークと不自由な力を伴う漸進的な改善でした. サブタイピングとポリモーフィズムを混在させることは本質的に困難です。しかし、それが Java Generics がそのように機能する理由ではありません。古いバージョンの Java に対する漸進的な改善であるという制約があるため、これらはそのように機能します。同上、OOP が発明され、人々が「目的」を書き始めた時代にさかのぼります。C (Objective-C と混同しないでください) などです。覚えておいてください。C++ は、C の厳密なスーパーセットであるという装いで始まりました。新しいパラダイムを追加するには、常に言語を新たに定義する必要があります。そうしないと、複雑な混乱を招くことになります。ここで私が言いたいのは、Haskell に真の依存型を追加するには、言語をある程度骨抜きにして再構築する必要があるということです。しかし、私たちが行ってきた漸進的な進歩は短期的には安く見えるのに対し、そのようなオーバーホールにコミットするのは本当に難しい. 実際、GHC をハッキングする人はそれほど多くありませんが、存続させなければならない大量のレガシー コードがあります。これが、DDC、Cayenne、Idris などのスピンオフ言語が非常に多い理由の 1 つです。C++ は、C の厳密なスーパーセットであるという装いで始まりました。新しいパラダイムを追加するには、常に言語を新たに定義する必要があります。そうしないと、複雑な混乱に陥ります。ここで私が言いたいのは、Haskell に真の依存型を追加するには、言語をある程度骨抜きにして再構築する必要があるということです。しかし、私たちが行ってきた漸進的な進歩は短期的には安く見えるのに対し、そのようなオーバーホールにコミットするのは本当に難しい. 実際、GHC をハッキングする人はそれほど多くありませんが、存続させなければならない大量のレガシー コードがあります。これが、DDC、Cayenne、Idris などのスピンオフ言語が非常に多い理由の 1 つです。C++ は、C の厳密なスーパーセットであるという装いで始まりました。新しいパラダイムを追加するには、常に言語を新たに定義する必要があります。そうしないと、複雑な混乱に陥ります。ここで私が言いたいのは、Haskell に真の依存型を追加するには、言語をある程度骨抜きにして再構築する必要があるということです。しかし、私たちが行ってきた漸進的な進歩は短期的には安く見えるのに対し、そのようなオーバーホールにコミットするのは本当に難しい. 実際、GHC をハッキングする人はそれほど多くありませんが、存続させなければならない大量のレガシー コードがあります。これが、DDC、Cayenne、Idris などのスピンオフ言語が非常に多い理由の 1 つです。または、複雑な混乱に陥ります。ここで私が言いたいのは、Haskell に真の依存型を追加するには、言語をある程度骨抜きにして再構築する必要があるということです。しかし、私たちが行ってきた漸進的な進歩は短期的には安く見えるのに対し、そのようなオーバーホールにコミットするのは本当に難しい. 実際、GHC をハッキングする人はそれほど多くありませんが、存続させなければならない大量のレガシー コードがあります。これが、DDC、Cayenne、Idris などのスピンオフ言語が非常に多い理由の 1 つです。または、複雑な混乱に陥ります。ここで私が言いたいのは、Haskell に真の依存型を追加するには、言語をある程度骨抜きにして再構築する必要があるということです。しかし、私たちが行ってきた漸進的な進歩は短期的には安く見えるのに対し、そのようなオーバーホールにコミットするのは本当に難しい. 実際、GHC をハッキングする人はそれほど多くありませんが、存続させなければならない大量のレガシー コードがあります。これが、DDC、Cayenne、Idris などのスピンオフ言語が非常に多い理由の 1 つです。そのようなオーバーホールにコミットするのは本当に難しいですが、私たちが行ってきた漸進的な進歩は短期的には安くなっているようです. 実際、GHC をハッキングする人はそれほど多くありませんが、存続させなければならない大量のレガシー コードがあります。これが、DDC、Cayenne、Idris などのスピンオフ言語が非常に多い理由の 1 つです。そのようなオーバーホールにコミットするのは本当に難しいですが、私たちが行ってきた漸進的な進歩は短期的には安くなっているようです. 実際、GHC をハッキングする人はそれほど多くありませんが、存続させなければならない大量のレガシー コードがあります。これが、DDC、Cayenne、Idris などのスピンオフ言語が非常に多い理由の 1 つです。