Para empezar, una variable de tipo "rígido" en un contexto significa una variable de tipo ligada por un cuantificador fuera de ese contexto, que por lo tanto no se puede unificar con otras variables de tipo.
Esto funciona en gran medida como variables vinculadas por una lambda: dado un lambda (\x -> ...), desde el "exterior" puede aplicarlo a cualquier valor que desee, por supuesto; pero en el interior, no puede simplemente decidir que el valor de x debe ser de algún valor particular. Escoger un valor para x dentro de la lambda debería sonar bastante tonto, pero eso es lo que significan los errores sobre "no puede coincidir bla, bla, variable de tipo rígido, bla, bla".
Tenga en cuenta que, incluso sin el uso de cuantificadores explícitos forall, cualquier firma de tipo de nivel superior tiene implícita forall para cada variable de tipo mencionado.
Por supuesto, ese no es el error que está recibiendo. Lo que significa una "variable de tipo de escape" es incluso más tonto: es como tener un lambda (\x -> ...) e intentar usar valores específicos de xfuera de lambda, independientemente de aplicarlo a un argumento. No, no aplicar el lambda a algo y usar el valor del resultado - me refiero en realidad a usar la variable misma fuera del alcance donde está definida.
La razón por la que esto puede suceder con los tipos (sin parecer tan obviamente absurdo como el ejemplo con una lambda) es porque hay dos nociones de "variables de tipo" flotando: Durante la unificación, tiene "variables" que representan tipos indeterminados, que luego se identifican con otras variables de ese tipo a través de la inferencia de tipo. Por otro lado, tiene las variables de tipo cuantificadas descritas anteriormente que se identifican específicamente como variables sobre los tipos posibles.
Considere el tipo de la expresión lambda (\x -> x). Comenzando desde un tipo completamente indeterminado a, vemos que se necesita un argumento y se lo reduce a a -> b, luego vemos que debe devolver algo del mismo tipo que su argumento, por lo que lo reducimos más a a -> a. Pero ahora funciona para cualquier tipo a que desee, por lo que le damos un cuantificador (forall a. a -> a).
Por lo tanto, una variable de tipo escapado ocurre cuando usted tiene un tipo ligado por un cuantificador que infiere GHC deberían unificarse con un tipo indeterminado fuera del alcance de este cuantificador.
Parece ser que olvidé explicar el término "skolem type variable" aquí, heh. Como se menciona en los comentarios, en nuestro caso es esencialmente sinónimo de "variable de tipo rígida", por lo que lo anterior aún explica la idea.
no estoy del todo seguro de que el término se originó a partir, pero me imagino que implica Skolem normal form y representando existencial cuantificación en términos de universales, como se hace en GHC. Una variable de tipo skolem (o rígida) es aquella que, dentro de algún alcance, tiene un tipo desconocido pero específico por alguna razón, que es parte de un tipo polimórfico, proveniente de un tipo de datos existenciales, & c.
http://hackage.haskell.org/trac/ghc/ticket/7194? –
Sí, lo vi, pero ese boleto no da mucha explicación sobre lo que es un skolem. –
Estoy buscando una explicación de qué skolems son y qué los causa, en lugar de específicamente cómo arreglar mi código. Ya arreglé mi código, pero no estoy muy seguro de por qué lo que hice hizo que los skolems se fueran ... –