What are skolems and why are they causing type errors?

Newton’s type system is an adaptation of Haskell’s, so it inherits many of the same concepts. One such concept is “skolems”. But what does that mean?

The best way to explain it is with an example.

The example

def add_one_implicit(a):
    return add_ints(a, 1)

def add_one_explicit[T](a: T):
    return add_ints(a, 1)

def add_ints(a: Int, b: Int) -> Int:
    return a + b

The first function omits the type of the a parameter, while in the second it has type T, an explicit type parameter. If you are new to languages in the ML family, the functions may seem equivalent. You will be surprised then that the second fails with a type error!

In academic jargon, the reason the type checker accepts one and not the other is that omitted types become unification variables, while explicit type parameters are skolem constants.

Type variables and skolems

A unification variable is a stand-in for an unknown and arbitrary type. The type checker will analyze how it is used and if possible infer another type to replace it.

Consider how a is used in the first function. It must have type Int since it is passed as an argument to add_ints. The compiler will thus assign add_one_implicit the type Int -> Int without complaints.

But why does it reject the second function? Because it is not free to make assumptions in this case. The caller can pass in anything it likes, and the callee is required to accept everything. The compiler cannot decide that T is actually an Int without contradicting the type annotation. The annotation and the type required by the body are therefore in conflict, so the type checker reports an error and aborts.

The programmer did not commit to a polymorphic type for the first function, so the compiler was free to infer that it is actually monomorphic.

Who decides?

Another way of saying it is that the difference lies in which side of the call gets to pick the type: the callers or the function body.

• For unification variables, the function body determines the type.
• For skolems, callers decide.

The side that does not decide must adapt to the other.

Constant variables

Skolems are sometimes referred to as rigid variables and sometimes as constants, which is confusing. They can’t be both, right?

The way I understand it is they are variables in one sense and constants in another. Variables in the sense that they represent an unknown, and constants in the sense that they cannot be given another value.

A common way to represent skolems in a compiler is actually to generate a fresh constant. Being constant prevents it from unifying with another type, and being fresh means the name is not taken already.

Summary

Skolems and unification variables both represent unknown types, but the compiler is not permitted to substitute skolems with another type. This is a useful concept to have for upholding the contract of a polymorphic type annotation, for instance.