既存の言語で行われた最新の実用的な変更について学ぶだけでなく、型の背後にある実際の理論を理解したいと思います(たとえば、HaskellやScalaの型システムがどのように機能するかだけではありません)。
この背景を理解するための最良の方法は何ですか?
既存の言語で行われた最新の実用的な変更について学ぶだけでなく、型の背後にある実際の理論を理解したいと思います(たとえば、HaskellやScalaの型システムがどのように機能するかだけではありません)。
この背景を理解するための最良の方法は何ですか?
型理論は大きな領域です。まず第一に、「タイプ」という用語は、ほとんど同じ基本的な考え方に使用されているにもかかわらず、いくつかの理由から、コンピュータサイエンスでは一種の誤称です。タイプは、ほとんど同じ理由で、多くのコンテキスト、哲学、コンピューターサイエンス、および数学で発生しました。数学の型の起源は、集合論を形式化しようとし、本質的なパラドックスにぶつかることから来ていますが、コンピュータサイエンスでも同様のパラドックスが発生します。(たとえば、私はこれに関するジラールのパラドックスを指摘するのが好きです)。
現時点でタイプを解釈する方法は、70年代から90年代にかけてコンピューターで普及したアイデアです。タイプは、フローに依存しない軽量の分析であり、作成するプログラムについて簡潔な論理的保証を行うことができます。これには型を使用できますが、実際には、プログラムが証明である高階述語論理のエンコードに至るまで、型を使用することができます。ここに行くと、証明を取り、計算コンポーネントを抽出し、それを「正しい」結果を計算するプログラムに変換できます(証明した定理に関して)。
ここから行くことができるいくつかの道があります:
また、いくつかの関連フィールドを調べることもできます。
これを超えて学ぶための素晴らしい推奨事項がいくつかありますが、私は間違いなくベン・ピアスの本から始めます(フォローアップの本「タイプとコンピューターサイエンスの高度なトピック」に実際に触れたことはありませんが、それもおそらく興味深いものですあなたへ)。特に、自動推論ハンドブックに高次型理論に関する素晴らしい記事があったことを覚えています。
追伸、私はこの質問への答えは具体的には「プログラミング言語、哲学、または論理の博士号を取得する...」であると確信しています;-)