10

私の知る限り、関数またはモジュールの記述中にソースに型注釈を記述する必要がなく、そのコードのチャンクが「型が正しい」場合、コンパイラーは型を推測してコードをコンパイルします。それ以上のものはありますか？

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

更新1：明確にするために、動的に型付けされたプログラミング言語ではなく、静的に型付けされ、完全に型推論されたプログラミング言語について質問しています。

4

3 に答える 3

15

型推論とは何ですか？

歴史的に、型推論（または型再構築）は、プログラム内のすべての型を、本質的に明示的な型注釈を必要とせずに導出できることを意味していました。ただし、近年、プログラミング言語の主流では、ボトムアップ型推論の最も些細な形式でさえ「型推論」（たとえば、autoC ++ 11の新しい宣言）としてラベル付けすることが流行しています。そのため、人々は「本物」を指すために「フル」を追加し始めました。

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

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

f(x) = x + 1

型システムは、fがInt→Int型であると判断し、この型推論と呼ぶのが理にかなっています。さらに、ポリモーフィック型推論については、たとえば、

g(x) = x

ジェネリック型∀（t）t→tが自動的に割り当てられます。

型推論は、単純型付きラムダ計算のコンテキストで発明され、ポリモーフィック型推論（1970年代に発明された別名Hindley / Milner型推論）は、MLファミリーの言語（標準ML、OCaml、および間違いなくHaskell）。

フルタイプの推論の限界は何ですか？

Core MLには、「完全な」ポリモーフィック型推論の贅沢があります。しかし、それはその型システムにおけるポリモーフィズムの特定の制限に依存しています。特に、関数の引数ではなく、定義のみをジェネリックにすることができます。あれは、

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

id定義がわかっている場合はポリモーフィック型を指定できるため、正常に機能します。だが

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

id関数の引数として多形にすることはできないため、MLでチェックを入力しません。言い換えると、型システムは∀（t）t→tのようなポリモーフィック型を許可しますが、（∀（t）t→t）→Boolのようないわゆる上位のポリモーフィック型は許可しません。ファーストクラスの方法（明確にするために、明示的に型指定された言語がごくわずかでも許可されます）。

明示的に型付けされる多形ラムダ計算（「システムF」とも呼ばれる）は、後者を可能にします。しかし、完全なシステムFの型再構成が決定不可能であるというのは、型理論の標準的な結果です。Hindley / Milnerは、型の再構築がまだ決定可能である、わずかに表現力の低い型システムのスイートスポットに当たります。

完全な型の再構築を決定不能にする、より高度な型システムの機能もあります。そして、それを決定可能に保つが、それでも実行不可能にする他のものがあります。例えば、それが組み合わせ爆発につながるので、アドホックなオーバーロードまたはサブタイピングの存在。

于 2012-05-06T12:00:19.487 に答える
13

フル型推論の制限は、多くの高度な型システム機能では機能しないことです。例として、HaskellとOCamlを考えてみましょう。これらの言語はどちらもほぼ完全に型推論されていますが、型推論を妨げる可能性のある機能がいくつかあります。

Haskellでは、多形の戻り型と組み合わされた型クラスです。

readAndPrint str = print (read "asd")

readこれは型の関数です。これは、「型クラスをサポートするRead a => String -> aすべての型の場合、関数はaを取り、を返すことができることを意味します。したがって、がintを受け取るメソッドの場合、次のように記述して、「123」をIntに変換します。 123を呼び出して呼び出します。これは、Intを取るため、文字列をIntに変換する必要があることを認識しています。fがintのリストを取得した場合、代わりに文字列をIntのリストに変換しようとします。問題ありません。aReadreadStringaff (read "123")ff

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

OCamlの問題のある機能は、クラス内のポリモーフィック関数です。オブジェクトを引数として取り、そのオブジェクトのメソッドを呼び出す関数を定義すると、コンパイラはそのメソッドのモノモーフィック型を推測します。例えば：

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

ここで、コンパイラは、タイプobjという名前のメソッドを持つクラスのインスタンスである必要があると推測します。つまり、Intを受け取り、Intを返すメソッドです。これで、そのようなメソッドを持つ一連のクラスを定義し、そのクラスのインスタンスを引数としてに渡すことができます。問題ない。methint -> intf

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

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

その結果、そのような高度な機能のないMLの基本的な方言は、完全に型推論されます。たとえば、Caml Lightは基本的にクラスのないOCamlであるため、完全に型推論されていると思います（ただし、実際には言語がわからないため、これは単なる仮定です）。

于 2012-05-05T18:04:05.533 に答える
2

もう1つの制限は、ランクの高いタイプです。たとえば、次のプログラムは、MLスタイルの型推論を使用する言語で型チェックを行いません。

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

タイプチェッカーは、タイプ[Char]->[Char]または[Int]->[Int]を割り当てることができますが、すべてのa。[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
于 2012-05-07T09:00:55.483 に答える