型推論

型推論は、型再構築とも呼ばれ、^{[1] : 320}形式言語における式の型の自動検出を指します。これにはプログラミング言語や数学的型システムだけでなく、コンピュータサイエンスや言語学のいくつかの分野における自然言語も含まれます。

型付けされた言語では、用語の型によって、その言語で使用できる方法と使用できない方法が決まります。たとえば、英語と「sing _」というフレーズの空白を埋めることができる用語について考えてみましょう。「a song」という用語には歌える型があるため、空白に入れて意味のあるフレーズ「sing a song」を形成できます。一方、「a friend」という用語には歌える型がないため、「sing a friend」は意味がありません。せいぜい比喩かもしれません。型規則を曲げることは詩的な言語の特徴です。

用語の型は、その用語に関連する操作の解釈にも影響します。たとえば、「a song」は構成可能な型なので、「write a song」というフレーズで作成されたものとして解釈します。一方、「a friend」は受信者型なので、「write a friend」というフレーズの宛先として解釈します。通常の言語では、「write a song」が曲に手紙を宛てることを意味する場合や、「write a friend」が紙に友人宛ての下書きを意味する場合、私たちは驚くでしょう。

異なるタイプの用語が、実質的に同じものを指すこともあります。たとえば、「物干しロープを掛ける」はロープを使用するという意味ですが、「ひもを掛ける」はロープを片付けるという意味になります。ただし、文脈上、「物干しロープ」と「ひも」はどちらも、単にタイミングが異なるだけで、同じロープを指している可能性があります。

型付けは、オブジェクトが一般化しすぎないようにするためによく使用されます。たとえば、型システムがすべての数値を同じものとして扱う場合、プログラマーが誤って4「4 秒」を意味するはずのコードを「4 メートル」と解釈すると、実行時に問題が発生するまで、その間違いを警告されません。単位を型システムに組み込むことで、これらの間違いをはるかに早い段階で検出できます。別の例として、ラッセルのパラドックスは、何でもセット要素になることができ、どんな述語でもセットを定義できる場合に発生しますが、より慎重な型付けによって、このパラドックスを解決する方法がいくつか提供されます。実際、ラッセルのパラドックスは、型理論の初期のバージョンのきっかけとなりました。

用語の型を取得する方法はいくつかあります。

• このタイプは、文章の外部から提供される場合があります。たとえば、話し手が英語で「a song」に言及する場合、通常、話し手は聞き手に「a song」が歌える、作曲できると伝える必要はありません。その情報は、話し手が共有する背景知識の一部です。
• 型は明示的に宣言できます。たとえば、プログラマーはdelay: seconds := 4コード内に のような文を記述します。ここで、コロンは項とその型をマークするための慣例的な数学記号です。つまり、この文は をdelay値 に設定するだけでなく4、delay: secondsの部分は の型が秒単位の時間量であることを示しますdelay。
• タイプはコンテキストから推測できます。たとえば、「I buy it for a song」というフレーズでは、「a song」という用語に「singable」や「composable」などのタイプを割り当てようとすると意味不明になりますが、「amount of currency」というタイプはうまくいきます。したがって、言われなくても、ここでの「song」は英語の慣用句「for a song」のように「ほとんど何もない」という意味であり、「通常は歌詞のある音楽」という意味ではないと結論付けることができます。

特にプログラミング言語では、コンピューターが利用できる共有の背景知識があまりない場合があります。明示的に型付けされた言語では、ほとんどの型を明示的に宣言する必要があります。型推論は、この負担を軽減し、コンピューターがコンテキストから推測できる型を宣言する必要がないように作成者を解放することを目的としています。

型付けでは、式 E は型 T と対比され、正式には E : T と記述されます。通常、型付けは特定のコンテキスト内でのみ意味を持ちますが、ここでは省略されています。

この設定では、次の質問が特に興味深いです。

