Principal Type Inference under a Prefix

At the heart of the Damas-Hindley-Milner (HM) type system lies
the abstraction rule which derives a function type for a lambda expression.
In this rule, the type of the parameter can be “guessed”, and can be any
type that fits the derivation. The beauty of the HM system is that there always exists a most general type that
encompasses all possible derivations — Algorithm W is used to infer these most
general types in practice.

Unfortunately, this property is also the bane of the HM type rules. Many languages
extend HM typing with additional features which often require complex side
conditions to the type rules to maintain principal types. For example, various type systems for
impredicative type inference, like HMF, FreezeML, or Boxy types, require
let-bindings to always assign most general types. Such a restriction is difficult
to specify as a logical deduction rule though, as it ranges over all possible
derivations. Despite these complications, the actual implementations of various
type inference algorithms are usually straightforward extensions of algorithm\ W,
and from an implementation perspective, much of the complexity of various type
system extensions, like boxes or polymorphic weights, is in some sense
artificial.

In this article we rephrase the HM type rules as _type inference under a
prefix_, called HMQ. HMQ is sound and complete with respect to the HM type
rules, but always derives principal types that correspond to the types inferred
by algorithm W. The HMQ type rules are close to the clarity of the declarative HM
type rules, but also specific enough to “read off” an inference algorithm, and
can form an excellent basis to describe type system extensions in practice.
We show in particular how to describe the FreezeML and HMF systems in terms
of inference under a prefix, and how we no longer require complex side conditions.
We also show a novel formalization of static overloading in HMQ as implemented
in Koka language.