20

OCaml コンパイラには "-principal" オプションがあり、"principal type" という用語がメーリング リストで言及されることがあります。正確にはどういう意味ですか？ウィキペディアの定義は再帰的であり、読者がその概念に既に精通していることを前提としています。

4

2 に答える 2

36

型推論のプロセスは、ユーザーが作成したプログラムが与えられた場合に、そのプログラムの型を推測することです。一般に、特定のプログラムにはいくつかの正しいタイプが存在する場合があります。たとえば、プログラムに と の型をfun x -> x指定できます。int -> intbool -> bool

プログラムが与えられた場合、このプログラムの型が、このプログラムに与えることができる最も一般的な型である場合、他のすべての可能な型がこの型の特殊化 (インスタンス) であるという意味で、その型はプリンシパルです。私のfun x -> x例では、ポリモーフィック'a -> 'aはプリンシパル型です。

一部の型システムでは、プリンシパル型が常に存在するとは限りません。P2 つの可能なタイプT1とを持つプログラムがありT2、どちらも他のタイプよりも一般的ではありません。たとえば、数値演算子がオーバーロードされている一部のシステムでは、プログラムに typeとtype をfun x -> x + x指定できますが、両方を包含する型はありません。これは推論エンジンにとって問題です。これは、任意の選択をしなければならないことを意味し、ユーザーが意図したものであるかどうかを知らずに可能なタイプの 1 つを選択することを意味します。プリンシパル型がある場合、推論プロセスで選択する必要はありません。int -> intfloat -> float

(その例を解決するために、次のことができます: (1) 算術演算子をオーバーロードしない (2) 任意の選択を行う (F# が iirc で行うこと) (3) プログラムを拒否し、あいまいさを取り除くために型注釈を要求する (4) もっとHaskell のような表現型Num a => a -> a。)

Hindley-Milner 型推論に基づく OCaml 言語の「単純な」サブセットには、主要な型があります。これは、推論エンジンが常に正しいことを行うことを意味します (考えられる型の仕様が与えられた場合)。型システムのいくつかのより高度な側面 (例: ポリモーフィック フィールドとメソッド) では、このプロパティが失われます。型システムが最も一般的な型を見つけられない場合や、最も一般的な型を見つけるには、型推論エンジン (一般的に高速化を目指します)。オプションは、私の記憶が正しければ次の-principalようなノブです。

  • 失敗は、タイプチェッカーがそうでなければ非主要な解決策を受け入れたであろういくつかのケースです (任意の選択を行いました)
  • より長い型チェック時間とメモリ使用量を犠牲にして、主な解決策を見つけようとする

私はこのフラグにあまり詳しくありません (あまりにも高度な型システム機能は避けたいので、私のプログラムは通常気にしません)、これを再確認する必要がありますが、それは大まかな考えです。私の意見では、このフラグは比較的重要ではありません (通常は気にする必要はありません) が、プリンシパル型の概念は ML 言語の理論の重要な部分です。

さらに詳しく知りたい場合は、さらに 2 つの技術的な詳細を以下に示します。

  • 「プリンシパル型」の ML 概念は、固定型環境が与えられた場合に最も一般的な型が存在するかどうかという問題です。一部の著者は、それらが最も一般的な (環境、タイプ) ペア、いわゆる「プリンシパル タイピング」であるかどうかという問題を研究しています。これは難しい問題です (他のモジュールから何を期待するかを推測する必要がありますが、ML では依存する外部モジュールの署名が与えられます。ポリモーフィズムを推測するのは非常に困難です)。言語。

  • プリンシパル型の存在は、型システムの設計者にとって微妙なバランスです。ML 型システム (ポリモーフィズム、 などの型) から機能を削除する'a -> 'aと、主性が失われますが、力を加えると (ML からより表現力豊かなポリモーフィック型を持つシステム F に移行する場合)、主性も失われる可能性があります。MLF などのさらに複雑な型システムに移行することで、失われた主権を取り戻すことができますが、これは難しい問題です。

実際には、プログラミング言語の設計者の比較的大部分が最近、主権という考えをあきらめました。彼らは、主体性を求めるのが難しすぎる、より野心的な型システム (依存型など) を持ちたいと考えているため、代わりに非主要な推論に満足しています: 推論エンジンが何らかの型を見つけることができれば、それはすでに良いことです。結果の一般性については難しい。OCaml 型システムのメイン メンテナである Jacques Garrigue は、今でもそれを非常に気にかけています。これは、OCaml プログラミング言語研究の興味深い側面だと思います。

于 2012-07-18T16:08:42.887 に答える
10

ガッシェの説明に基づいて少し構築するために、OCaml 自身のテスト スイートから盗んだ例を示します。免責事項: これはオブジェクトを使用します。

class c = object method id : 'a. 'a -> 'a = fun x -> x end;;
type u = c option;;
let just = function None -> failwith "just" | Some x -> x;;
let f x = let l = [Some x; (None : u)] in (just(List.hd l))#id;;
let g x =
  let none = (fun y -> ignore [y;(None:u)]; y) None in
  let x = List.hd [Some x; none] in (just x)#id;;
let h x =
  let none = let y = None in ignore [y;(None:u)]; y in 
  let x = List.hd [Some x; none] in (just x)#id;;

トップレベルのセッションでこれを実行すると、次のようになります。

#     val f : c -> 'a -> 'a = <fun>
#     val g : c -> 'a -> 'a = <fun>
#     val h : < id : 'a; .. > -> 'a = <fun>

これらの関数はまったく同じことを実行しますが、異なる型が割り当てられます!

このオプションを指定して OCaml を呼び出すと-principal、最初の 2 つの例がトリガーされます。

Warning 18: this use of a polymorphic method is not principal.

興味深いことに'a、 の型をhwithに置き換えると、 and と'a -> 'aまったく同じ型が得られます。これは、この型が単なる型の省略形 (つまり、展開先) であるためです。fgc< id: 'a -> 'a; .. >

ここでコンパイラがプログラマーに伝えたいことは、 と には 2 つの適切な型がfありg、OCaml がどちらが「最良」であるかを決定するのに役立つ基準はないということです (「最良」とは、「主」を意味します。もちろん！）。

于 2012-07-23T20:23:29.743 に答える