[解決済み] なぜ依存型でないのか？

質問

Haskellは徐々に依存型言語になりつつある、という意見をいくつかのソースで目にしました。その意味するところは、より多くの言語拡張により、Haskellはその一般的な方向へ向かっているが、まだそこに到達していないということです。

知りたいことは基本的に2つあります。1つ目は、簡単に言うと、「依存型言語であること」とは、実際にはどのようなことなのか、ということです。 意味 ? (できれば、あまり専門的なことは抜きにして)。

2つ目の質問は...欠点は何でしょうか？つまり、人々は私たちがその方向に向かっていることを知っているのですから、何か利点があるはずです。しかし、まだそこに到達していないのですから、人々がその道を突き進むのを阻む何らかの欠点があるはずです。問題は、複雑さが急激に増すことだという印象があります。しかし、従属型付けが何であるかをよく理解していないため、確かなことはわかりません。

私の場合 する 依存型プログラミング言語について読み始めると、いつも文章がまったく理解できないんです......。おそらく、それが問題なのでしょう。(?)

どのように解決するのか？

依存型付けは実際には値と型のレベルを統一するだけなので，型に値をパラメタライズすることができ（Haskellでは型クラスとパラメトリック多相性ですでに可能），値に型をパラメタライズできる（厳密に言えば，Haskellではまだ可能ではない，ただし DataKinds は非常に近くなっています)。

編集する どうやら、ここから先は、私の勘違いだったようです（@pigworkerさんのコメント参照）。 この続きは、私が食べさせられてきた神話の記録として保存しておきます :P

私が聞いたところによると、完全な依存型付けに移行することの問題は、Haskellを消去された型で効率的な機械語にコンパイルできるようにしている、型レベルと値レベルの間の位相制約を壊してしまうことです。 現在の技術レベルでは、依存型付けされた言語が しなければならない ある時点で（すぐに、あるいは依存型バイトコードなどにコンパイルされた後に）インタープリタを経由する。

これは必ずしも根本的な制約ではありませんが、この点で有望と思われる研究であっても、まだGHCに取り込まれていないものは、個人的には知りません。 もし他にもっと知っている人がいれば、訂正していただけると幸いです。