Почему я не могу объявить предполагаемый тип?

Question

У меня есть следующее:

runcount :: (Eq a, Num b) => [a] -> b
runcount = runcountacc 0

runcountacc :: (Eq a, Num b) => b -> [a] -> b
runcountacc n (_:[]) = runcountacc (n+1) []
runcountacc n (x:xs) = runcountacc (n+(if head xs==x then 0 else 1)) xs 
runcountacc n _ = n

, которое генерирует эту ошибку при попытке загрузить ее в Hugs:

:6 - Cannot justify constraints in explicitly typed binding
*** Expression    : runcountacc
*** Type          : (Eq a, Num b) => b -> [a] -> b
*** Given context : (Eq a, Num b)
*** Constraints   : Eq c

и следующую ошибку при загрузке в ghci:

:6:23: Ambiguous type variable `a0' in the constraint:
  (Eq a0) arising from a use of `runcountacc'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: runcountacc (n + 1) []
In an equation for `runcountacc':
   runcountacc n ([x]) = runcountacc (n + 1) []

Однако при удалении объявления типа runcountacc:

runcount :: (Eq a, Num b) => [a] -> b
runcount = runcountacc 0

runcountacc n (_:[]) = runcountacc (n+1) []
runcountacc n (x:xs) = runcountacc (n+(if head xs==x then 0 else 1)) xs 
runcountacc n _ = n

Код загружается нормально, и когда ghci спрашивают, что это за тип runcountacc, мы получаем следующее:

λ> :t runcountacc 
runcountacc :: (Num a, Eq a1) => a -> [a1] -> a

Почему я не могу объявить предполагаемый тип runcountacc?

Answer 1

Я предполагаю, что когда вы пропускаете сигнатуру типа, Haskell предполагает, что вы не собираетесь использовать полиморфную рекурсию (для которой выведение типа не так эффективно). Соответственно, когда вы делаете этот рекурсивный вызов runcountacc (n + 1) [], тип элемента списка принимается таким же, как в исходном вызове функции. Обычный процесс Хиндли-Милнера работает нормально, вычисляя однородный мономорфный тип для runcountacc, затем формируя схему типов, обобщая переменные свободного типа и нерешенные ограничения.

Однако, как только вы пишете сигнатуру типа, вы допускаете возможность полиморфной рекурсии, и когда вы вызываете runcountacc (n + 1) [], нет никаких оснований предполагать, что неопределенный тип элемента для [] должен быть чем-то в конкретный. Однако этому неопределенному типу все еще требуется экземпляр Eq, чтобы удовлетворить ограничения на runcountacc, и нет способа выяснить, какой экземпляр Eq использовать. Это действительно неоднозначно.

Существует множество способов переписать этот код, чтобы устранить эту неоднозначность.

Answer 2

Почему я не могу написать предполагаемый тип runcountacc в коде?

Короткий ответ: если вы создали полиморфную рекурсию по ошибке, то вывод типа не должен работатьвообще, если присутствует полиморфная рекурсия.

GHC дает лучшее сообщение об ошибке:

orig.hs:5:24:
    Ambiguous type variable `a0' in the constraint:
      (Eq a0) arising from a use of `runcountacc'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: runcountacc (n + 1) []
    In an equation for `runcountacc':
        runcountacc n (_ : []) = runcountacc (n + 1) []

Там он не может вывести тип для правой стороны [].Следующая подпись решает проблему, потому что без нее не ясно пустой список того, что следует использовать:

runcountacc n (_:[]) = runcountacc (n+1) ([] :: [a])

У нас есть некая (бесконечная) полиморфная рекурсия здесь.Тип пустого списка справа может быть любым, и GHC не может понять, какой именно.Например, все еще действует следующее:

runcountacc n (_:[]) = runcountacc (n+1) ([] :: [String])

Вопрос о том, почему проблема исчезает без сигнатур типов, остается открытым.

Идея @pigworker заключается в том, что если вы опустите сигнатуры,Haskell запрещает полиморфную рекурсию, и с мономорфным рекурсией нет никакой двусмысленности.

Примечание: у вас неправильный базовый случай рекурсии - бесконечный цикл не должен появляться на первом месте.