How does GHC insert type abstraction/application under the RankNTypes extension

Question

I'm developing a functional programming language that offers Rank-n polymorphism. Like Haskell I don't want types to appear at the term level, but I have no idea to insert type abstraction and type application in a term afterward.

For example, identity function is defined like below in Haskell.

id :: forall a. a -> a
id = \x -> x

But in lambda calculus which is adopted as Haskell's core language, this represents id = ΛT. λx:T. x (ΛT is a type abstraction). And following function

foo :: Int
foo = id 3

is translated into foo = id @Int 3 in the core language (@Int is a type application)

Inserting type abstraction looks simple (just inserting ΛT in the place corresponding to forall a.), but type application is complicated because you have to decide not only where to apply the type but also what type to apply.

Although visualization of type application is discussed on this web page, I have not been able to find any document that describes an implicit insertion algorithm of type abstraction/application. It would be great if you could just give me a hint of the algorothm.

Answer 1

The one key thing that you need to do differently to support GHC-style rank-N types is use the user-supplied type signatures to guide the process of translation to System F. In ordinary Hindley-Milner type inference, that's optional: you can instead infer your own type and then unify it with the user-supplied type after the fact. With rank-N type signatures it's mandatory, as you'll generally end up inferring an incompatible type otherwise.

The specific cases largely write themselves, but here are some key examples:

• If you have a term $e$ with the known (user-supplied) type $\forall α. T(α)$, then the System F translation is $Λτ.$ prepended to the result of translating $e$ with the known type $T(τ)$, where $τ$ is a fresh rigid type variable.

• If you have a term $λx.e$ with the known type $S\to T$, then the translation is $λx{:}S.$ prepended to the result of translating $e$ with the known type $T$. Note that $S$ may contain $\forall$, so variables without type signatures can end up with higher-rank types inherited from a type signature on a containing term.

• If you have a term $x$ (an identifier), and $x$ in the environment has the type $\forall α_1\cdots α_k. T(α_1,\ldots,α_k)$, then translate to $x@τ_1@\cdots@τ_k$, where $τ_1,\ldots,τ_k$ are fresh flexible type variables, and return the type $T(τ_1,\ldots,τ_k)$ for that term. The actual types to be applied are determined by unification.

For instance:

• Type checking $λx.x$ with the type $\forall α. α\to α$ results in $Λτ. λx{:}τ. x$ by the first two rules.

• Type checking $\text{id}$ with $\text{id}:\forall α. α\to α$ in the environment results in $\text{id}@τ$ by the third rule, and $τ$ will at some point be unified with $\text{Int}$, so you will end up with $\text{foo} = \text{id}@\text{Int}\, 3$.

• For an actual higher-rank example, type-checking $λx.x$ with the type $(\forall α. α) \to (\forall β. β)$ results in $λx{:}(\forall α. α). Λτ. x@τ$.

The ugliest case is actually in standard H-M inference when you have mutually recursive functions with no type signatures. Since you haven't yet generalized them, you can't know whether type applications will need to be inserted at the recursive call sites, so you have to do a second pass after generalization, or extend your intermediate language in some way to avoid it. You don't have that problem with rank-N inference because the signature tells you where the type applications go.