스콜 렘은 무엇입니까?

스콜 렘은 무엇입니까?

---

Eeek! GHCi가 내 코드에서 Skolem을 찾았습니다!

...
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
...

그들은 무엇인가? 그들은 내 프로그램에서 무엇을 원합니까? 그리고 왜 그들은 도망치려 고하는 것일까 요?

---

우선 컨텍스트의 "고정"유형 변수는 해당 컨텍스트 외부의 수량 자에 의해 바인딩 된 유형 변수를 의미하므로 다른 유형 변수와 통합 할 수 없습니다.

이것은 람다로 묶인 변수와 매우 유사하게 작동합니다. 람다가 주어지면 (\x -> ... )"외부"에서 물론 원하는 값에 적용 할 수 있습니다. 그러나 내부적으로는의 값이 x특정 값이어야한다고 단순히 결정할 수는 없습니다 . x람다 내부에 대한 값을 선택하는 것은 꽤 어리석은 것처럼 들릴 것입니다. 그러나 이것이 "어쩌구 저쩌구, 딱딱한 유형 변수, 어쩌구 저쩌구"에 대한 오류의 의미입니다.

명시 적 forall한정자 를 사용하지 않더라도 모든 최상위 형식 서명에는 forall언급 된 각 형식 변수에 대해 암시 적이 있습니다.

물론 그것은 당신이 얻는 오류가 아닙니다. "이스케이프 된 유형 변수"가 의미하는 것은 훨씬 더 어리석은 것입니다. 마치 람다 를 갖고 인수에 적용하는 것과 관계없이 람다 외부 의 (\x -> ...)특정 값을 사용하려는 것과 같습니다 . 아니요, 람다를 무언가에 적용하지 않고 결과 값을 사용합니다. 실제로 정의 된 범위 밖에서 변수 자체를 사용한다는 의미 입니다.x

유형에서 이것이 발생할 수있는 이유는 (람다를 사용하는 예제처럼 명백하게 터무니없는 것처럼 보이지 않음) 두 가지 "유형 변수"개념이 떠 다니기 때문입니다. 통합하는 동안 결정되지 않은 유형을 나타내는 "변수"가 있고 식별 된 유형 추론을 통해 다른 변수와 함께. 반면에 위에서 설명한 수량화 된 유형 변수는 가능한 유형에 대한 범위로 구체적으로 식별됩니다.

람다 식의 유형을 고려하십시오 (\x -> x). 완전히 결정되지 않은 유형에서 시작하여 a하나의 인수를 취하고이를로 좁힌 a -> b다음 인수와 동일한 유형의 무언가를 반환해야한다는 것을 알 수 있으므로 더 좁 힙니다 a -> a. 그러나 이제는 a원하는 모든 유형에 대해 작동 하므로 수량 자를 제공합니다 (forall a. a -> a).

따라서 이스케이프 된 형식 변수는 GHC 가 해당 한정자의 범위를 벗어난 결정되지 않은 형식으로 통합되어야한다고 추론하는 한정자에 의해 바인딩 된 형식이있을 때 발생합니다 .

---

그래서 여기서 "skolem type variable"이라는 용어를 실제로 설명하는 것을 잊었습니다. 주석에서 언급했듯이, 우리의 경우 본질적으로 "강체 유형 변수"와 동의어이므로 위의 내용은 여전히 ​​아이디어를 설명합니다.

나는 그 용어가 어디서 유래했는지 완전히 확신하지 못하지만 GHC 에서처럼 Skolem 정규 형식 과 보편적 측면에서 실존 적 정량화를 포함한다고 생각합니다 . skolem (또는 rigid) 유형 변수는 어떤 범위 내에서 어떤 이유로 알 수 없지만 특정 유형 (존재 데이터 유형 & c에서 비롯된 다형성 유형의 일부)을 갖는 변수입니다.

---

내가 알기로 "Skolem 변수"는 자신을 포함하여 다른 변수와 일치하지 않는 변수입니다.

이것은 명시 적 foralls, GADT 및 기타 유형 시스템 확장과 같은 기능을 사용할 때 Haskell에서 나타나는 것처럼 보입니다.

예를 들어, 다음 유형을 고려하십시오.

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

이것이 말하는 것은 Widget클래스 를 구현하는 모든 유형을 가져 와서 유형으로 래핑 할 수 있다는 것 AnyWidget입니다. 이제 이것을 풀 려고한다고 가정합니다 .

unwrap (AnyWidget w) = w

음, 아니, 그렇게 할 수 없습니다. 왜냐하면 컴파일 타임에는 타입 w이 무엇인지 알지 못 하기 때문에 이에 대한 올바른 타입 서명을 작성할 방법이 없습니다. 여기서의 유형은 허용되지 않는 w에서 "이스케이프"되었습니다 AnyWidget.

내가 알기로 내부적으로 GHC는 wSkolem 변수 인 유형을 제공 하여 이스케이프해서는 안된다는 사실을 나타냅니다. (이것은 유일한 시나리오가 아닙니다. 입력 문제로 인해 특정 값이 이스케이프 할 수없는 몇 가지 다른 위치가 있습니다.)

---

유형 변수가 범위를 이스케이프하려고 할 때 오류 메시지가 나타납니다.

이것을 알아내는 데 시간이 좀 걸렸으므로 예제를 작성하겠습니다.

{-# 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
  • i온 LHS 종류가 I z몇 가지 유형을 z. forall수량 자 때문에 우리는 새로운 (새로운) 유형 변수를 도입해야했습니다. (SomeI i)표현 안에 묶여 있기 때문에 보편적이지 않습니다 .
  • 따라서 유형 변수를 x으로 통합 할 수 있습니다 SomeI. 괜찮습니다. 따라서 unI유형이 있어야합니다 SomeI -> y.
• i온 RHS 따라서 입력이 I z너무.
• At this point unifier tries to unify y and I z, but it notices that z is introduced in the lower context. Thus it fails.

Otherwise the type for unI would have type forall z. SomeI -> I z, but the correct one is exists z. SomeI -> I z. Yet that one GHC cannot represent directly.

---

Similarly, we can see why

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

works.

The (existential) variable inside AE x doesn't escape into outer scope, so everything is ok.

---

Also I encountered a "feature" in GHC 7.8.4 and 7.10.1 where RankNTypes on itself is ok, but adding GADTs triggers the error

{-# 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

So it might be nothing wrong with your code. It might be GHC, which cannot figure everything out consistently.

EDIT: The solution is to give a type to s :: forall a. I a -> String.

GADTs turn on MonoLocalBinds, which makes inferred type of s to have skolem variable, so the type is not forall a. I a -> String, but t -> String, were t gets bound in the wrong context. See: https://ghc.haskell.org/trac/ghc/ticket/10644

참고URL : https://stackoverflow.com/questions/12719435/what-are-skolems