74

イーク！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
...

彼らは何ですか？彼らは私のプログラムに何を望んでいますか？そして、なぜ彼らは逃げようとしているのですか（恩知らずの小さなブライター）？

4

4 に答える 4

58

まず、コンテキスト内の「厳密な」型変数とは、そのコンテキスト外の数量詞によってバインドされた型変数を意味します。したがって、他の型変数と統合することはできません。

これは、ラムダによってバインドされた変数のように非常に機能します。ラムダが与えられると(\x -> ... )、「外部」から、もちろん、好きな値に適用できます。xしかし、内部では、の値を特定の値にする必要があると単純に判断することはできません。ラムダ内の値をx選択するのはかなりばかげているように聞こえますが、それが「何とか何とか、リジッド型変数、何とか何とか一致できない」というエラーが意味することです。

forall明示的な数量詞を使用しなくても、最上位の型シグニチャには、forall言及されている型変数ごとに暗黙的なものがあることに注意してください。

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

これが型で発生する可能性がある理由（ラムダの例のように明らかにばかげているようには見えない）は、「型変数」の2つの概念が浮かんでいるためです。統合中に、未決定の型を表す「変数」があり、それが識別されます。型推論を介して他のそのような変数と。一方、上記の定量化された型変数は、可能な型に及ぶものとして具体的に識別されます。

ラムダ式のタイプを考えてみましょう(\x -> x)。完全に未決定の型から始めて、a1つの引数を取りa -> b、それをに絞り込みます。次に、引数と同じ型の何かを返す必要があることがわかります。したがって、さらに絞り込みa -> aます。しかし、今ではaあなたが望むどんなタイプでも機能するので、数量詞を与え(forall a. a -> a)ます。

したがって、エスケープされた型変数は、GHCが推測する数量詞によってバインドされた型があり、その数量詞の範囲外の未決定の型と統合する必要がある場合に発生します。

ですから、ここで「スコーレム型変数」という用語を実際に説明するのを忘れたようです。コメントで述べたように、私たちの場合、それは本質的に「剛体型変数」と同義であるため、上記はまだアイデアを説明しています。

この用語がどこから来たのか完全にはわかりませんが、GHCで行われているように、スコーレム標準形を含み、普遍的な観点から存在記号を表すと思います。スコーレム（またはリジッド）型変数は、ある範囲内で、何らかの理由で未知であるが特定の型を持つ変数です。つまり、実存的なデータ型に由来するポリモーフィック型の一部です。

于 2012-10-04T02:43:05.053 に答える
23

私が理解しているように、「スコーレム変数」は、それ自体を含む他のどの変数とも一致しない変数です。

これは、明示的なforall、GADT、その他の型システム拡張機能などの機能を使用すると、Haskellでポップアップするようです。

たとえば、次のタイプについて考えてみます。

data AnyWidget = forall x. Widget x => AnyWidget x

これは、クラスを実装する任意の型を取得して、Widgetそれを型にラップできることを意味しますAnyWidget。ここで、これをアンラップしようとしたとします。

unwrap (AnyWidget w) = w

ええと、いや、あなたはそれをすることはできません。なぜなら、コンパイル時には、型が何であるかわからないwため、これに対して正しい型シグネチャを記述する方法がないからです。ここで、タイプはwから「エスケープ」されてAnyWidgetいますが、これは許可されていません。

私が理解しているように、内部的にGHCはw、エスケープしてはならないという事実を表すために、Skolem変数である型を提供します。（このようなシナリオはこれだけではありません。入力の問題のために特定の値をエスケープできない場所が他にもいくつかあります。）

于 2012-10-04T08:06:44.080 に答える
11

型変数がそのスコープをエスケープしようとすると、エラーメッセージがポップアップ表示されます。

これを理解するのに少し時間がかかったので、例を書きます。

