Who ordered Skolem constants?

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.

About these ads
This entry was posted in Typing Tidbits and tagged . Bookmark the permalink.

9 Responses to Who ordered Skolem constants?

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

  2. Antoine Latter says:

    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.

  3. Iago says:

    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.

  4. Pingback: Let polymorphism | Generic Language

  5. Pingback: Type checking polarity | Generic Language

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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s