Что такое сколемы?

как я понимаю, "переменная Skolem" - это переменная, которая не соответствует никакой другой переменной, включая саму себя.

это, кажется, всплывает в Haskell, когда вы используете такие функции, как явные foralls, GADTs и другие системные расширения типа.

рассмотрим, например, следующий вид:

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

это говорит о том, что вы можете взять любой тип, который реализует Widget класс, и оберните его в AnyWidget тип. Теперь, предположим, вы попытаетесь развернуть это:

unwrap (AnyWidget w) = w

нет, ты не можешь этого сделать. Потому что во время компиляции мы понятия не имеем, какой тип w имеет, так что нет никакого способа, чтобы написать правильный тип подписи для этого. Вот тип w и "сбежал" от AnyWidget, что не допускается.

как я понимаю, внутренне GHC дает w тип, который является переменной Skolem, чтобы представить тот факт, что он не должен бежать. (Это не единственный такой сценарий, есть пару другие места, где определенное значение не может избежать из-за проблем с вводом.)

сообщение об ошибке появляется, когда переменная типа пытается выйти из своей области.

мне потребовалось некоторое время, чтобы понять это, поэтому я напишу пример.

{-# 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 тоже.
• в этот момент unifier пытается объединить y и I z, но он замечает, что z вводится в Нижнем контексте. Таким образом, он терпит неудачу.

в противном случае тип для unI будет иметь тип forall z. SomeI -> I z, но правильный -exists z. SomeI -> I z. Тем не менее, что один GHC не может представлять непосредственно.

---

точно так же мы можем понять, почему

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, который не может понять все последовательно.

EDIT: решение состоит в том, чтобы дать тип 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