20

Hindley-Milner Type Inferenceに関するウィキペディアの記事を読んで、意味を理解しようとしています。これまでのところ、これは私が理解したことです：

  1. タイプは、モノタイプまたはポリタイプのいずれかに分類されます。
  2. intモノタイプは、型定数 (または などstring) または型変数 (αおよび など)としてさらに分類されますβ。
  3. 型定数は、具象型 (intや などstring) または型コンストラクタ ( やMapなど) のいずれかSetです。
  4. 型変数 (αや などβ) は、具象型 (intや などstring) のプレースホルダーとして動作します。

今、私はポリタイプを理解するのに少し苦労していますが、Haskellを少し学んだ後、これが私が作るものです:

  1. 型自体に型があります。正式には、タイプのタイプはカインドと呼ばれます (つまり、タイプにはさまざまな種類があります)。
  2. 具象型 (intや などstring) と型変数 (αや などβ) は一種*です。
  3. 型コンストラクタ (Mapおよび などSet) は、型のラムダ抽象化です (たとえば、 Setis of kind* -> *およびMapis of kind * -> * -> *)。

私が理解していないのは、修飾子が何を意味するのかということです。例えば何∀α.σを表しているのですか？私はそれの頭も尻尾も作ることができないようで、次の段落を読めば読むほど混乱します。

対照的に、ポリタイプ∀α.α -> αを持つ関数は、同じ型の任意の値をそれ自体にマップでき、恒等関数はこの型の値です。別の例として、∀α.(Set α) -> intは、すべての有限集合を整数にマッピングする関数の型です。メンバーの数は、このタイプの値です。修飾子はトップレベルにしか現れないことに注意してください。例えば、タイプ∀α.α -> ∀α.αはタイプの構文によって除外され、モノタイプはポリタイプに含まれるため、タイプは一般的な形式∀α₁ を持ちます。. . ∀αₙ.τ .

4

2 に答える 2

20

まず、種類とポリモーフィック型は別物です。すべての型が同じ種類 (*) である HM 型システムを持つことができます。ポリモーフィズムはなく複雑な種類を持つシステムを持つこともできます。

項Mが typeである場合、それは、置換できる∀a.t型が何であれ(しばしば と書かれ、それは typeであるとします。これは、任意の項を普遍的に量化された変数に置き換えることができる論理にいくぶん似ています。ですが、ここでは型を扱っています。ssatt[a:=s]Mt[a:=s]

これはまさに Haskell で起こっていることであり、Haskell では量指定子が表示されないだけです。型シグネチャに現れるすべての型変数はforall、型の前にあるかのように、暗黙的に量化されます。たとえば、mapタイプがあります

map :: forall a . forall b . (a -> b) -> [a] -> [b]

など。この暗黙の全称量化がなければ、型変数aと型変数bは何らかの固定された意味を持つ必要がありmap、ポリモーフィックにはなりません。

HM アルゴリズムは、タイプ(量指定子なし、モノタイプ) とタイプ スキーマ(普遍的に量化されたタイプ、ポリタイプ) を区別します。一部の場所では型スキーマを使用することが重要ですが (のようにlet)、他の場所では型のみが許可されます。これにより、すべてが決定可能になります。

System Fに関する記事もお読みになることをお勧めします。これはより複雑なシステムでありforall、型のどこでも使用できます (したがって、そこにあるものはすべてtypeと呼ばれます) が、型の推論/チェックは決定できません。仕組みを理解するのに役立ちますforall。System F については、Girard、Lafont、Taylor のProofs and Typesで詳しく説明されています。

于 2013-03-19T12:00:36.780 に答える
4

l = \x -> tHaskell で検討します。tこれは変数内の項を表すラムダであり、x後で置換されます (たとえばl 1、それが意味するものは何でも)。同様に、∀α.σは型 variable を持つ型を表しますα。つまりf : ∀α.σ、 type によってパラメーター化された関数の場合αです。ある意味では にσ依存するαため、 typeのf値を返します。これは後で置換され、具体的な型が得られます。σ(α)ασ(α)

∀Haskell では、 のように関数を省略して定義することができますid : a -> a。RankNTypes数量詞の省略を許可する理由は、基本的に、それらがトップ レベル (拡張なし) でのみ許可されているためです。このコードを試すことができます：

id2 : a -> a -- I named it id2 since id is already defined in Prelude
id2 x = x

id( :t id)の型を ghci に尋ねると、が返されa -> aます。より正確に言えば (より型理論的に)、id型は∀a. a -> aです。ここで、コードに追加すると:

val = id2 3

, 3 には型Intがあるので、その型Intが に代入されσ、具体的な型が得られInt -> Intます。

于 2013-03-19T12:03:27.300 に答える