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

Question

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

{-# 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 не нуждаясь в сигнатуре мономорфного типа, но он получает неправильный ответ на лямбдах:

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? Почему он делает то, что делает здесь?

Answer 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

Обычно, без перекрывающихся экземпляров, при попытке сопоставления типа с классом он сравнивает тип со всеми экземплярами этого класса. Если есть только одно совпадение, он будет использовать этот экземпляр. Overwise вы либо получите ошибку без экземпляра (например, с 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 быть булл Наконец это закончится сопоставление 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, Я не могу придумать причину, по которой эти два выражения не должны быть абсолютно одинаковыми.