完全型推定言語とは何ですか？そのような言語の限界？

Question

私が知る限り、関数やモジュールを記述している間にソースに型注釈を書く必要がなく、そのコード塊が「型正しく」あるならば、コンパイラはその型を推測しコンパイルしますコード。それ以上はありますか？

には、そのような言語がありますか？はいの場合は、型システムに何らかの制限がありますか？

アップデート1： だけ本当に明確にするために、私は静的に型付けされた、完全に入力し、推測されたプログラミング言語ではない動的型付けプログラミング言語について尋ねています。

Answer 1

フルタイプの推論の制限は、多くの高度なタイプのシステム機能では機能しないということです。例として、HaskellとOCamlを考えてみましょう。これらの言語はいずれも、完全にタイプ推定されたですが、型推論を妨げる可能性のある機能がいくつかあります。多型戻り値の型と組み合わせ

Haskellで

---

それの型クラス：

readAndPrint str = print (read "asd") 

ここ

readは型クラスRead機能をサポートしている任意のタイプaのために」という意味タイプRead a => String -> aの関数であるreadStringを返してaを返すことができます。したがって、fがintを取るメソッドの場合は、f (read "123")と書くことができ、123をInt 123に変換し、fを呼び出しますそれ。 fはIntを取りますので、文字列をIntに変換する必要があることがわかります。 fがintのリストを取った場合、代わりに文字列をIntsのリストに変換しようとします。問題ない。

しかし、上記のreadAndPrint機能の場合、このアプローチは機能しません。ここで問題となるのは、printは、印刷可能な任意のタイプ（つまり、Showのタイプクラスをサポートするタイプ）の引数を取ることができるということです。したがって、文字列をint、intのリスト、または印刷可能なものに変換するかどうかをコンパイラが知る方法はありません。したがって、このような場合には型の注釈を追加する必要があります。 OCamlでは

---

問題の特徴は、クラスで多型の関数である：あなたがそのオブジェクトを引数として受け取り、そのオブジェクトのメソッドを呼び出す関数を定義した場合、コンパイラはそのメソッドの単相タイプを推測します。例えば：ここ

let f obj = obj#meth 23 + obj#meth 42 

コンパイラはobjタイプint -> intのmeth命名法のIntを受け取り、intを返し、すなわちメソッドを持つクラスのインスタンスでなければならないことを推測します。このようなメソッドを持つクラスを定義し、そのクラスのインスタンスを引数としてfに渡すことができます。問題ない。

タイプ'a. 'a -> intのメソッドでクラスを定義すると、問題が発生します。つまり、任意の型の引数をとり、intを返すことができるメソッドです。推論型と一致しないため、そのクラスのオブジェクトをfの引数として渡すことはできません。 fに引数のようなオブジェクトを渡したい場合は、唯一の方法は型の注釈をfに追加することです。

---

これは、ほとんど完全に型推論されている言語の例であり、そうでない場合の例です。これらの言語から問題のある機能を削除すると、完全に型推論されます。

そのような高度な機能を持たないMLの基本方言は完全に推論されます。たとえば、Caml Lightは基本的にクラスなしのOCamlなので、完全に型推論されていると仮定します（しかし、実際には言語は分かりませんので、あくまで仮定です）。

Answer 2

タイプ推論とは何ですか？

歴史的に、型推論（またはタイプの再構成）は、プログラムで全てタイプが本質的に任意の明示的な型注釈を必要とせずに誘導することができることを意味します。しかし、近年では、プログラミング言語の主流において、「型推論」（例えば、C++ 11の新しいauto宣言）として、ボトムアップ型の控除の最も些細な形態でさえも強調されている。だから、人々は "本当の"ものを参照するために "フル"を追加し始めている。

フルタイプ推論とは何ですか？

言語がどの程度推論できるかについての幅広いスペクトルがありますが、実際には、厳密な意味で「完全」型推論をサポートする言語はほとんどありません（コアMLは唯一の例です）。しかし、主な区別の要因は、それらに「定義」が添付されていないバインディングに対して型を導き出すことができるかどうかです。特に、関数のパラメータは—です。たとえば、

f(x) = x + 1 

と書くことができます。 Int → Int型を持つ場合、この型推論を呼び出すことは理にかなっています。また、我々は、ときに約多型型推論を話し、例えば、

g(x) = x 

はFORALLジェネリック型＆が割り当てられ;（T）T →トン自動的。

型推論は単純型ラムダ計算の文脈で発明され、多型推論（別名Hindley/Milner型推論、1970年に発明された）は、MLファミリの言語、OCaml、そして間違いなくHaskell）。

フルタイプの推論の限界はありますか？

コアMLは、 "完全な"多形型推論の高級品です。しかし、それは型システムにおける多形性の特定の限界にかかっています。特に、関数の引数ではなく、定義だけを汎用にすることができます。それは定義がわかっている場合にidが多型の種類を与えることができますので、

id(x) = x; 
id(5); 
id(True) 

は、正常に動作しています。 idは、関数の引数として多型にはできませんので、しかし

f(id) = (id(5); id(True)) 

は、MLにチェックを入力しません。言い換えれば、型システムは、＆lt;; t> t →のような多型を許しますが、多型の値が使われる（明白であるように、明示的に型指定された言語でさえ非常に少数ですら）。

明示的に型指定された多形ラムダ計算（「システムF」とも呼ばれる）は、後者を可能にする。しかし、完全なシステムFのタイプ再構成は決めることができないというタイプ理論の標準的な結果です。 Hindley/Milnerは、やや表現力の低いタイプのシステムのスイートスポットに当たるが、そのタイプの再構成は依然として決定可能である。

フルタイプの再構成が確定できなくなる高度なタイプのシステム機能があります。そして、それを決定可能に保ちながらもそれを実行不可能にする他のものがある。アドホックなオーバーロードまたはサブタイプの存在は、コンビナトリアルな爆発を招くためです。

Answer 3

さらに高いランクのタイプがあります。 例えば、次のプログラムは、MLスタイルの型推論を持つ言語でないです。TypeCheckない： - > [チャー]または[INT] -

foo = let bar f = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse 

型チェッカーは、タイプ[シャア] Fまで割り当てることができます> [Int]ですが、a aalla [a] - > [a]はありません。 ML、Ocaml、F＃では、上位の型を記述することさえできないので、これを修正する方法はありません。

しかし、Haskell（GHC拡張を介して）とFregeは上位のランクタイプをサポートしています。しかし、唯一の上位の型チェックが（上位型推論ではなく）可能性があるため、プログラマは、例えば、しかし、型注釈を与えるために必要とされています

foo = let bar (f :: forall a.[a]->[a]) = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse