Loading article…
型理論では、型推論（型再構築と呼ばれることもある）は式の型を自動的に検出することです。[ 1 ] : 320これにはプログラミング言語や数学的型システムだけでなく、コンピュータ科学や言語学のいくつかの分野では自然言語も 含まれます。
型付け可能性は、型推論とほぼ同義語として使われることがあるが、一部の著者は、型付け可能性を（はい/いいえの答えがある）決定問題として、型推論を項の実際の型を計算することとして区別している。[ 2 ]
型付けされた言語では、用語の型によって、その言語で使用できる方法と使用できない方法が決まります。たとえば、英語を考えてみましょう。「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メートル」と解釈してしまうと、実行時に問題が発生するまで間違いに気付くことはありません。型システムに単位を組み込むことで、こうした間違いをはるかに早い段階で検出できます。別の例として、ラッセルのパラドックスは、あらゆるものが集合の要素になり、あらゆる述語が集合を定義できる場合に発生しますが、より慎重な型付けによって、このパラドックスを解決する方法がいくつか得られます。実際、ラッセルのパラドックスは、初期の型理論の着想源となりました。
用語が型を取得する方法はいくつかあります。
delay: seconds := 4delay4delay: secondsdelay特にプログラミング言語においては、コンピュータが利用できる共通の背景知識は限られている場合がある。型が明示的に指定されている言語では、ほとんどの型を明示的に宣言する必要がある。型推論は、この負担を軽減し、コンピュータが文脈から推論できるはずの型を開発者が宣言する必要をなくすことを目的としている。
型付けにおいて、式 E は型 T と対をなし、正式には E : T と表記されます。通常、型付けは特定の文脈においてのみ意味を持ちますが、ここではその文脈は省略します。
このような状況において、以下の質問は特に興味深い。
単純な型付けのラムダ計算では、3つの質問すべてについて判定可能です。より表現力豊かな型が許容される場合は、状況はそれほど容易ではありません。
型は、静的型付けが厳格な 一部の言語に存在する機能です。また、一般的には関数型プログラミング言語の特徴でもあります。型推論を含む言語には、C ( C23以降)、[ 3 ] C++ ( C++11以降)、[ 4 ] C# (バージョン 3.0 以降)、Chapel、Clean、Crystal、D、Dart、[ 5 ] F#、[ 6 ] FreeBASIC、Go、Haskell、Java (バージョン 10 以降)、Julia、[ 7 ] Kotlin、[ 8 ] ML、Nim、OCaml、Opa、Q#、RPython、Rust、[ 9 ] Scala、[ 10 ] Swift、[ 11 ] TypeScript、[ 12 ] Vala、[ 13 ] Zig、Visual Basic [ 14 ] (バージョン 9.0 以降)などがあります。これらの言語の大部分は、単純な形式の型推論を使用しています。 Hindley –Milner型システムは、より完全な型推論を提供できます。型を自動的に推論できる機能により、多くのプログラミング作業が容易になり、プログラマは型チェックを維持しながら型注釈を省略できるようになります。
一部のプログラミング言語では、すべての値にコンパイル時に明示的にデータ型が宣言され、実行時に特定の式が取り得る値が制限されます。ジャストインタイムコンパイルの普及により、実行時とコンパイル時の区別はますます曖昧になっています。しかし、歴史的に見ると、値の型が実行時にのみ判明する言語は動的型付け言語です。他の言語では、式の型はコンパイル時にのみ判明します。これらの言語は静的型付け言語です。ほとんどの静的型付け言語では、関数とローカル変数の入力型と出力型は、通常、型注釈によって明示的に指定する必要があります。たとえば、ANSI Cでは次のようになります。
int increment ( int x ) { int result ; // 整数型 result を宣言result = x + 1 ; return result ; }この関数定義のシグネチャは、が1つの引数（整数）を受け取り、整数を返す関数であることを宣言しています。は、ローカル変数が整数であることを宣言しています。型推論をサポートする仮想的な言語では、コードは次のように記述されるかもしれません。intincrement(intx)increment()int result;result
increment ( x ) { var result ; // 推論型変数 result var result2 ; // 推論型変数 result #2result = x + 1 ; result2 = x + 1.0 ; // この行は（提案された言語では）機能しませんreturn result ; }これは、 Dart言語でコードを記述する方法とまったく同じですが、以下に説明するように、いくつかの追加の制約が適用されます。コンパイル時にすべての変数の型を推論することが可能です。上記の例では、定数が整数型であるため、コンパイラはresultと が整数型であると推論し、したがって は関数であると推論します。変数 は正当な方法で使用されていないため、型は持ちません。x1increment()int -> intresult2
最後の例が記述されている架空の言語では、コンパイラは、反対の情報がない限り、+は 2 つの整数を受け取り、1 つの整数を返すものと想定します。（これは、たとえばOCaml の動作と同じです。）このことから、型推論器は の型がx + 1整数であると推論でき、これはresultが整数であることを意味し、したがって の戻り値はadd_one整数になります。同様に、 は+両方の引数が同じ型であることを要求するため、xは整数でなければならず、したがって はadd_one引数として 1 つの整数を受け入れます。
しかし、次の行では、浮動小数点演算でresult2小数を加算して計算されるため、整数式と浮動小数点式の両方での使用に競合が生じます。このような状況に対する正しい型推論アルゴリズムは1958年から知られており、1982年から正しいことが知られています。このアルゴリズムは以前の推論を再検討し、最初から最も一般的な型（この場合は浮動小数点型）を使用します。ただし、これには悪影響が生じる可能性があり、たとえば、最初から浮動小数点型を使用すると、整数型では発生しなかった精度の問題が発生する可能性があります。1.0x
しかしながら、多くの場合、このような状況ではバックトラックできず、代わりにエラーメッセージを生成するような、退化した型推論アルゴリズムが用いられます。型推論はアルゴリズム的に常に中立であるとは限らないため（前述の浮動小数点精度の問題が示すように）、この動作の方が望ましい場合もあります。
中程度の汎用性を持つアルゴリズムでは、暗黙的にresult2浮動小数点変数として宣言され、加算によって暗黙的にx浮動小数点型に変換されます。呼び出し元のコンテキストが浮動小数点引数を決して提供しない場合は、これは正しい動作となります。このような状況は、型変換を伴わない型推論と、多くの場合制約なしにデータを別のデータ型に強制的に変換する暗黙的な型変換との違いを示しています。
最後に、複雑な型推論アルゴリズムの大きな欠点は、結果として得られる型推論の解決が人間にとって分かりにくいこと（特にバックトラッキングのため）であり、コードは主に人間が理解できるように設計されているため、これは有害となる可能性がある。
近年登場したジャストインタイムコンパイルにより、様々な呼び出しコンテキストから提供される引数の型がコンパイル時に判明し、同じ関数の多数のコンパイル済みバージョンを生成できるハイブリッドアプローチが可能になりました。各コンパイル済みバージョンは、異なる型セットに合わせて最適化できます。例えば、JITコンパイルでは、少なくとも2つのコンパイル済みバージョンが存在しますincrement()。
型推論とは、コンパイル時に式の型を部分的または完全に自動的に推論する機能のことです。コンパイラは、明示的な型注釈がなくても、変数の型や関数の型シグネチャを推論できる場合が多くあります。型推論システムが十分に堅牢であるか、プログラムや言語が十分に単純であれば、多くの場合、プログラムから型注釈を完全に省略することが可能です。
式の型を推論するために必要な情報を取得するために、コンパイラは、その部分式に与えられた型注釈を集約してさらに簡略化することでこの情報を収集するか、またはさまざまな原子値の型（例：true ：Bool、42 ：Integer、3.14159 ：Realなど）を暗黙的に理解することによってこの情報を取得します。型推論言語のコンパイラは、式が最終的に暗黙的に型付けされた原子値に簡略化されることを認識することによって、型注釈なしでプログラムを完全にコンパイルすることができます。
複雑な高階プログラミングや多態性においては、コンパイラが常に十分な推論を行うとは限らず、曖昧さを解消するために型注釈が必要になる場合がある。例えば、多態性再帰における型推論は決定不能であることが知られている。さらに、明示的な型注釈を用いることで、コンパイラが推論した型よりも具体的な（より高速でより小さな）型を使用するように強制し、コードを最適化することができる。[ 15 ]
例えば、Haskellの関数はmapリストの各要素に関数を適用し、次のように定義できます。
map f [] = [] map f ( first : rest ) = f first : map f rest（:Haskellでは、 consは、先頭要素とリストの末尾をより大きなリストに構造化したり、空でないリストを先頭要素と末尾に分解したりする操作を表します。これは、数学やこの記事の他の箇所で説明されているような「型」を表すものではありません。Haskellでは、その「型」を表す演算子は::代わりに別の形式で記述されます。）
関数の型推論はmap次のように進みます。mapは 2 つの引数を取る関数なので、その型は の形式に制約されます。 Haskell では、パターンと は常にリストに一致するため、2 番目の引数はリスト型でなければなりません。つまり、 は何らかの型 です。その最初の引数は引数 に適用され、その型はリスト引数の型 に対応する 型でなければなりません。つまり、 は何らかの型 です(は「 型 である」という意味です) 。最後に、 の戻り値はを生成するもののリストなので、 となります。a->b->c[](first:rest)b=[d]dffirstdf::d->e::emapff[e]
パーツを組み合わせると になります。型変数には特別なことは何もないので、 とラベルを変更できます。map::(d->e)->[d]->[e]
map :: ( a -> b ) -> [ a ] -> [ b ]結果として、これ以上の制約が適用されないため、これは最も一般的な型であることがわかります。 の推論型はパラメトリック多相でmapあるため、 の引数と結果の型は推論されず、型変数として残されます。したがって、 は、各呼び出しで実際の型が一致する限り、さまざまな型の関数やリストに適用できます。fmap
コンパイラなどのプログラムで使用されるアルゴリズムは、上記の非公式に構造化された推論と同等ですが、もう少し冗長で体系的です。具体的な詳細は選択された推論アルゴリズムによって異なります（最もよく知られているアルゴリズムについては次のセクションを参照）が、以下の例は一般的な考え方を示しています。ここでも、次の定義から始めますmap。
map f [] = [] map f ( first : rest ) = f first : map f rest（繰り返しますが、:ここでの は Haskell のリストコンストラクタであり、「型の」演算子ではありません。Haskell では代わりに と表記されます::。）
まず、各用語ごとに新しい型変数を作成します。
αmapは、推論したい型を表します。βf最初の式におけるは のタイプを表すものとする。[γ][]は、最初の等式の左辺ののタイプを表すものとする。[δ][]は、最初の等式の右辺ののタイプを表すものとする。εfは、2番目の式におけるのタイプを表すものとする。ζ -> [ζ] -> [ζ]:は、最初の等式の左辺におけるの型を表すものとする。（このパターンは定義から明らかである。）ηは のタイプを示すものとするfirst。θは のタイプを示すものとするrest。ι -> [ι] -> [ι]:は、最初の等式の右辺ののタイプを表すものとする。次に、これらの項から構築された部分式に対して新しい型変数を作成し、それに応じて呼び出される関数の型を制約します。
κは の型を表します。ここで「類似」記号は「 と統一する」という意味です。つまり、 の型である は、と のリストを受け取り、 を返す関数の型と互換性がある必要があるということです。mapf[]α ~ β -> [γ] -> κ~αmapβγκλは のタイプを表すものとする。我々は と結論付ける。(first:rest)ζ -> [ζ] -> [ζ] ~ η -> θ -> λμは のタイプを表すものとする。我々は と結論付ける。mapf(first:rest)α ~ ε -> λ -> μνは のタイプを表すものとする。我々は と結論付ける。ffirstε ~ η -> νξは のタイプを表すものとする。我々は と結論付ける。mapfrestα ~ ε -> θ -> ξοは のタイプを表すものとする。我々は と結論付ける。ffirst:mapfrestι -> [ι] -> [ι] ~ ν -> ξ -> οまた、各方程式の左辺と右辺が互いに統一されるように制約を課します。κ ~ [δ]すなわち、 とμ ~ οです。全体として、解くべき統一系の式は次のようになります。
α ~ β -> [γ] -> κ ξ -> [ξ] -> [ξ] ~ η -> θ -> λ α ~ ε -> λ -> μ ε ~ η -> ν α ~ ε -> θ -> ξ ι -> [ι] -> [ι] ~ ν -> ξ -> ο κ ~ [δ] μ ~ ο
次に、これ以上変数を削除できなくなるまで代入を繰り返します。正確な順序は重要ではありません。コードの型チェックが成功すれば、どの順序でも同じ最終形式になります。οまず、 を にμ、[δ]を に代入することから始めましょうκ。
α ~ β -> [γ] -> [δ] ξ -> [ξ] -> [ξ] ~ η -> θ -> λ α ~ ε -> λ -> ο ε ~ η -> ν α ~ ε -> θ -> ξ ι -> [ι] -> [ι] ~ ν -> ξ -> ο
、ζおよび、および、およびをそれぞれ代入することは、のような型コンストラクタが引数に関して可逆であるため、すべて可能です。η[ζ]θλιν[ι]ξο·->·
α ~ β -> [γ] -> [δ] α ~ ε -> [ζ] -> [ι] ε ~ ζ -> ι
ζ -> ιをε、β -> [γ] -> [δ]を に置き換え、最後にαを復元できるように2番目の制約を残しておく。α
α ~ (ι -> ι) -> [ι] -> [ι] β -> [γ] -> [δ] ~ (ι -> ι) -> [ι] -> [ι]
そして最後に、型コンストラクタが可逆であるため、(ζ -> ι)とをβそれぞれ と にζ置き換えることで、2 番目の制約に固有のすべての変数が削除されます。γιδ[·]
α ~ (ι -> ι) -> [ι] -> [ι]
これ以上の置換は不可能であり、ラベルを付け直すと、詳細に立ち入らずに見つけたものと同じ結果が得られます。map::(a->b)->[a]->[b]
型推論を実行するために最初に使用されたアルゴリズムは、現在では非公式にヒンドレー・ミルナーアルゴリズムと呼ばれていますが、このアルゴリズムは本来ダマスとミルナーに帰属されるべきものです。[ 18 ] また、伝統的に型再構築とも呼ばれています。[ 1 ]： 320項がヒンドレー・ミルナー型付け規則に従って適切に型付けされている場合、規則は項の主型付けを生成します。この主型付けを発見するプロセスが「再構築」のプロセスです。
このアルゴリズムの起源は、1958 年にHaskell CurryとRobert Feysによって考案された、単純型付きラムダ計算の型推論アルゴリズムです。1969 年にJ. Roger Hindley はこの研究を拡張し、彼らのアルゴリズムが常に最も一般的な型を推論することを証明しました。1978 年にRobin Milner [ 19 ]は、Hindley の研究とは独立して、同等のアルゴリズムであるアルゴリズム Wを提供しました。1982 年にLuis Damas [ 18 ]は、 Milner のアルゴリズムが完全であることを最終的に証明し、多相参照を持つシステムをサポートするように拡張しました。
設計上、型推論は最も適切な汎用型を推論します。しかし、多くの言語、特に古いプログラミング言語は、やや不完全な型システムを持っており、より汎用的な型を使用してもアルゴリズム的に中立ではない場合があります。典型的な例としては、次のものが挙げられます。
+整数を加算できますが、バリアント型が整数を保持していても、それらを文字列として連結できます。型推論アルゴリズムは、プログラミング言語だけでなく自然言語の分析にも使用されてきました。 [ 20 ] [ 21 ] [ 22 ]また、型推論アルゴリズムは、自然言語の文法誘導[ 23 ] [ 24 ]や制約ベースの文法システム[ 25 ]にも使用されています。
!-- 下記のカテゴリは非表示です -->