haskell - recursive - ¿Qué son skolems?

syntax record haskell

Question

Eeek! ¡GHCi encontró Skolems en mi código!

...
Couldn''t match type `k0'' with `b''
because type variable `b'' would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for
groupBy :: Ord b => (a -> b) -> Set a -> Set (b, [a])
The following variables have types that mention k0
...

¿Qué son? ¿Qué es lo que quieren con mi programa? ¿Y por qué están tratando de escapar (los pequeños ingratos blighters)?

Answer 1

El mensaje de error aparece cuando una variable de tipo intenta escapar de su alcance.

Me tomó un tiempo entender esto, así que voy a escribir un ejemplo.

{-# LANGUAGE ExistentialQuantification #-}
data I a = I a deriving (Show)
data SomeI = forall a. MkSomeI (I a)

Entonces, si tratamos de escribir una función

 unI (MkSomeI i) = i

GHC se niega a escribir-inferir / verificar-tipo esta función.

¿Por qué? Probemos inferir el tipo nosotros mismos:

• unI es una definición lambda, por lo que su tipo es x -> y para algunos tipos x e y .
• MkSomeI tiene un tipo para todo forall a. I a -> SomeI forall a. I a -> SomeI
  • MkSomeI i un tipo SomeI
  • i en el LHS tiene un tipo I z para algún tipo z . Debido a todo el cuantificador, tuvimos que introducir una nueva variable de tipo (reciente). Tenga en cuenta que no es universal, ya que está dentro de la (SomeI i) .
  • así podemos unificar la variable de tipo x con SomeI , esto está bien. Entonces, la unI debería tener el tipo SomeI -> y .
• i en el RHS tengo así tipo I z también.
• En este punto, unificador intenta unificar y y I z , pero nota que z se introduce en el contexto inferior. Por lo tanto, falla.

De lo contrario, el tipo para unI tendría tipo forall z. SomeI -> I z forall z. SomeI -> I z , pero el correcto es exists z. SomeI -> I z exists z. SomeI -> I z . Sin embargo, ese único GHC no puede representar directamente.

Del mismo modo, podemos ver por qué

data AnyEq = forall a. Eq a => AE a
-- reflexive :: AnyEq -> Bool
reflexive (AE x) = x == x

trabajos.

La variable (existencial) dentro de AE x no escapa al alcance externo, entonces todo está bien.

También encontré una "feature" en GHC 7.8.4 y 7.10.1 donde RankNTypes está bien, pero agregar GADTs desencadena el error

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
example :: String -> I a -> String
example str x = withContext x s
where
s i = "Foo" ++ str
withContext :: I a -> (forall b. I b -> c) -> c
withContext x f = f x

Por lo tanto, puede ser que no haya nada de malo en tu código. Podría ser GHC, que no puede resolver todo de manera consistente.

EDIT : la solución es dar un tipo a s :: forall a. I a -> String s :: forall a. I a -> String .

GADTs activan MonoLocalBinds , lo que hace que el tipo inferido de s tenga una variable skolem, por lo que el tipo no es siempre forall a. I a -> String forall a. I a -> String , pero t -> String , no se enlaza en el contexto incorrecto. Ver: https://ghc.haskell.org/trac/ghc/ticket/10644

Answer 2

Para empezar, una variable de tipo "rígida" 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" puedes aplicarlo al valor que quieras, por supuesto; pero por dentro, no puedes 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 utilizar cuantificadores explícitos forall , cualquier firma de tipo de nivel superior tiene un forall implícito para cada variable de tipo mencionada.

Por supuesto, ese no es el error que estás recibiendo. Lo que significa una "variable de tipo escapada" es incluso más tonto, es como tener un lambda (/x -> ...) y tratar de usar valores específicos de x fuera del 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 en el que 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 similares 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 expresión lambda (/x -> x) . Empezando desde un tipo completamente indeterminado a , vemos que toma un argumento y lo reduce a a -> b , luego vemos que debe devolver algo del mismo tipo que su argumento, por lo que lo reducimos aún más a a -> a . Pero ahora funciona para cualquier tipo que desee, así que le damos un cuantificador (forall a. a -> a) .

Por lo tanto, una variable de tipo de escape se produce cuando tiene un tipo vinculado por un cuantificador que GHC infiere debe ser unificado con un tipo indeterminado fuera del alcance de ese cuantificador.

Entonces, aparentemente me olvidé de explicar el término "variable de tipo skolem" aquí, je. 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 dónde se originó el término, pero supongo que implica Skolem forma normal y que representa la cuantificación existencial en términos de universal, como se hace en GHC. Una variable de tipo skolem (o rígida) es aquella que, dentro de algún ámbito, tiene un tipo desconocido pero específico por alguna razón: ser parte de un tipo polimórfico, procedente de un tipo de datos existencial, & c.

Answer 3

Según lo entiendo, una "variable Skolem" es una variable que no coincide con ninguna otra variable, incluido él mismo.

Esto parece aparecer en Haskell cuando se utilizan funciones como foralls explícitos, GADT y otras extensiones de sistema de tipo.

Por ejemplo, considere el siguiente tipo:

data AnyWidget = forall x. Widget x => AnyWidget x

Lo que esto dice es que puede tomar cualquier tipo que implemente la clase Widget , y envolverlo en un tipo AnyWidget . Ahora, supongamos que tratas de desenvolver esto:

unwrap (AnyWidget w) = w

Um, no, no puedes hacer eso. Porque, en tiempo de compilación, no tenemos idea de qué tipo tiene w , por lo que no hay forma de escribir una firma de tipo correcta para esto. Aquí el tipo de w ha "escapado" de AnyWidget , lo que no está permitido.

Según lo entiendo, internamente, GHC le da a w un tipo que es una variable Skolem, para representar el hecho de que no debe escapar. (Este no es el único escenario de este tipo, hay un par de otros lugares donde un cierto valor no puede escapar debido a problemas de tipeo).