Haskell tipo matices del sistema

Question

He estado metiéndome en lo esencial del sistema de tipos haskell y tratando de llegar a los puntos finos de las clases tipográficas. Aprendí un montón, pero estoy golpeando una pared en los siguientes pedazos de código.

El uso de estas definiciones de clase e instancia:

class Show a => C a where 
    f :: Int -> a 

instance C Integer where 
    f x = 1 

instance C Char where 
    f x = if x < 10 then 'c' else 'd' 

Por qué es que este tipo pasa el corrector:

pero esto no lo hace?

g :: C a => a -> Int -> String 
g x y = show(f y) 

me parece la segunda alternativa mucho más fácil de leer, y parece ser sólo una pequeña diferencia (tenga en cuenta las firmas de tipos). Sin embargo, tratando de pasar eso, los resultados de typechecker en:

*Main> :l typetests.hs 
[1 of 1] Compiling Main    (typetests.hs, interpreted) 

typetests.hs:11:14: 
    Ambiguous type variable `a0' in the constraints: 
     (C a0) arising from a use of `f' at typetests.hs:11:14 
     (Show a0) arising from a use of `show' at typetests.hs:11:9-12 
    Probable fix: add a type signature that fixes these type variable(s) 
    In the first argument of `show', namely `(f y)' 
    In the expression: show (f y) 
    In an equation for `g': g x y = show (f y) 
Failed, modules loaded: none. 

Y no entiendo por qué.

Nota: No pregunte "¿Qué está intentando hacer?" Espero que sea obvio que estoy metiéndome en un contexto abstracto para sondear el funcionamiento de este lenguaje. No tengo otro objetivo en mente que aprender algo nuevo.

Gracias

Answer 1

Aquí es donde un juguete divertido entra en juego. Considere la función Preludio estándar asTypeOf.

asTypeOf :: a -> a -> a 
asTypeOf = const 

Simplemente devuelve su primer argumento, sin importar cuál sea el segundo argumento. Pero la firma de tipo en él coloca la restricción adicional de que ambos argumentos deben ser del mismo tipo.

g :: C a => a -> Int -> String 
g x y = show (f y `asTypeOf` x) 

Ahora, GHC sabe lo que el tipo de f y es. Es lo mismo que el tipo del primer argumento en g. Sin esa información, bueno, recibes el mensaje de error que viste. Simplemente no había suficiente información para determinar el tipo de f y. Y dado que el tipo es importante (se usa para determinar qué instancia usar para show), GHC necesita saber qué tipo de código desea generar.

Answer 2

En

g :: C a => a -> Int -> a 
g x y = f y 

el tipo de retorno de f y se fija por la firma de tipo, por lo que si usted llama, por ejemplo, g 'a' 3, instance C Char serán utilizados. Pero en

g :: C a => a -> Int -> String 
g x y = show(f y) 

hay dos restricciones sobre el tipo de devolución de f: debe ser una instancia de C (de modo que se puede utilizar f) y de Show (de modo que show puede ser utilizado). ¡Y eso es todo! La coincidencia de los nombres de variable de tipo a en las definiciones de f y g no significa nada. Por lo tanto, el compilador no tiene forma de elegir entre instance C Char y instance C Integer (o cualquier instancia definida en otros módulos, por lo que eliminar estas instancias no hará que el programa se compile).

Answer 3

Esta es una variante del notorio problema show . read. La versión clásica utiliza

read :: Read a => String -> a 
show :: Show a => a -> String 

por lo que la composición podría parecer ser un transductor de cadena simple y llano

moo :: String -> String 
moo = show . read 

excepto que no hay información en el programa para determinar el tipo en el medio, por lo tanto, lo que debe read y luego show.

Ambiguous type variable `b' in the constraints: 
    `Read b' arising from a use of `read' at ... 
    `Show b' arising from a use of `show' at ... 
Probable fix: add a type signature that fixes these type variable(s) 

Por favor, no ghci hace un montón de locos extra por defecto, resolviendo la ambigüedad arbitrariamente.

> (show . read) "()" 
"()" 

Su clase C es una variante de Read, excepto que decodifica un Int en lugar de leer un String, pero el problema es esencialmente el mismo.

entusiastas del sistema de tipo notarán que las variables de tipo subestimados no son per se un gran problema. Es ambiguo instancia de inferencia ese es el problema aquí. Considere

poo :: String -> a -> a 
poo _ = id 

qoo :: (a -> a) -> String 
qoo _ = "" 

roo :: String -> String 
roo = qoo . poo 

En la construcción de roo, nunca se determina cuál es el tipo en el medio debe ser, ni es roo polimórficos en ese tipo. ¡La inferencia de tipo no resuelve ni generaliza la variable! Aun así,

> roo "magoo" 
"" 

no es un problema, porque la construcción es paramétrico en el tipo desconocido. El hecho de que el tipo no pueda determinarse tiene la consecuencia de que el tipo no puede materia.

Pero desconocido instancias claramente importa. El resultado de integridad para la inferencia de tipo Hindley-Milner se basa en la parametricidad y, por lo tanto, se pierde cuando agregamos la sobrecarga. No lloremos por ello.