1. E : T? この場合、式 E と型 T の両方が与えられます。では、 E は本当に T でしょうか? このシナリオは型チェックとして知られています。
2. E : _? ここでは、式のみがわかっています。E の型を導出する方法があれば、型推論が達成されます。
3. _ : T? 逆です。型だけが与えられた場合、それを表す式はありますか、それとも型には値がありませんか? T の例はありますか? これは、型の居住として知られています。

単純に型付けされたラムダ計算の場合、3 つの質問はすべて決定可能です。より表現力豊かな型が許可されている場合、状況はそれほど快適ではありません。

型は、一部の強く 静的に型付けされた言語に存在する機能です。一般的に関数型プログラミング言語の特徴であることが多いです。型推論を含む言語には、 C23、^[2] C++11、^[3] C#（バージョン3.0以降）、Chapel、Clean、Crystal、D、F#、^[4] FreeBASIC、Go、Haskell、Java（バージョン10以降）、Julia、^[5] Kotlin、^[6] ML、Nim、OCaml、Opa、Q#、RPython、Rust、^[7] Scala、^[8] Swift、^[9] TypeScript、^[10] Vala、^[11] Dart、^[12]、Visual Basic ^[13]（バージョン9.0以降）などがあります。そのほとんどは単純な型の推論を使用していますが、Hindley–Milner型システムはより完全な型推論を提供できます。型を自動的に推論する機能により、多くのプログラミング タスクが容易になり、プログラマーは型チェックを許可しながら 型注釈を省略できるようになります。

一部のプログラミング言語では、すべての値のデータ型がコンパイル時に明示的に宣言され、特定の式が実行時に取ることができる値が制限されます。ジャストインタイム コンパイルにより、実行時とコンパイル時の区別がますます曖昧になっています。ただし、歴史的には、値の型が実行時にのみ判明する場合、これらの言語は動的型付けされます。その他の言語では、式の型はコンパイル時にのみ判明し、これらの言語は静的型付けされます。ほとんどの静的型付け言語では、関数とローカル変数の入力型と出力型は通常、型注釈によって明示的に指定する必要があります。たとえば、ANSI Cでは次のようになります。

int add_one ( int x ) { int result ; /* 整数結果を宣言する */   
      

    結果= x + 1 ;結果を返す; }    
     

この関数定義のシグネチャは、 が 1 つの引数(整数 )を受け取り、整数を返す関数であることを宣言します。 は、ローカルint add_one(int x)変数が整数であることを宣言します。 型推論をサポートする仮想言語では、コードは次のように記述される可能性があります。 add_oneint result;result

add_one ( x ) { var result ; /* 推論された型変数の結果 */ var result2 ; /* 推論された型変数の結果 #2 */ 
       
      

    result = x + 1 ; result2 = x + 1.0 ; /* この行は動作しません (提案された言語では) */ return result ; }    
          
     

これは、 Dart言語でコードが記述される方法と同じですが、以下に説明するように、いくつかの追加の制約が適用されます。コンパイル時にすべての変数の型を推論することが可能です。上記の例では、定数が整数型であるため、コンパイラはresultと が整数型であると推論し、したがって は関数です。変数は正当な方法で使用されていないため、型はありません。 x1add_oneint -> intresult2

最後の例が書かれた架空の言語では、反対の情報がない場合、コンパイラは が+2 つの整数を受け取り、 1 つの整数を返すものと想定します。(これは、たとえばOCamlでの動作です。) このことから、型推論器は の型がx + 1整数であると推論できます。つまり、 は整数resultであり、したがって の戻り値もadd_one整数です。同様に、 は+両方の引数が同じ型である必要があるため、 はx整数でなければならず、したがって はadd_one引数として 1 つの整数を受け入れます。

