型推論

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

型推論とは、形式言語での式のの自動検出を指しますこれらには、プログラミング言語や数学的型システムが含まれますが、コンピュータサイエンス言語学の一部の分野における自然言語も含まれます

非技術的な説明

最も一般的なビューのタイプは、そのタイプのオブジェクトで可能なアクティビティを提案および制限する指定された用途に関連付けることができます。言語の多くの名詞はそのような使用法を指定します。たとえば、leashという単語は、 lineという単語とは異なる使用法を示します何かをテーブルと呼ぶことは、それをと呼ぶこととは別の指定を示しますが、それは実質的に同じことかもしれません。それらの材料特性は物事をいくつかの目的に使用できるようにしますが、それらは特定の指定の対象にもなります。これは特に抽象的な分野、つまり数学やコンピュータサイエンスの場合に当てはまり、最終的には材料がビットまたは数式になります。

望ましくないが実質的に可能な使用法を除外するために、タイプの概念が定義され、多くのバリエーションで適用されます。数学では、ラッセルのパラドックスが型理論の初期のバージョンを引き起こしました。プログラミング言語では、典型的な例は「タイプエラー」です。たとえば、数値ではない値を合計するようにコンピューターに命令します。実質的には可能ですが、結果はもはや意味がなく、プロセス全体にとって悲惨な結果になる可能性があります。

タイピングでは、式はタイプとは反対です例えば、、 とタイプとはすべて別個の用語です自然数の場合。伝統的に、式の後にはコロンとそのタイプが続きます。これは、値がタイプですこのフォームは、新しい名前を宣言するためにも使用されます。、「探偵デッカー」という言葉でシーンに新しいキャラクターを紹介するようなものです。

指定がゆっくりと展開される話とは対照的に、形式言語のオブジェクトは、多くの場合、最初からタイプで定義する必要があります。さらに、式があいまいな場合は、使用目的を明示的にするために型が必要になる場合があります。たとえば、式タイプがあるかもしれませんしかし、有理数または実数として、あるいはプレーンテキストとしても読むことができます。

結果として、プログラムまたは証明は型に非常に煩わされる可能性があるため、コンテキストからそれらを推測することが望ましいです。これは、型指定されていない式(未定義の名前を含む)の使用を収集することで可能になります。たとえば、まだ定義されていない名前nが式で使用されている場合nは少なくとも数であると結論付けることができます。式とそのコンテキストから型を推測するプロセスは、型推論です。

一般に、オブジェクトだけでなく、アクティビティにもタイプがあり、それらを使用するだけで導入できます。スタートレックのストーリーの場合、そのような未知のアクティビティは「ビーム」である可能性があります。これは、ストーリーの流れのために実行されるだけで、正式に紹介されることはありません。それにもかかわらず、何が起こったのかに従ってそのタイプ(輸送)を推測することができます。さらに、オブジェクトとアクティビティの両方をそれらのパーツから構築できます。このような設定では、型推論はより複雑になるだけでなく、競合する使用や意図しない使用を検出しながら、構成されたシーン内のすべての完全な説明を収集できるため、より便利になります。

型チェックと型推論

タイピングでは、式EはタイプTとは反対であり、正式にはE:Tと記述されます。通常、タイピングは特定のコンテキスト内でのみ意味がありますが、ここでは省略されています。

この設定では、次の質問が特に重要です。

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

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

プログラミング言語のタイプ

型は、いくつかの強く 静的に型付けされた言語に存在する機能です。これは、一般的な関数型プログラミング言語の特徴であることがよくあります型推論を含むいくつかの言語には、C ++ 11[1] C#(バージョン3.0以降)、ChapelCleanCrystalDF#[2] FreeBASICGoHaskellJava(バージョン10以降)、ジュリア[3] コトリン[4] MLNimOCamlOpaRPythonRust[5] Scala[6] Swift[7] TypeScript[8] Vala[9] Dart[10]およびVisual Basic [11](バージョン9.0以降) 。それらの大部分は、単純な形式の型推論を使用しています。Hindley-Milner型システムは、より完全な型推論を提供できます。型を自動的に推測する機能により、多くのプログラミングタスクが簡単になり、プログラマーは型の注釈を自由に省略できます。型チェックを許可しながら。

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

