¿Por qué no puedo declarar el tipo inferido?

Question

Tengo el siguiente:

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 

que genera este error cuando intento cargarlo en abrazos:

: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 

Y el siguiente error cuando se carga en 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) [] 

Sin embargo, cuando se elimina la declaración de tipo 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 

Las cargas de código bien y cuando se le pide ghci lo que el tipo de runcountacc es, obtenemos lo siguiente:

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

Por qué no puedo declarar el tipo inferido de runcountacc?

Answer 1

Supongo que cuando omite el tipo de firma, Haskell supone que no tiene la intención de utilizar la recursión polimórfica (para lo cual la inferencia de tipo no es tan efectiva). En consecuencia, cuando realiza esa llamada recursiva al runcountacc (n + 1) [], se considera que el tipo de elemento de lista es el mismo que en la llamada a función original. El proceso habitual de Hindley-Milner funciona bien, computando un tipo monomórfico uniforme para runcountacc, luego formando un esquema de tipos generalizando sobre las variables de tipo libre y las restricciones no resueltas.

Sin embargo, tan pronto como se escribe una declaración de tipo, que permiten la posibilidad de la repetición polimórfica, y cuando se llama runcountacc (n + 1) [], no hay ninguna razón para suponer que el tipo de elemento indeterminado de [] debe ser nada en particular. Sin embargo, este tipo indeterminado aún necesita una instancia Eq para satisfacer las restricciones en runcountacc, y no hay forma de averiguar qué instancia de Eq usar. Es genuinamente ambiguo.

Existen muchas maneras de reescribir este código para solucionar esta ambigüedad.

Answer 2

¿Por qué no puedo escribir el tipo inferido de runcountacc en el código?

La respuesta corta es que, debido a que creó la recursión polimórfica por error y se supone que la inferencia de tipo no funciona en absoluto si hay una recursión polimórfica.

GHC da una mejor mensaje de error:

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) [] 

Allí no se puede inferir el tipo para el lado derecho []. La siguiente firma soluciona el problema, ya que sin ella no está claro lista vacía de lo que se debe utilizar:

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

Tenemos una especie de (infinito) recursividad polimórfica aquí. El tipo de lista vacía del lado derecho puede ser cualquier cosa, y GHC no puede entender cuál. Por ejemplo, la siguiente es aún válida:

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

La pregunta de por qué el problema desaparece sin las firmas de tipos permanecen abiertos sin embargo.

La idea de @pigworker es que si omites las firmas, Haskell no permite la recursión polimórfica, y con la recitación monomórfica no hay ambigüedad.

NB: Tiene el caso base de recursión incorrecta - un bucle infinito no debe aparecer allí en primer lugar.