しかし、次の行では、result2 は浮動小数点演算1.0で小数を加算して計算されるため、整数式と浮動小数点式の両方で の使用に競合が生じます。このような状況に対する正しい型推論アルゴリズムは 1958 年から知られており、1982 年から正しいことが知られています。このアルゴリズムは、以前の推論を再検討し、最初から最も一般的な型 (この場合は浮動小数点) を使用します。ただし、これには悪影響が生じる可能性があります。たとえば、最初から浮動小数点を使用すると、整数型では発生しなかった精度の問題が発生する可能性があります。 x

しかし、多くの場合、バックトラックできず、このような状況ではエラー メッセージを生成する退化した型推論アルゴリズムが使用されます。前述の浮動小数点精度の問題で示されているように、型推論はアルゴリズム的に常に中立であるとは限らないため、この動作は好ましい場合があります。

中程度の一般性のアルゴリズムは、result2 を浮動小数点変数として暗黙的に宣言し、加算によって暗黙的にx浮動小数点に変換します。呼び出しコンテキストが浮動小数点引数を決して提供しない場合は、これが正しい可能性があります。このような状況は、型変換を伴わない型推論と、多くの場合制限なしにデータを別のデータ型に強制する 暗黙的な型変換との違いを示しています。

最後に、複雑な型推論アルゴリズムの大きな欠点は、結果として得られる型推論の解決が人間にとって明らかではないことです (特にバックトラッキングのため)。コードは主に人間が理解できるように意図されているため、これは有害となる可能性があります。

最近登場したジャストインタイム コンパイルにより、さまざまな呼び出しコンテキストによって提供される引数の型がコンパイル時にわかるハイブリッド アプローチが可能になり、同じ関数のコンパイル済みバージョンを大量に生成できるようになりました。コンパイルされた各バージョンは、異なる型セットに合わせて最適化できます。たとえば、JIT コンパイルでは、add_oneのコンパイル済みバージョンが少なくとも 2 つ存在できます。

整数入力を受け入れ、暗黙的な型変換を使用するバージョン。

浮動小数点数を入力として受け入れ、全体にわたって浮動小数点命令を使用するバージョン。

型推論とは、コンパイル時に式の型を部分的または完全に自動的に推論する機能です。コンパイラは、明示的な型注釈が与えられていなくても、変数の型や関数の型シグネチャを推論できることがよくあります。多くの場合、型推論システムが十分に堅牢であるか、プログラムまたは言語が十分に単純であれば、プログラムから型注釈を完全に省略することができます。

式の型を推論するために必要な情報を取得するために、コンパイラは、その部分式に与えられた型注釈の集約とその後の縮小としてこの情報を収集するか、さまざまな原子値の型を暗黙的に理解することによって収集します (例: true : Bool、42 : Integer、3.14159 : Real など)。型推論言語のコンパイラが型注釈なしで完全にプログラムをコンパイルできるのは、式が暗黙的に型付けされた原子値に最終的に縮小されることを認識することによってです。

高階プログラミングや多態性の複雑な形態では、コンパイラが常に推論できるとは限らず、曖昧さを解消するために型注釈が必要になることがあります。たとえば、多態的再帰による型推論は決定不可能であることが知られています。さらに、明示的な型注釈を使用すると、コンパイラが推論した型よりも具体的な（より高速で小さい）型を使用するように強制することで、コードを最適化できます。^[14]

型推論のいくつかの方法は、制約充足^[15]または満足可能性法理論^[16]に基づいています。

たとえば、Haskell関数はmapリストの各要素に関数を適用し、次のように定義できます。

map f [] = [] map f ( first : rest ) = f first : map f rest    
         

( :Haskell では、consはヘッド要素とリストの末尾をより大きなリストに構造化するか、空でないリストをヘッド要素と末尾に分解することを表します。これは、数学やこの記事の他の箇所のように「of type」を表すものではありません。Haskell では、::代わりに「of type」演算子が記述されます。)

