Que sont les skolems?

Question

Eeek! GHCi a trouvé Skolems dans mon code!

 ...
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
...
 

Que sont-ils? Que veulent-ils avec mon programme? Et pourquoi tentent-ils de s'échapper (les petits fripons ingrats)?

Answer 1

Pour commencer, un "rigide" type de variable dans un contexte signifie un type de variable liée par un quantificateur en dehors de ce contexte, qui ne peut donc pas être unifiée avec d'autres variables de type.

Cela fonctionne beaucoup comme les variables liées par un lambda: étant Donné un lambda (\x -> ... ), de "l'extérieur", vous pouvez l'appliquer à la valeur que vous souhaitez, bien sûr; mais à l'intérieur, vous ne pouvez pas simplement décider que la valeur de x devrait être une certaine valeur particulière. Sélection d'une valeur de x à l'intérieur de la lambda devrait paraître très bête, mais c'est ce que les erreurs sur les "peuvent ne pas correspondre bla bla, rigide de type variable, bla bla" signifie.

Notez que, même sans l'aide explicite forall quantificateurs, tout haut-niveau de signature de type implicite forall pour chaque variable de type mentionné.

Bien sûr, ce n'est pas l'erreur que vous obtenez. Ce qu'une "échappé à la variable de type" moyen est encore plus idiot--c'est comme avoir un lambda (\x -> ...) et d'essayer d'utiliser des valeurs de x à l'extérieur de la lambda, indépendamment l'un de l'appliquer à un argument. Non, pas l'application de la lambda à quelque chose et, à l'aide de la valeur du résultat, je veux dire en fait à l'aide de la variable elle-même en dehors de la portée où elle est définie.

La raison de ce qui peut arriver avec des types (sans avoir l'air de toute évidence absurde, comme le montre l'exemple avec un lambda) c'est parce que il y a deux notions de "variables de type" flottant autour de: au Cours de l'unification, vous avez des "variables" qui représentent les types indéterminés, qui sont ensuite identifiés avec d'autres variables telles par l'inférence de type. D'autre part, vous avez la quantifiés type des variables décrites ci-dessus qui sont spécifiquement identifiés comme allant de plus de types possibles.

Prendre en compte le type de l'expression lambda (\x -> x). À partir d'une complètement indéterminé type a, nous voir, il prend un argument et étroite que d' a -> b, alors nous voyons qu'elle doit retourner quelque chose du même type que son argument, donc nous restreindre davantage d' a -> a. Mais maintenant, il fonctionne pour tout type a vous voulez, afin de nous donner un quantificateur (forall a. a -> a).

Donc, un échappé de la variable de type se produit lorsque vous avez un type liée par un quantificateur que GHC déduit devrait être unifiée avec un indéterminé type en dehors de la portée du quantificateur.

---

Donc, apparemment, j'ai oublié de réellement expliquer le terme "skolem variable de type" ici, heh. Comme mentionné dans les commentaires, dans notre cas, c'est essentiellement synonyme de "rigide type de variable", de sorte que la photo ci-dessus explique l'idée.

Je ne suis pas entièrement sûr de l'endroit où le terme est apparu, mais je suppose qu'il implique à la forme normale de Skolem et représentant existentielle quantification en termes de universel, comme cela se fait dans GHC. Un skolem (ou rigide) type de variable est celui qui, dans une certaine étendue, a un inconnu-mais-type spécifique pour une raison quelconque, une partie d'un type polymorphe, venant d'une existentiel type de données, &c.

Answer 2

Si je comprends bien, un "Skolem variable" est une variable qui ne correspond pas à une autre variable, y compris lui-même.

Ce qui semble apparaître dans Haskell lorsque vous utilisez des fonctions explicites foralls, GADTs, et d'autres types d'extensions système.

Par exemple, considérez le type suivant:

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

Ce que cela dit, c'est que vous pouvez prendre n'importe quel type qui implémente l' Widget classe, et l'envelopper dans un AnyWidget type. Maintenant, supposons que vous essayez de déballer ce:

unwrap (AnyWidget w) = w

Euh, non, vous ne pouvez pas le faire. Parce que, au moment de la compilation, nous n'avons aucune idée de ce type w a, donc il n'y a aucun moyen d'écrire un type correct de la signature de la présente. Ici le type d' w a "échappé" de l' AnyWidget, ce qui n'est pas autorisé.

Si je comprends bien, en interne GHC donne w d'un type qui est un Skolem variable, pour représenter le fait qu'il ne doit pas s'échapper. (Ce n'est pas le seul scénario; il ya un couple de d'autres endroits où une certaine valeur ne peut pas s'enfuir, grâce à la saisie des questions.)