戻り値の型として推測されるジェネリック関数の型チェックは、引数の型ではありません

私はSYBとランクnタイプについて学んでいて、単相制限のように見えるものの紛らわしいケースに出くわしました。

述語に一致する最も浅いエントリを見つける関数を作成しました。縮小関数の代わりに、を使用してより述語のような関数を受け入れ、それをAlternative自分でジェネリック関数に変換したかったのです。letこの実装で単相性の削減が型にどのように影響するかを確認するために、ブロック内の型注釈を省略することにしました。

shallowest :: (Alternative f, Typeable b) => (b -> f a) -> GenericQ (f a)
shallowest p z =
  let op = (empty `mkQ` p) in
    op z <|> foldl (<|>) empty (gmapQ op z)

これにより、letバインディングのあいまいさがタイプチェッカーによる制約の解決を妨げることを示唆するエラーが生成されますData a1。

Error: • Couldn't match type ‘d’ with ‘a1’
  ‘d’ is a rigid type variable bound by
    a type expected by the context:
      forall d. Data d => d -> m a
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      shallowest :: (b -> m a) -> GenericQ (m a)

（のような他の機関は、「 'mkQ'の使用から生じる（Typeable a0）を推測できませんでした」の行に沿っhead (gmapQ op z)たletバインディングのあいまいさについて明示的なエラーを引き起こします。上記の形式がなぜそうでないのかも理解していません） 。

（ScopedTypeVariablesが必要）のletブロックに注釈を追加すると、型エラーはなくなりop :: GenericQ (f a)ます。

ただし、Data制約が推測op できるように思われるので混乱しています。次の型は、戻り値の型の場合にチェックします。

shallowest p = let { op = (empty `mkQ` p) } in op

違いは何ですか？どちらの場合opもforall d. Data d => d -> f a;である必要があります。私が見る唯一の違いは、最初の位置が引数の位置にあり、2番目の位置が戻りの位置にあることです。

2番目のスニペットでopは、実際にはポリモーフィックではありません。

shallowest p = let { op = (empty `mkQ` p) } in op

これは微妙な違いopです。実際には単形ですが、オープンなコンテキストです。判断を入力するための通常の表記法でopは、右側の入力はin次のようになります。

 types         values
 ↓             ↓
 x, a, f, ...; op :: x -> f a, ... |- op :: x -> f a
                                            ↑
                                            monotype (no "forall")

 In English: "op has type (x -> f a) in the context consisting of type variables (x, a, f, ...) and values (op :: x -> f a, ...)"

shallowestトップレベルで発生する一般化ステップによって多形になります。型変数を持つコンテキストで、場合x, a, f, ...、本体がshallowest型を持つx -> f a、我々は、「コンテキストを閉じて」との型に型変数を移動することができますshallowest :: forall x a f. x -> f a。タイプの派生は次のようになります。

     x, a, f |- (let op = ... in op) :: x -> f a
 ⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻⸻ (generalization)
   |- (let op = .... in op) :: forall x a f. x -> f a

（型クラスと統合アルゴリズムによって物事はさらに複雑になりますが、それはこの答えのポイントの外にあります。）

ポリモーフィズムを使用したタイプチェックの主な問題は、一般化をいつ行うかを決定することです。主要なタイプの欠如と決定不可能性により、一般的な解決策はありません。したがって、タイプチェッカーの実装はいくつかの選択を行う必要があります。

Haskellでは、一般化は次の場所で行われます（リストは網羅的ではないかもしれません）。これはかなり自然な選択です。

• 関数定義、つまり、let少なくとも1つの明示的な引数を持つトップレベルのバインディング（これが単相性の制限です）。

• 上位機能の多型の引数：あなたが機能を持っている場合はf :: (forall a. w a) -> r、その後、f x一般化しようとしているa型チェック時にx、

• そしてもちろん、明示的な注釈によって指示された場合_ :: forall a. t a。

予備的注記：ここに提示された証拠を考慮して、私はあなたが以下を使用していると仮定します：

• type GenericQ r = forall a . Data a => a -> r sybから、そして
• gmapQ :: Data a => (forall d. Data d => d -> u) -> a -> [u] からData.Data。

間違えたら教えてください。また、forall以下のsは明示的に記述されます。

ここには目に見える以上のものがあります。Li-yao Xiaが示唆しているように、それはのタイプを含む一般化の問題ですop。あなたの最初の定義について3つの関連する事実がありますshallowest：

1. 一般化の前に、の推定タイプはopですData d => d -> f a。Data d制約がある場合、単相制限のルール1（レポートのサブセクション4.5.5を参照）はd、このタイプでは一般化できないことを意味します。

2. の本文ではshallowest、op2か所に表示されます。最初のものはop zでありz :: a1、の署名によってトップレベルでバインドおよび制約されますshallowest。結論として、この発生は引数タイプの一般化を必要とopしないということです。それに関する限り、タイプはタイプ変数で単形であるop可能性がforall f a. a1 -> f aありますa1（この用語はレポートのサブセクション4.5.4から取得しました）。

3. ただし、他の発生はgmapQ op zです。gmapQランク2タイプであり、多形引数が必要です。そのため、opLi-yao Xiaの回答の最後に記載されているように、この発生には引数タイプの一般化が必要です。

＃1と＃3は矛盾する要件であるため、型エラーが発生します。これは、単相制限を無効にするかop、署名付きの引数型で多態性を要求することで回避できます。op＃2で説明した他の発生のおかげで、状況は2つの発生を含む不一致として報告されます。

以下は、何が起こっているかを確認するのに役立つ可能性のある、より最小限の拡張例です。（ほかに、あなたは、GHCiのに次のスニペットをウンチしようとしている場合は-XRankNTypes、あなたも設定する必要があります-XMonomorphismRestrictionし、-XNoExtendedDefaultRules同じ結果を見るために。）