{-# LANGUAGE ExistentialQuantification #-}
data I a = I a deriving (Show)
data SomeI = forall a. MkSomeI (I a)

次に、関数を書き込もうとすると

 unI (MkSomeI i) = i

GHCは、この関数の型推論/型チェックを拒否します。

なんで？自分でタイプを推測してみましょう。

  • unIはラムダ定義であるため、その型はx -> y一部の型xとy。
  • MkSomeIタイプがありますforall a. I a -> SomeI
    • MkSomeI iタイプがありますSomeI
    • iLHSには、あるタイプI zのタイプがありzます。数量詞のため、forall新しい（新しい）型変数を導入する必要がありました。式の内部にバインドされているため、普遍的ではないことに注意してください(SomeI i)。
    • したがって、型変数xをと統合できますSomeI。これで問題ありません。したがって、unIはタイプが必要SomeI -> yです。
  • iしたがって、RHSにはタイプI zもあります。
  • この時点で、unifierはyandをunifyしようとしますが、それが下位コンテキストで導入されてI zいることに気付きます。zしたがって、失敗します。

それ以外の場合、のタイプはタイプになりますが、正しいタイプはunIです。しかし、その1つのGHCは直接表すことはできません。forall z. SomeI -> I zexists z. SomeI -> I z

同様に、理由がわかります

data AnyEq = forall a. Eq a => AE a
-- reflexive :: AnyEq -> Bool
reflexive (AE x) = x == x

動作します。

内部の（存在する）変数AE xは外部スコープにエスケープされないため、すべて問題ありません。

また、GHC 7.8.4および7.10.1で「機能」に遭遇しましたがRankNTypes、それ自体は問題ありませんが、追加GADTsするとエラーが発生します

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

example :: String -> I a -> String
example str x = withContext x s
  where
    s i = "Foo" ++ str

withContext :: I a -> (forall b. I b -> c) -> c
withContext x f = f x

したがって、コードに問題はない可能性があります。すべてを一貫して把握できないGHCの可能性があります。

編集：解決策は、に型を与えることs :: forall a. I a -> Stringです。

GADTsをオンにMonoLocalBindsすると、推論された型sがskolem変数を持つようになるため、型はではありませんforall a. I a -> Stringがt -> String、t間違ったコンテキストでバインドされます。参照：https ：//ghc.haskell.org/trac/ghc/ticket/10644

于 2015-07-16T13:34:46.200 に答える
0

スコーレムとは？

存在記号変数IEは、「外界は知ることができないが、内界は知ることができる、剛体/具体的なタイプを持っている」。

では、Skolemsをどのように使用しますか？

TL; DR

unwrapBroken (ExistentiallyTyped x) = x

unwrapOk (ExistentiallyTyped x) = useConstraint x

Skolemは、気になるタイプクラスのインスタンスがある場合に役立ちます。アンラップされたものは、その制約を介して（のみ？）使用できます。

簡潔にするために、ここにエスケープするスコーレム（a内のforall a. ExistentiallyTyped a）があります：

data ExistentiallyTyped = forall a. SomeConstraint a => ExistentiallyTyped a

unwrapBroken :: forall a. ExistentiallyTyped -> a  <---- what? how'd that `a` break out? not the same `a` as in ExistentiallyTyped
unwrapBroken (ExistentiallyTyped x) = x :: a  <---- not the same `a` as above!

あなたはそれをすることはできません、それaはラッピングx :: a内で定量化されていますが、ライン上でExistentiallyTyped考えてください。今ではどういうわけか全称記号化されていますか？！（注意、これは依存型で可能になり始めていると思いますが、haskellにはまだありません...）。つまり、この関数はまたはを返すことができると私に言っていますか？aunwrapBroken :: forall a. ...IntStringAnyFrigginThing

いいえ。ただし、その制約を介してそれを利用できます。x :: a

unwrapOk :: ExistentiallyTyped -> ResultOfUseConstraint
unwrapOk (ExistentiallyTyped x) = useConstraint x

たとえば、ある型クラスを共有する型のリストが必要な場合は、これを利用しました。

notPossible :: HasBork a => [Proxy a]
notPossible = [Proxy @Thing1, Proxy @Thing2]
-- Error! expected a `Proxy a` but got a `Proxy Thing1`

代わりに：

data Borkable = forall a. HasBork a => Borkable a

borks :: [Borkable]
borks = [thing1, thing2]

later = useBork <$> borks
于 2021-02-04T23:34:36.423 に答える