¿Cómo es el tipo de `([] ==) []` inferido haskell?

Question

Suena tonto, pero no puedo entenderlo. ¿Por qué la expresión [] == [] se puede escribir? Más específicamente, ¿qué tipo (en la clase Eq) se deduce del tipo de elementos de lista?

En una sesión ghci, veo lo siguiente:

Prelude> :t (==[]) 
(==[]) :: (Eq [a]) => [a] -> Bool 

Pero la restricción Eq [a] implica Eq a también, como se muestra aquí:

Prelude> (==[]) ([]::[IO()]) 

<interactive>:1:1: 
No instance for (Eq (IO())) 
    arising from use of `==' at <interactive>:1:1-2 
Probable fix: add an instance declaration for (Eq (IO())) 
In the definition of `it': it = (== []) ([] :: [IO()]) 

Así, en [] == [] , el verificador de tipos debe asumir que el elemento de lista es de algún tipo a que está en la clase Eq. ¿Pero cual? El tipo de [] es solo [a], y esto es ciertamente más general que Eq a => [a].

mi humilde opinión, esto debería por ambigua, al menos en Haskell 98 (que es lo que estamos hablando)

Answer 1

GHCi tiene extended rules for type defaulting, que es lo que te hizo tropezar. En este caso, creo que dejaría el tipo ambiguo predeterminado en (). Las maneras sutiles en que GHCi se comporta de manera diferente son agradables por el bien de una mejor interactividad, pero a veces ocasionan confusión ...

Answer 2

GHC infiere el tipo más general:

(== []) :: (Eq a) => [a] -> Bool

debe leerse como:

• si tiene una instancia de una ecuación,
• continuación, Haskell le puede dar una función de las listas de los 'un es a Bool

Así que sí, la implicación aquí es que usted tiene una instancia de la ecuación para los elementos de la lista, y GHC ya tiene una instancia para las listas en general (confiando en Eq para los elementos), así obtenemos un buen tipo general.

El comprobador de tipos "asume" que puede proporcionar una instancia de Eq cuando se llama a un tipo en particular.

No puedo reproducir los resultados de tener una restricción de Eq [a].