スコーレムって何？

質問

えーっ! GHCiが私のコードの中にSkolemsを発見しました!

...
Couldn't match type `k0' with `b'
  because type variable `b' would escape its scope
This (rigid, skolem) type variable is bound by
  the type signature for
    groupBy :: Ord b => (a -> b) -> Set a -> Set (b, [a])
The following variables have types that mention k0
...

彼らは何なのか？ 彼らは私のプログラムに何を望んでいるのか？ そして、なぜ彼らは逃げ出そうとしているのか（恩知らずの小悪党どもめ）？

どのように解決するのですか？

そもそも、あるコンテキストにおける "rigid" 型変数とは、そのコンテキスト外の量詞で束縛された型変数を意味し、したがって他の型変数と統一することはできない。

これはラムダによって束縛される変数と非常によく似ています。ラムダが与えられると (\x -> ... ) が与えられたら、もちろん外側から好きな値に適用することができます。 x の値はある特定の値であるべきだと決めることはできません。の値を選択することは x に対して値を選ぶことは、かなり馬鹿げているように聞こえますが、これが "can't match blah blah, rigid type variable, blah blah" についてのエラーが意味するところです。

なお、明示的な forall の量詞を使わなくても、トップレベルの型署名には暗黙のうちに forall を持ちます。

もちろん、これはあなたが得たエラーではありません。エスケープされた型変数が意味するものはもっと愚かなもので、ラムダの (\x -> ...) の特定の値を使おうとしているようなものだ。 x 外 というように、ラムダを引数に適用するのとは別に、ラムダを使うことができます。いや、ラムダを何かに適用してその結果値を使うのではなく、実際に 変数自体 を定義されたスコープ外で実際に使うということです。

ラムダの例のように明らかに不合理に見えることなく）型でこのようなことが起こるのは、quot;型変数" の2つの概念が出回っているからです。単一化の際、未確定の型を表すquot;変数"があり、これは型推論によって他の変数と識別される。一方、上記の定量化された型変数があり、これは可能な型に及ぶものとして明確に識別されます。

ラムダ式の型について考えてみましょう。 (\x -> x) . 完全に未決定の型から出発して a であることから、引数を1つ取り、それを絞って a -> b に、そして、引数と同じ型のものを返す必要があることがわかるので、さらに絞って a -> a . しかし、これでどんな型に対しても a が欲しいかもしれないので、量詞を与えます。 (forall a. a -> a) .

つまり、エスケープされた型変数は、GHCが未確定の型に統一されるべきだと推測する量詞によって束縛された型があるときに発生します。 の外側 の外にある未決定の型に統一されるべきだとGHCが推測しているときです。

どうやら、ここで実際に "skolem type variable" という用語を説明するのを忘れていたようです、へぇ。コメントで述べたように、私たちの場合、それは本質的に "rigid type variable" と同義なので、上記はまだアイデアを説明しています。

この用語がどこから来たのか完全にはわかりませんが、おそらくは スコーレム正規形 を表現し 実存的 を表現することができます。スコレム（またはリジッド）型変数とは、ある範囲内で、多相型の一部である、実存的データ型から来るなど、何らかの理由で未知の、しかし特定の型を持つものを指します。