関数の型推論はmap次のように行われます。はmap2 つの引数を取る関数なので、その型は という形式に制限されます。Haskell では、パターンと は常にリストと一致するため、2 番目の引数は何らかの型 に対してリスト型でなければなりません。その最初の引数は引数 に適用されます。引数 は、リスト引数 の型に対応する型 を持つ必要があります。したがって、何らかの型 に対して（は「型である」という意味です）。最終的に の戻り値はを生成するものであれば何でも のリストなので、 となります。 a -> b -> c[](first:rest)b = [d]dffirstdf :: d -> e::emap ff[e]

部分をまとめると になります。型変数には特別なことは何もないので、次のように書き直すことができます。 map :: (d -> e) -> [d] -> [e]

マップ: :( a- > b ) -> [ a ] -> [ b ]        

これ以上の制約は適用されないため、これは最も一般的な型でもあることがわかります。 の推論された型はパラメトリック多態的mapであるため、 の引数と結果の型は推論されず、型変数として残されます。そのため、実際の型が各呼び出しで一致している限り、さまざまな型の関数とリストに適用できます。 fmap

コンパイラなどのプログラムで使用されるアルゴリズムは、上記の非公式に構造化された推論と同等ですが、もう少し冗長で体系的です。正確な詳細は、選択した推論アルゴリズムによって異なります (最もよく知られているアルゴリズムについては、次のセクションを参照してください) が、次の例は一般的な考え方を示しています。ここでも、 の定義から始めますmap。

map f [] = [] map f ( first : rest ) = f first : map f rest    
         

(ここでも、 は:Haskell のリスト コンストラクターであり、「of type」演算子ではないことに注意してください。Haskell では、代わりに と表記されます::。)

まず、個々の用語ごとに新しい型変数を作成します。

• αmap推論したいの型を表します。
• βf最初の式の のタイプを表します。
• [γ][]最初の式の左側ののタイプを表します。
• [δ][]最初の式の右側ののタイプを表します。
• εf2番目の式の のタイプを表します。
• ζ -> [ζ] -> [ζ]:最初の式の左側のの型を表します。(このパターンはその定義からわかります。)
• ηの型を表すものとしますfirst。
• θの型を表すものとしますrest。
• ι -> [ι] -> [ι]:最初の式の右側ののタイプを表します。

次に、これらの項から構築された部分式に新しい型変数を作成し、それに応じて呼び出される関数の型を制限します。

• κは の型を表します。 と結論付けることができます。ここで、「類似」記号は「と統合する」という意味です。つまり、 の型は、と のリストを受け取り を返す関数の型と互換性がある必要があるということです。map f []α ~ β -> [γ] -> κ~αmapβγκ
• λは の型を表すものとする。 と結論づけられる。(first:rest)ζ -> [ζ] -> [ζ] ~ η -> θ -> λ
• μは の型を表すものとする。 と結論づけられる。map f (first:rest)α ~ ε -> λ -> μ
• νは の型を表すものとする。 と結論づけられる。f firstε ~ η -> ν
• ξは の型を表すものとする。 と結論づけられる。map f restα ~ ε -> θ -> ξ
• οは の型を表すものとする。 と結論づけられる。f first : map f restι -> [ι] -> [ι] ~ ν -> ξ -> ο

また、各方程式の左辺と右辺が互いに統一されるように制約します。κ ~ [δ]全体μ ~ οとして、解くべき統一システムは次のとおりです。

α ~ β -> [γ] -> κ
ξ -> [ξ] -> [ξ] ~ η -> θ -> λ
α ~ ε -> λ -> μ
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο
κ ~ [δ]
μ ～ ο

次に、変数が削除できなくなるまで代入します。正確な順序は重要ではありません。コードが型チェックされれば、どのような順序でも同じ最終形式になります。まず、と をο代入μしてみましょう。 [δ]κ

α ~ β -> [γ] -> [δ]
ξ -> [ξ] -> [ξ] ~ η -> θ -> λ
α ~ ε -> λ -> ο
ε ~ η -> ν
α ~ ε -> θ -> ξ
ι -> [ι] -> [ι] ~ ν -> ξ -> ο

