36

既存の言語で行われた最新の実用的な変更について学ぶだけでなく、型の背後にある実際の理論を理解したいと思います（たとえば、HaskellやScalaの型システムがどのように機能するかだけではありません）。

この背景を理解するための最良の方法は何ですか？

4

1 に答える 1

60

型理論は大きな領域です。まず第一に、「タイプ」という用語は、ほとんど同じ基本的な考え方に使用されているにもかかわらず、いくつかの理由から、コンピュータサイエンスでは一種の誤称です。タイプは、ほとんど同じ理由で、多くのコンテキスト、哲学、コンピューターサイエンス、および数学で発生しました。数学の型の起源は、集合論を形式化しようとし、本質的なパラドックスにぶつかることから来ていますが、コンピュータサイエンスでも同様のパラドックスが発生します。（たとえば、私はこれに関するジラールのパラドックスを指摘するのが好きです）。

現時点でタイプを解釈する方法は、70年代から90年代にかけてコンピューターで普及したアイデアです。タイプは、フローに依存しない軽量の分析であり、作成するプログラムについて簡潔な論理的保証を行うことができます。これには型を使用できますが、実際には、プログラムが証明である高階述語論理のエンコードに至るまで、型を使用することができます。ここに行くと、証明を取り、計算コンポーネントを抽出し、それを「正しい」結果を計算するプログラムに変換できます（証明した定理に関して）。

ここから行くことができるいくつかの道があります：

  • ベンピアスのタイプとプログラミング言語のコピーを入手してください。 これは読むべき本であり、コンピュータサイエンスで最高の本の1つです。型が必要な理由と、型を使用してプログラムに制約を適用する方法についての理論について説明します。
  • プログラムのセマンティクスに関することを強制するために定期的に型を使用する言語を学びます。特に、OCaml、Haskell、またはAgdaを学ぶことができます。Haskellは現時点で最良の選択のようです。それは本当に魅力的で、本当にアクティブなユーザーコミュニティを作るかなりの数の拡張機能を持っています。実際、トップカンファレンスで公開された結果がわずか数年以内にコミュニティで広く使用されるようになることは非常に一般的です。
  • 建設的な型理論に基づいた定理証明器の使い方を学びます。私の意見では、これが型理論の背後にある本当の問題を理解する唯一の本当の方法です。CoqとIsabelleは現在、真の競争相手として際立っていますが、いくつかの良い選択肢があります。Coqには1つの大きな利点があります。BenPierceにもそれをカバーする本があります。 Software Foundationsは、プログラミング言語からの理論の量を詳細にカバーしており、それを使用して実際に物事を証明することができます。

また、いくつかの関連フィールドを調べることもできます。

  • 圏論は、このようなものの根底にある傾向がある数学です。たとえば、これらの言語で指定された（共）帰納的データ型を分類的に解釈することができます。
  • 論理。古き良き伝統的な論理を少し学ぶことは役に立ちますが、ベン・ピアスのSFの本を読むことで、必要なもののほとんどを理解できると確信しています。ただし、古いシステム（その後の計算と自然演繹）への参照はまだたくさんあります。
  • Haskellコミュニティについて学びましょう！私が言ったように、彼らは速く動いていて、コンピュータサイエンスのタイプについて深い質問をします。
  • プログラミング言語の優れた作品には、多くの優れた記事があります。

これを超えて学ぶための素晴らしい推奨事項がいくつかありますが、私は間違いなくベン・ピアスの本から始めます（フォローアップの本「タイプとコンピューターサイエンスの高度なトピック」に実際に触れたことはありませんが、それもおそらく興味深いものですあなたへ）。特に、自動推論ハンドブックに高次型理論に関する素晴らしい記事があったことを覚えています。

追伸、私はこの質問への答えは具体的には「プログラミング言語、哲学、または論理の博士号を取得する...」であると確信しています;-)

于 2012-06-15T19:54:01.703 に答える