Menu
Eeek! GHCi found Skolems in my 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 ... What are they? What do they want with my program? And why are they trying to escape (the ungrateful little blighters)?
235
Skolem function (plural Skolem functions) (logic) A function which replaces a variable bound by an existential quantifier which lies in the scope of an even number of logical negations; such function is a function of the remaining bound variables whose scope contain the given variable (being replaced).
A Skolem constant is a new constant that is substituted for a variable when eliminating an existential quantifier from a fact or a universal quantifier from a conjecture.
In general, an existential variable is replaced by a Skolem function of all the universal variables to its left. (A Skolem constant is a function of no variables.) Each Skolem constant or function that is introduced must be a new one, distinct from any constant or function symbol that has been used already.
Given any consistent first-order theory expressed in a countable language, Skolem showed how to construct a countable model of that theory from the countably many terms expressible in the language augmented with these Skolem functions.
In mathematical logic, a formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers. Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization).
Skolem used the term "relative" to describe this state of affairs, where the same set is included in two models of set theory, is countable in one model, and is not countable in the other model. He described this as the "most important" result in his paper.
Skolem's Paradox involves a seeming conflict between two theorems from classical logic. The Löwenheim-Skolem theorem says that if a first-order theory has infinite models, then it has models whose domains are only countable. Cantor's theorem says that some sets are uncountable.
To start with, a "rigid" type variable in a context means a type variable bound by a quantifier outside that context, which thus can't be unified with other type variables.
This works a great deal like variables bound by a lambda: Given a lambda (\x -> ... ), from the "outside" you can apply it to whatever value you like, of course; but on the inside, you can't simply decide that the value of x should be some particular value. Picking a value for x inside the lambda should sound pretty silly, but that's what errors about "can't match blah blah, rigid type variable, blah blah" mean.
Note that, even without using explicit forall quantifiers, any top-level type signature has an implicit forall for each type variable mentioned.
Of course, that's not the error you're getting. What an "escaped type variable" means is even sillier--it's like having a lambda (\x -> ...) and trying to use specific values of x outside the lambda, independently of applying it to an argument. No, not applying the lambda to something and using the result value--I mean actually using the variable itself outside the scope where it's defined.
The reason this can happen with types (without seeming as obviously absurd as the example with a lambda) is because there are two notions of "type variables" floating around: During unification, you have "variables" representing undetermined types, which are then identified with other such variables via type inference. On the other hand, you have the quantified type variables described above which are specifically identified as ranging over possible types.
Consider the type of the lambda expression (\x -> x). Starting from a completely undetermined type a, we see it takes one argument and narrow that to a -> b, then we see that it must return something of the same type as its argument, so we narrow it further to a -> a. But now it works for any type a you might want, so we give it a quantifier (forall a. a -> a).
So, an escaped type variable occurs when you have a type bound by a quantifier that GHC infers should be unified with an undetermined type outside the scope of that quantifier.
So apparently I forgot to actually explain the term "skolem type variable" here, heh. As mentioned in comments, in our case it's essentially synonymous with "rigid type variable", so the above still explains the idea.
I'm not entirely sure where the term originated from, but I would guess it involves Skolem normal form and representing existential quantification in terms of universal, as is done in GHC. A skolem (or rigid) type variable is one that, within some scope, has an unknown-but-specific type for some reason--being part of a polymorphic type, coming from an existential data type, &c.
51
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
