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


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

что это такое? Что им нужно от моей программы? И почему они пытаются убежать (неблагодарные маленькие мерзавцы)?

3 58

3 ответа:

начнем с того, что" жесткая " переменная типа в контексте означает переменную типа, связанную квантором вне этого контекста, которая, таким образом, не может быть объединена с другими переменными типа.

это работает очень похоже на переменные, связанные лямбда: учитывая лямбда (\x -> ... ), из "снаружи" вы можете применить его к любому значению, которое вам нравится, конечно; но внутри вы не можете просто решить, что значение x должно быть какое-то конкретное значение. Выбор значения для x внутри лямбда должно звучать довольно глупо, но это то, что ошибки о "не может соответствовать бла-бла, жесткая переменная типа, бла-бла" означает.

обратите внимание, что даже без использования явных forall кванторы, любая подпись типа верхнего уровня имеет неявное forall для каждого типа упомянутых переменных.

конечно, это не та ошибка, которую вы получаете. То, что означает" экранированная переменная типа", еще глупее-это похоже на лямбду (\x -> ...) и пытается использовать определенные значения xза пределами лямбда, независимо от применения его в качестве аргумента. Нет, не применяя лямбду к чему-то и используя значение результата--я имею в виду фактически используя переменная вне области, где он определен.

причина, по которой это может произойти с типами (не кажущимися столь же очевидно абсурдными, как пример с лямбда), заключается в том, что есть два понятия "переменных типа", плавающих вокруг: во время объединения у вас есть " переменные" представление неопределенных типов, которые затем идентифицируются с другими такими переменными с помощью вывода типа. С другой стороны, у вас есть количественные переменные типа, описанные выше, которые специально определены как ранжирование по возможным типам.

рассмотрим тип лямбда-выражения (\x -> x). Начиная с совершенно неопределенного типа a, мы видим, что требуется один аргумент и сузить его до a -> b, то мы видим, что он должен вернуть что-то того же типа, что и его аргумент, поэтому мы сузим его до a -> a. Но теперь он работает для любого типа a вы можете захотеть, поэтому мы даем ему Квантор (forall a. a -> a).

таким образом, экранированная переменная типа возникает, когда у вас есть тип, связанный квантором, который выводит GHC, должен быть объединен с неопределенным типом за пределами область действия этого квантора.


так что, видимо, я забыл на самом деле объяснить термин "переменная типа skolem" здесь, хех. Как уже упоминалось в комментариях, в в нашем случае это по существу синоним "жесткой переменной типа", поэтому вышеизложенное все еще объясняет идею.

Я не совсем уверен, откуда взялся этот термин, но я бы предположил, что он включает нормальная форма Сколема и представляющий экзистенциальные количественная оценка с точки зрения универсальности, как это делается в GHC. Переменная типа skolem (или rigid) - это переменная, которая в некоторой области имеет неизвестный, но определенный тип по какой-то причине, являясь частью полиморфного типа, исходя из экзистенциального типа данных, &c.

как я понимаю, "переменная 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