int add_one int x {   
    int結果; / *整数の結果を宣言します* /  

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

この関数定義のシグニチャ、それが1つの引数、整数を取り、整数を返す関数であることint add_one(int x)を宣言します。ローカル変数が整数であることを宣言します。型推論をサポートする架空の言語では、コードは代わりに次のように記述される場合があります。 add_oneint result;result

add_one x  { 
    var  result ;   / *推定型変数の結果* / 
    var  result2 ;  / *推定型変数の結果#2 * /

    結果 =  x  +  1 ; 
    result2  =  x  +  1.0 ;   / *この行は(提案された言語では)機能しません* /
    結果を返し ます; }

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

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

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

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

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

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

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

整数入力を受け入れ、暗黙の型変換を使用するバージョン。
入力として浮動小数点数を受け入れ、全体で浮動小数点命令を使用するバージョン。

技術的な説明

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

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

高次プログラミングポリモーフィズムの複雑な形式では、コンパイラが多くを推測できるとは限らず、曖昧性解消のために型注釈が必要になる場合があります。たとえば、多形再帰を使用した型推論は決定不能であることが知られています。さらに、明示的な型注釈を使用して、コンパイラーに推測よりも具体的な(より高速/より小さな)型を使用させることにより、コードを最適化できます。[12]

型推論のいくつかの方法は、制約の満足度[13]または満足度のモジュロ理論に基づいています。[14]

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

map  f  []  =  [] 
map  f  first rest  =  f  first   map  f  rest

関数の型推論は次のmapように進行します。mapは2つの引数の関数であるため、その型はの形式に制限されますa → b → cHaskellでは、パターン[](first:rest)常にリストに一致するため、2番目の引数はリスト型である必要があります:b = [d]ある型の場合dその最初の引数fは引数に適用されます。引数は、リスト引数の型に対応するfirst型を持っている必要があります。したがって、ある型では「型の」を意味します)最後に、の戻り値は、生成されるもののリストであるため、 df :: d → e::emap ff[e]

パーツを組み合わせると、になりmap :: (d → e) → [d] → [e]ます。型変数について特別なことは何もないので、次のようにラベルを変更できます。

