It’s tempting, after a bit of experience with using nice functional languages, and some time spent really understanding what’s going on with (for example) Pierce’s books on type systems, to think you actually have some idea of what you’re doing when implementing one.

Ha!

Suppose you write:

foo :: a -> b
foo x = x

This should be a type error, of course. But how is this error discovered, exactly?

Typical presentations of type systems gloss over many implementation details, and for good reason, but here is one “implementation detail” that isn’t so much an implementation detail. It is a very important part of how type checking must be done in polymorphic languages with type annotations. Yet, I have seen nothing describing it.

To answer my own question, the trick seems to be that the ‘a’ and ‘b’ in the explicit type aren’t type variables, they are Skolem constants. Unlike variables, which can be unified with anything, Skolem constants only unify with exactly themselves. (Well, of course a variable can unify with a Skolem constant, but the rewrite generated is always from the variable to the constant.) The above gets caught as a type error because at some point the type checker will try to unify the two different Skolem constants ‘a’ and ‘b’.

Have you heard of this before, in this context? Please tell me where you might have seen it. So far, the only likely place I know of that I haven’t checked is the definition of SML. Haskell 98 does not seem to mention it, though I just realized perhaps I should check literature on Haskell prior to that. To discover this was the answer, I had to dive right into the GHC source code, and I really shouldn’t have had to do that.

### Like this:

Like Loading...

*Related*

My understanding is that a and b are implicitly universally quantified: forall a. forall b. a -> b. This is not directly helpful for writing the inference algorithm (as far as I can tell, Pierce mentions schemes for unifying subsets of System F, but doesn’t actually cover them in Types and Programming Languages), but it gives a really good intuition for the behavior of Skolem variables.

This may also be quite correct, and is another way to try to do this, actually without involving Skolem constants, I believe.

There is a trade-off in this approach, though, which is you cannot make use of annotations to drive other parts of inference. (I think I mention this in the next post…) What you’re doing, if you go this route, is doing inference without the annotation and then implementing some sort of “Is The Same As Or An Instance Of” test for the type annotation and the inferred type. (Which I don’t think would be the same as unification, nor is it alpha equivalence, it’s something slightly funnier… For example, it definitely has to ignore the order of the variable quantification. Maybe you can twist unification into working somehow…)

(The reason the quantification approach doesn’t involve Skolem constants is that you already had to type check the body of a definition before generalization happens. So those ‘forall’s don’t show up until, in some sense, it’s too late, you already did inference normally.)

This paper: “Practical type inference for arbitrary-rank types” extensively treats Skolem constants, but doesn’t go out of its way to define them. But the paper is a excellent read. (http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/)

The paper “Type Checking with Open Type Functions” also uses them in solving and has a better introduction and has a citation from ’97 on Skolem constants (http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/index.htm)

Aha! Thanks for these pointers. That first paper is actually already in my reading queue. :)

I have actually found a few dozen papers that make vague references to skolemization, but I still haven’t managed to trace them all back to something that’s quite explicit about it (though, I have been busy lately.) I still have a bit of a suspicion that it’s a folklore thing that may never have been explicitly described on its own, though that first paper does seem to adequately document it.

Well, take a look to “Practical Type Inference for Arbitrary Rank Polymorphism.”

If you transform

foo :: a -> b

foo x = x

as

foo = (\x -> x) :: forall a b. a -> b

then the typechecker described gives exactly the error you expect.

`1) forall a b. a -> b is skolemised resulting in a!1 -> b!1`

2) The meta-variable $1 is used as the type of x in \x -> ...

3) (\(x::$1) -> x) :: a!1 -> b!1

3.1) $1 is unified with a!1, so we continue with x:a!1 |- x : a!1

3.2) The inferred type a!1 does not unify with the expected type b!1, so we have a type error due to the attempt to unify two different skolem type variables.

In 3.1), shouldn’t it be x:a!1 |- x : b!1 ?

Pingback: Let polymorphism | Generic Language

Pingback: Type checking polarity | Generic Language

Pingback: A follow-up on Skolem constants | Generic Language