Как работает IncoherentInstances?

Играя с некоторым кодом:

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Arity f where
  arity :: f -> Int

instance Arity x where
  arity _ = 0

instance Arity f => Arity ((->) a f) where
  arity f = 1 + arity (f undefined)

Без IncoherentInstances:

ghci> arity foldr
blah blah ambiguous blah blah possible fix blah
ghci> arity (foldr :: (a -> Int -> Int) -> Int -> [a] -> Int)
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3
2

Если мы добавим IncoherentInstances в список прагм, тогда он может обрабатывать foldr, не нуждаясь в мономорфной сигнатуре типа, но получает неправильный ответ на lambdas:

ghci> arity foldr
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3 -- should be 2
0

Что такое черная магия за Incoherent Instances? Почему он делает то, что здесь делает?

Ответ 1

Ну, это довольно сложно. Давайте начнем с неоднозначной ошибки:

<interactive>:1:1:
    Ambiguous type variable `b0' in the constraint:
      (Arity b0) arising from a use of `arity'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: arity foldr
    In an equation for `it': it = arity foldr

Как правило, без совпадающих экземпляров при попытке сопоставить тип с классом он будет сравнивать тип со всеми экземплярами для этого класса. Если есть ровно одно совпадение, он будет использовать этот экземпляр. В противном случае вы либо получите ошибку экземпляра без экземпляра (например, с помощью show (*)), либо ошибку перекрывающихся экземпляров. Например, если вы удаляете функцию языка OverlappingInstances из вышеуказанной программы, вы получите эту ошибку с помощью arity (&&):

<interactive>:1:1:
    Overlapping instances for Arity (Bool -> Bool -> Bool)
      arising from a use of `arity'
    Matching instances:
      instance Arity f => Arity (a -> f)
        -- Defined at tmp/test.hs:9:10-36
      instance Arity x -- Defined at tmp/test.hs:12:10-16
    In the expression: arity (&&)
    In an equation for `it': it = arity (&&)

Он соответствует Arity (a -> f), поскольку a может быть Bool и f может быть Bool -> Bool. Он также соответствует Arity x, поскольку x может быть Bool -> Bool -> Bool.

С OverlappingInstances, когда вы сталкиваетесь с ситуацией, когда могут совпадать два или более экземпляра, если есть наиболее конкретный, он будет выбран. Экземпляр x более специфичен, чем экземпляр Y, если x может соответствовать Y, но не наоборот.

В этом случае (a -> f) соответствует x, но x не соответствует (a -> f) (например, рассмотрите x как Int). Таким образом, Arity (a -> f) более конкретный, чем Arity x, поэтому, если оба соответствуют первому, будут выбраны.

Используя эти правила, arity (&&) будет сначала соответствовать Arity ((->) a f), причем a будет Bool, а f будет Bool -> Bool. В следующем матче будет a Bool и f - bool. Наконец, он завершит сопоставление Arity x, при этом x будет Bool.

Обратите внимание на приведенную выше функцию, (&&) результат представляет собой конкретный тип Bool. Что происходит, когда тип не является конкретным? Например, давайте посмотрим на результат arity undefined. undefined имеет тип a, поэтому он не является конкретным типом:

<interactive>:1:1:
    Ambiguous type variable `f0' in the constraint:
      (Arity f0) arising from a use of `arity'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: arity undefined
    In an equation for `it': it = arity undefined

Вы получаете ошибку переменной типа, как и для foldr. Почему это происходит? Это потому, что в зависимости от того, что a, потребуется другой экземпляр. Если a был Int, то экземпляр Arity x должен быть сопоставлен. Если a был Int -> Int, то экземпляр Arity ((->) a f) должен быть сопоставлен. Из-за этого ghc отказывается компилировать программу.

Если вы заметите тип foldr: foldr :: forall a b. (a -> b -> b) -> b -> [a] -> b, вы заметите ту же проблему: результат не является конкретной переменной.

Вот где IncoherentInstances входит: с включенной функцией языка, он будет игнорировать вышеупомянутую проблему и просто выбрать экземпляр, который всегда будет соответствовать переменной. Например, с arity undefined, Arity x всегда будет соответствовать a, поэтому результат будет равен 0. Аналогичная операция выполняется для foldr.

Теперь для второй проблемы, почему arity $ \x y -> 3 возвращает 0, когда IncoherentInstaces включен?

Это очень странное поведение. Этот следующий сеанс ghci покажет, насколько странно это:

*Main> let f a b = 3
*Main> arity f
2
*Main> arity (\a b -> 3)
0

Это заставляет меня думать, что есть ошибка в ghc, где \a b -> 3 видно, что IncoherentInstances имеет тип x вместо a -> b -> Int. Я не могу придумать, почему эти два выражения не должны быть точно такими же.