ζをη、[ζ]およびθをλ、ιおよび をν、および[ι]をに置き換えるとξ、οのような型コンストラクタは引数が 反転可能であるため、すべて可能になります。· -> ·

α ~ β -> [γ] -> [δ]
α ~ ε -> [ζ] -> [ι]
ε ~ ζ -> ι

ζ -> ιをε、β -> [γ] -> [δ]を に代入し、2 番目の制約を維持して最後に α回復できるようにします。α

α ~ (ι -> ι) -> [ι] -> [ι]
β -> [γ] -> [δ] ~ (ι -> ι) -> [ι] -> [ι]

そして最後に、のような型コンストラクタは可逆(ζ -> ι)なので、をβおよびをζに置き換えると、2 番目の制約に固有のすべての変数が削除されます。 γιδ[·]

α ~ (ι -> ι) -> [ι] -> [ι]

これ以上の置換は不可能であり、再ラベル付けすると、詳細を調べずに見つけたものと同じ が得られます。 map :: (a -> b) -> [a] -> [b]

型推論を実行するために最初に使用されたアルゴリズムは、現在では非公式にHindley-Milnerアルゴリズムと呼ばれていますが、このアルゴリズムは正確にはDamasとMilnerに帰属するべきです。^{[17]これは伝統的に}型再構築 とも呼ばれています。^{[1] : 320}用語がHindley-Milner型付け規則に従って適切に型付けされている場合、規則は用語の主要な型付けを生成します。この主要な型付けを発見するプロセスが「再構築」のプロセスです。

このアルゴリズムの起源は、1958年にHaskell CurryとRobert Feysによって考案された単純型付きラムダ計算の型推論アルゴリズムです。 ^[要出典] 1969年にJ. Roger Hindleyはこの研究を拡張し、彼らのアルゴリズムが常に最も一般的な型を推論することを証明しました。1978年にRobin Milner ^[18]は、Hindleyの研究とは独立して、同等のアルゴリズムであるAlgorithm Wを提供しました。1982年にLuis Damas ^[17]は最終的にMilnerのアルゴリズムが完全であることを証明し、多態的参照を持つシステムをサポートするように拡張しました。

設計上、型推論は最も一般的な適切な型を推論します。ただし、多くの言語、特に古いプログラミング言語では、型システムがやや不健全であるため、より一般的な型を使用することが必ずしもアルゴリズム的に中立であるとは限りません。典型的なケースは次のとおりです。

• 浮動小数点型は整数型の一般化として考えられています。実際、浮動小数点演算には整数とは異なる精度とラッピングの問題があります。
• バリアント/動的型は、演算子オーバーロードの選択に影響する場合、他の型の一般化として考慮されます。たとえば、演算子+は整数を追加しますが、バリアントが整数を保持している場合でも、バリアントを文字列として連結する場合があります。

型推論アルゴリズムは、プログラミング言語だけでなく自然言語の解析にも使用されています。 ^{[19] [20] [21]型推論アルゴリズムは、一部の}文法誘導^{[22] [23]}や自然言語の制約ベース文法システムでも使用されています。 ^[24]

• ロジャー・ヒンドリーによるアーカイブされた電子メールメッセージ、型推論の歴史を説明
• Michael Schwartzbach による「Polymorphic Type Inference」では、ポリモーフィック型推論の概要が説明されています。
• Luca Cardelli による基本的な型チェックの論文。アルゴリズムについて説明し、Modula-2での実装も含まれています。
• Scalaでの Hindley–Milner 型推論の実装、Andrew Forrest 著 (2009 年 7 月 30 日取得)
• Perl 5 での Hindley-Milner の実装、Nikita Borisov 著、 Wayback Machineより(2007 年 2 月 18 日アーカイブ)
• Hindley-Milner とは何か? (そしてなぜそれがクールなのか?) Hindley–Milner の説明、Scala の例