30

Haskell の謙虚な恒等関数を例にとると、

id :: forall a. a -> a

Haskell がおそらく非予測的ポリモーフィズムをサポートしていることを考えると、型の帰属を介して型idに「制限」できるべきであることは合理的であるように思われます。(forall a. a -> a) -> (forall b. b -> b)しかし、これはうまくいきません:

Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)

<interactive>:1:1:
    Couldn't match expected type `b -> b'
                with actual type `forall a. a -> a'
    Expected type: (forall a. a -> a) -> b -> b
      Actual type: (forall a. a -> a) -> forall a. a -> a
    In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)
    In an equation for `it':
        it = id :: (forall a. a -> a) -> (forall b. b -> b)

もちろん、必要な署名を使用して、恒等関数の新しい制限された形式を定義することは可能です。

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId x = x

ただし、一般的な観点から定義するとid機能しません。

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId = id -- Similar error to above

それで、ここで何が起こっているのですか？非予測性の難しさに関係しているように見えますが、有効に-XImpredicativeTypesしても違いはありません。

4

3 に答える 3

9

why is it expecting a type of (forall a. a -> a) -> b -> b

I think the type forall b.(forall a. a -> a) -> b -> b is equivalent to the type you gave. It is just a canonical representation of it, where the forall is shifted as much to the left as possible.

And the reason why it does not work is that the given type is actually more polymorphic than the type of id :: forall c. c -> c, which requires that argument and return types be equal. But the forall a in your type effectively forbids a to be unified with any other type.

于 2011-10-05T08:25:14.947 に答える
2

あなたは絶対に正しいですが、それforall b. (forall a. a -> a) -> b -> bはと同等ではありません(forall a. a -> a) -> (forall b. b -> b)。

特に明記されていない限り、型変数は最も外側のレベルで定量化されます。の省略(a -> a) -> b -> b形です(forall a. (forall b. (a -> a) -> b -> b))。タイプの抽象化とアプリケーションが明示的にされているシステムFでは、これはのような用語を表しf = Λa. Λb. λx:(a -> a). λy:b. x yます。表記法に精通していない人のために明確にするために、パラメータとして項をとるのΛとは異なり、パラメータとして型をとるラムダがλあります。

の呼び出し元は、f最初に型パラメーターを提供しa、次に型パラメーターを提供しb、次に2つの値xを提供yし、それらは選択された型に準拠します。注意すべき重要なことは、発信者が選択することaですb。f String Int lengthしたがって、呼び出し元は、たとえば用語を生成するようなアプリケーションを実行できますString -> Int。

-XRankNTypes全称記号を明示的に配置することで用語に注釈を付けることができます。最も外側のレベルである必要はありません。タイプのrestrictedId用語は(forall a. a -> a) -> (forall b. b -> b)、システムFで大まかに例証できますg = λx:(forall a. a -> a). if (x Int 0, x Char 'd') > (0, 'e') then x else id。呼び出し先が両方にg適用でき、最初にタイプを使用してインスタンス化する方法に注意してください。x0'e'

ただし、この場合、呼び出し元は、以前のようにtypeパラメーターを選択できませんf。x Intアプリケーションとx Charラムダの内部に注意してください。これにより、呼び出し元はポリモーフィック関数を提供するように強制されるため、またはに適用されないため、のような用語g lengthは無効になります。lengthIntChar

それについて考える別の方法は、タイプとfツリーgを描画することです。のツリーにfは全称記号がルートとしてあり、のツリーにgは矢印がルートとしてあります。の矢印に到達するためにf、呼び出し元は2つの数量詞をインスタンス化します。を使用gすると、それはすでに矢印タイプであり、呼び出し元はインスタンス化を制御できません。これにより、呼び出し元は多態的な引数を提供する必要があります。

最後に、私の不自然な例を許してください。Gabriel Schererは、MLを介したSystem Fの適度に実用的な使用法で、上位のポリモーフィズムのより実用的な使用法について説明しています。また、TAPLの第23章と第30章を参照するか、コンパイラ拡張機能のドキュメントをざっと読んで、上位のポリモーフィズムのより詳細な例やより実用的な例を見つけることもできます。

于 2011-11-30T19:51:50.623 に答える
-2

私は非予測型の専門家ではないので、これは潜在的な答えであり、コメントから何かを学ぼうとする試みでもあります。

特化しても意味ない

\/ a . a -> a                       (1)

に

(\/ a . a -> a) -> (\/ b . b -> b)  (2)

私は、非予測型がそれを許可する理由になるとは思いません。量指定子には、(2) の左辺と右辺で表される型を一般に不等集合にする効果があります。ただし、a -> a(1) は、左側と右側が同等のセットであることを意味します。

たとえば、(2) を (int -> int) -> (string -> string) に具体化できます。しかし、どのシステムから見ても、これは (1) で表されるタイプではないことがわかっています。

エラー メッセージは、Haskel 型推論器が型を統一しようとした結果のようです。id 

\/ a . a -> a

あなたが与えたタイプで

\/ c . (c -> c) -> \/ d . (d -> d)

ここでは、わかりやすくするために、数量化された変数を一意化しています。

a型推論の仕事は、 、c、の最も一般的な割り当てを見つけてd、2 つの式を構文的に等しくすることです。c最終的に、とを統合する必要があることがわかりdます。それらは個別に定量化されているため、行き止まりになり、終了します。

(c -> c) -> (d -> d)おそらく、基本的な型インファーサー(属性を使用) は単に前進して設定するため、この質問をしているのでしょうc == d。結果のタイプは次のようになります

(c -> c) -> (c -> c)

これは単なる省略形です

\/c . (c -> c) -> (c -> c)

x = xこれはおそらく、 wherexが同じ定義域と共通定義域を持つ関数になるように制約されて いる型の最も一般的でない型 (型理論の最小上限) 式です。

与えられた「restrictedId」の型は、本当の意味で過度に一般的です。実行時型エラーにつながることは決してありませんが、前述のように、指定した式で記述された多くの型が(int -> int) -> (string -> string)あり、型がそれらを許可しても操作上不可能です。

于 2013-09-04T00:29:31.393 に答える