これはランク2タイプの関数であり、次の役割を果たしgmapQます。

glub :: (forall x. Show x => x -> String) -> String
glub f = f 7

それでは、以下を含むシナリオと同様のシナリオを試してみましょうshallowest...

foo1 :: forall a. Show a => a -> String
foo1 x = bar x ++ glub bar
  where
  bar = show

...そしてあなたのエラーがあります：

<interactive>:506:23: error:
    • Couldn't match type ‘x’ with ‘a’
      ‘x’ is a rigid type variable bound by
        a type expected by the context:
          forall x. Show x => x -> String
        at <interactive>:506:18-25
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo1 :: forall a. Show a => a -> String
        at <interactive>:505:1-38
      Expected type: x -> String
        Actual type: a -> String
    • In the first argument of ‘glub’, namely ‘bar’
      In the second argument of ‘(++)’, namely ‘glub bar’
      In the expression: bar x ++ glub bar
    • Relevant bindings include
        bar :: a -> String (bound at <interactive>:508:3)
        x :: a (bound at <interactive>:506:5)
        foo1 :: a -> String (bound at <interactive>:506:1)

の署名がbar必要な場所にワイルドカードを追加すると、少し示唆に富む追加のエラーが発生します。

foo2 :: forall a. Show a => a -> String
foo2 x = bar x ++ glub bar
  where
  bar :: _
  bar = show

• Found type wildcard ‘_’ standing for ‘a -> String’
  Where: ‘a’ is a rigid type variable bound by
           the type signature for:
             foo2 :: forall a. Show a => a -> String
           at <interactive>:511:1-38
  To use the inferred type, enable PartialTypeSignatures
• In the type signature: bar :: _
  In an equation for ‘foo2’:
      foo2 x
        = bar x ++ glub bar
        where
            bar :: _
            bar = show
• Relevant bindings include
    x :: a (bound at <interactive>:512:5)
    foo2 :: a -> String (bound at <interactive>:512:1)

ワイルドカード「の略」が、の型シグネチャによってバインドさa -> Stringれるのとは別の事実としてどのように記述されているかに注意してください。これは、上記のポイント2で触れた、型変数の単型と多型の違いに対応していると思います。afoo2

barポリモーフィック型の署名を与えると、それが機能します。

foo3 :: forall a. Show a => a -> String
foo3 x = bar x ++ glub bar
  where
  bar :: forall b. Show b => b -> String
  bar = show

また、バーの定義を意味のあるものにすることも同様です。これにより、バーを「単純なパターンバインディング」ではなく「関数バインディング」にすることで、単相性の制限を回避できます。

foo4 :: forall a. Show a => a -> String
foo4 x = bar x ++ glub bar
  where
  bar x = show x

完全を期すために、型に制約がないということは、単相性の制限がないことを意味することに注意してください。

foo5 :: forall a. Show a => a -> String
foo5 x = bar x ++ glub bar
  where
  bar = const "bar"

関連する状況では、bar2回使用しますが、ランク2関数は使用しません。

foo6 x y = bar x ++ bar y
  where
  bar = show

GHCはどのタイプを推測しfoo6ますか？

GHCi> :t foo6
foo6 :: Show a => a -> a -> [Char]

引数は同じ型を取得します。そうでない場合は、の一般化がbar必要になり、型シグネチャ（またはポイントフルネスなど）が必要になります。

foo7 x y = bar x ++ bar y
  where
  bar :: forall a. Show a => a -> String
  bar = show

GHCi> :t foo7
foo7 :: (Show a1, Show a2) => a1 -> a2 -> [Char]

私はまだそれについて言及しなかったので、ここにあなたの2番目のアナログがありますshallowest：

foo8 :: forall a. Show a => a -> String 
foo8 x = bar x
  where
  bar = show

ここではbar実際には一般化されていないことを強調する価値があります。それは型変数では単形ですa。：foo7ではなくをいじることで、この例を破ることができますbar。

foo9 = bar
  where
  bar :: _
  bar = show

この場合、barは一般化されておらず、どちらも一般化されていませんfoo（現在はポイントフリーで署名なし）。つまり、単相型変数は決して解決されません。モニック射制限のルール2に関しては、あいまいな型変数になります。

    <interactive>:718:14: error:
        • Found type wildcard ‘_’ standing for ‘a0 -> String’
          Where: ‘a0’ is an ambiguous type variable
          To use the inferred type, enable PartialTypeSignatures
        • In the type signature: bar :: _
          In an equation for ‘foo9’:
              foo9
                = bar
                where
                    bar :: _
                    bar = show
        • Relevant bindings include
            foo9 :: a0 -> String (bound at <interactive>:716:5)

<interactive>:719:13: error:
    • Ambiguous type variable ‘a0’ arising from a use of ‘show’
      prevents the constraint ‘(Show a0)’ from being solved.
      Relevant bindings include
        bar :: a0 -> String (bound at <interactive>:719:7)
        foo9 :: a0 -> String (bound at <interactive>:716:5)
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance Show a => Show (ZipList a)
          -- Defined in ‘Control.Applicative’
        instance Show Constr -- Defined in ‘Data.Data’
        instance Show ConstrRep -- Defined in ‘Data.Data’
        ...plus 64 others
        ...plus 250 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: show
      In an equation for ‘bar’: bar = show
      In an equation for ‘foo9’:
          foo9
            = bar
            where
                bar :: _
                bar = show

barの定義に型シグネチャを追加してfoo9も役に立ちません。エラーが報告されるポイントを変更するだけです。bar制約のないものに変更するbarと、との両方を一般化できるため、エラーがなくなりますfoo。