マップ :( a b [ a ] [ b ]      

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

Hindley-Milner型推論アルゴリズム

型推論を実行するために最初に使用されたアルゴリズムは、現在、非公式にHindley-Milnerアルゴリズムと呼ばれていますが、アルゴリズムはDamasとMilnerに適切に帰属する必要があります。[15]

このアルゴリズムの起源は、1958年にHaskellCurryとRobertFeysによって考案された単純型付きラムダ計算の型推論アルゴリズムです。[引用必要] 1969 J。RogerHindleyこの作業を拡張し、彼らのアルゴリズムが常に最も多くを推論することを証明しました。一般的なタイプ。1978年にロビンミルナー[16]は、ヒンドリーの研究とは無関係に、同等のアルゴリズムであるアルゴリズムWを提供しました。1982年、ルイス・ダマス[15]は、ミルナーのアルゴリズムが完全であることを最終的に証明し、多型参照を持つシステムをサポートするように拡張しました。

最も一般的なタイプを使用することの副作用

設計上、型推論、特に正しい(バックトラッキング)型推論では、適切な最も一般的な型の使用が導入されますが、より一般的な型は必ずしもアルゴリズム的に中立であるとは限らないため、これは影響を与える可能性があります。

  • 浮動小数点は一般的なタイプの整数と見なされますが、浮動小数点は精度の問題を引き起こします
  • バリアント/動的タイプは、他のタイプの一般的なタイプと見なされます。これにより、異なる可能性のあるキャストルールと比較が導入されます。たとえば、このようなタイプは、数値の加算と文字列の連結の両方に「+」演算子を使用しますが、実行される操作は次のとおりです。静的ではなく動的に決定

自然言語の型推論

型推論アルゴリズムは、プログラミング言語だけでなく自然言語の分析にも使用されてきました。[17] [18] [19]型推論アルゴリズムは、一部の文法誘導[20] [21]および自然言語の制約ベースの文法システムでも使用されます。[22]

参考文献

  1. ^ "プレースホルダー型指定子(C ++ 11以降)-cppreference.com"en.cppreference.com 2021年8月15日取得
  2. ^ cartermp。「型推論-F#」docs.microsoft.com 2020年11月21日取得
  3. ^ 「推論・ジュリア言語」docs.julialang.org 2020年11月21日取得
  4. ^ 「Kotlin言語仕様」kotlinlang.org 2021-06-28を取得
  5. ^ 「ステートメント-Rustリファレンス」doc.rust-lang.org 2021-06-28を取得
  6. ^ 「型推論」Scalaドキュメント2020年11月21日取得
  7. ^ 「基本— Swiftプログラミング言語(Swift 5.5)」docs.swift.org 2021-06-28を取得
  8. ^ 「ドキュメント-型推論」www.typescriptlang.org 2020年11月21日取得
  9. ^ 「Projects / Vala / Tutorial-GNOME Wiki!」wiki.gnome.org 2021-06-28を取得
  10. ^ 「ダート型システム」dart.dev 2020年11月21日取得
  11. ^ キャスリーンドラード。「ローカル型推論-VisualBasic」docs.microsoft.com 2021-06-28を取得
  12. ^ ブライアンオサリバン; ドン・スチュワート; ジョン・ゲルツェン(2008)。「第25章。プロファイリングと最適化」実世界のハスケルオライリー。
  13. ^ Talpin、Jean-Pierre、およびPierreJouvelot。ポリモーフィックタイプ、領域、および効果の推論。」関数型プログラミングのジャーナル2.3(1992):245-271。
  14. ^ ハッサン、モスタファ; アーバン、カテリーナ; アイラーズ、マルコ; ミュラー、ペーテル(2018)。「Python3のMaxSMTベースの型推論」コンピューター支援検証コンピュータサイエンスの講義ノート。10982. pp。12–19。土井10.1007 / 978-3-319-96142-2_2ISBN 978-3-319-96141-5
  15. ^ a b ダマス、ルイス; ミルナー、ロビン(1982)、「機能プログラムの主要なタイプスキーム」、POPL '82:プログラミング言語の原則に関する第9回ACM SIGPLAN-SIGACTシンポジウムの議事録(PDF)、ACM、pp。207–212
  16. ^ Milner、Robin(1978)、「プログラミングにおける型多型の理論」、Journal of Computer and System Sciences17(3):348–375、doi10.1016 / 0022-0000(78)90014-4
  17. ^ センター、人工知能。自然言語とコンピューター言語の構文解析と型推論Diss。スタンフォード大学、1989年。
  18. ^ Emele、Martin C.、およびRémiZajac。タイプされた統一文法。」計算言語学に関する第13回会議の議事録-第3巻。計算言語学会、1990年。
  19. ^ パレスキ、レモ。タイプ駆動型の自然言語分析。」(1988)。
  20. ^ フィッシャー、キャスリーン、他。"Fisher、Kathleen、etal。"汚れからシャベルまで:アドホックデータからの完全自動ツール生成。 "ACMSIGPLANNotices。Vol。43.No。1. ACM、2008。" ACMSIGPLAN通知。43. No. 1. ACM、2008年。
  21. ^ ラピン、シャローム; シーバー、スチュアートM.(2007)。「普遍文法への洞察の源としての機械学習理論と実践」(PDF)言語学ジャーナル43(2):393–427。土井10.1017 / s0022226707004628
  22. ^ スチュアートM.シーバー(1992)。制約ベースの文法形式:自然言語とコンピューター言語の構文解析と型推論MITプレス。ISBN 978-0-262-19324-5

外部リンク