@pithlessly · github · λ

Date: 2023-12-25
Last updated: 2025-12-28

This is the first entry in what I intend as a multi-part series.

1ML is a type system designed by Andreas Rossberg and described in a collection of papers by him. When it comes to integrating an ML-style module system into a new language, I think 1ML currently provides the best overall story (although it’s not perfect).

Unfortunately, Rossberg’s papers are pretty technical. He is a good writer, but I feel that right now there is still a communication barrier between academics who are in a position to discuss 1ML in depth and people who are in a position to write new compilers. I see a lot more discussion online that merely references 1ML than I do discussion that seems to deeply understand it.

I’ve been studying 1ML for the last several months, and working on my own prototype implementation (which unfortunately isn’t yet in a publishable state). In an effort to help these ideas percolate down towards mainstream adoption, I want to help demystify some things that I found confusing.

This series will not substitute for reading the paper, but I hope it can be a useful companion. I’ll be working from the version of the paper published in the Journal of Functional Programming in 2018. It’ll be very helpful to be able to look at that paper as you read this. In fact, you can press this button to pull it up on the side in this page: Open (It probably doesn’t look great on mobile, unfortunately.)

Prerequisite knowledge

In writing this, I assume the reader:

• Has some familiarity with inference rule notation and how type systems are defined using a combination of grammars and inference rules.
• Has some familiarity with the module system of OCaml or Standard ML, from a user’s perspective (not necessarily knowing their internals).
• Has familiarity with 1ML’s design goals as outlined in the paper introduction.
• Has not necessarily read the prequel, F-ing modules, Rossberg’s earlier paper on compiling module calculi to F_ω.

Goals

By the end of this series of articles, the reader will have the tools they need to understand every single inference rule, including those of the type inference algorithm described in Section 7.

I also want to discuss some implementation concerns that are not mentioned in the paper (such as how to integrate type inference with levels).

Non-goals

A decent portion of the paper is dedicated to meta-theory (e.g. the proofs that the type system is sound, etc.). I have not read these sections in depth, and will not be discussing them here. It is reasonable for compiler authors to take these results as given and not focus on their details.

In some places, I will be criticizing the way the paper presents its ideas. Please do not take these as prescriptions for how it should have been written. I do not have the standing to make prescriptions like that; the paper was written with considerations other than the ones most important to me (such as brevity of the rules, ease of meta-theory, & an intended audience of other academics).

System F_ω and the architecture of the type system

At a basic level, 1ML is really just a sophisticated syntactic sugar for a version of the lambda calculus called System F_ω. If you’re not familiar, this is basically the core type system of Haskell, including higher-kinded type constructors, with all polymorphism being explicit. 1ML terms (I’ll use term and expression interchangeably) are converted into F_ω terms and 1ML types are converted into F_ω types.

The specific structure of this translation is best saved for a later article. For now, I’ll say that whenever a type $T$ appears in the surface syntax, it is immediately converted to a F_ω type written with the variable $\Xi$. After this translation, the rules completely forget about $T$ and don’t touch it again. This is why we see similar constructs written with two different syntaxes, like $\text{(= \textbf{type} $T$)}$ and $[= \tau]$

This may seem a little unfamiliar; I was used to seeing type systems that don’t distinguish between the surface syntax for types and the internal representation of types. But of course, a routine like this exists in any real-world type checker, it’s just that many papers would consider it “out of scope” and not discuss it.

I want to linger on the type system of F_ω for a bit longer. We can think of F_ω type expressions $\tau$ as terms in a simply-typed lambda calculus whose base “type” is $\Omega$, the kind of types. This is the core of what gives F_ω, and therefore 1ML, its power — type checking can invoke some form of computation at the type level. This power comes with a corresponding burden for the implementer, who must essentially build an interpreter for STLC into their type checker.

The key rule is this one:

$$\frac{ \Gamma \vdash e : \tau' \qquad \tau' \equiv \tau \qquad \Gamma \vdash \tau : \Omega }{ \Gamma \vdash e : \tau }$$

In words: “whenever an F_ω term $e$ is considered to have a type $\tau'$

The type equivalence rules are presented as two-directional equalities ($\equiv$), but in practice, a compiler will want to think of these as one-directional reductions. You can use a technique like normalization by evaluation for this. Bringing types all the way to normal form whenever you construct them is a viable approach, but it gets slow for very large types; there are standard techniques available for being lazier (this is not 1ML-specific).

Semantic types and modeling them in code

Figure 6 defines the grammar for semantic types. It’s important, so I’ll reproduce it here.

$$\begin{align*} \text{(abstracted)} \quad && \Xi \quad & ::= \quad \exists \overline\alpha. \Sigma \\ \text{(large)} \quad && \Sigma \quad & ::= \quad \pi \mid \text{bool} \mid [= \Xi] \mid \{ \overline{ l : \Sigma } \} \mid \forall \overline\alpha. \Sigma \to_\eta \Xi \\ \text{(small)} \quad && \sigma \quad & ::= \quad \pi \mid \text{bool} \mid [= \sigma] \mid \{ \overline{ l : \sigma } \} \mid \sigma \to_{\texttt{I}} \sigma \\ \text{(paths)} \quad && \pi \quad & ::= \quad \alpha \mid \pi \overline\sigma \\ \text{(purity)} \quad && \eta \quad & ::= \quad \texttt{P} \mid \texttt{I} \end{align*}$$

Large and small semantic types

The first thing we should observe is that large and small types aren’t really defining a new grammar, but instead a subgrammar of F_ω types (so we have $\{ \sigma \} \subseteq \{ \Sigma \} \subseteq \{ \Xi \} \subseteq \{ \tau \}$

The only wrinkle is the new type formers: the singleton $[= \Xi]$

Paths

The path grammar is a little wonky. It allows repetition of $\sigma$ in two different ways, suggesting that a path is an F_ω type variable applied to a list of lists of small types, like $\pi ::= \alpha \overline{\overline\sigma}$

I honestly find the whole idea of a path a little poorly motivated. My best attempt to articulate the role paths play in the rest of the paper is that they enforce that a semantic type is (roughly) in normal form (since type-level function applications always have a variable at their head), and that only small types can be applied as arguments to functions. “Path” is really a misnomer from this perspective. (The fact that a set of paths is an input to the subtyping relation $\Gamma \vdash \Sigma' \leq_{\overline\pi} \Sigma$

Abstracted types

The abstracted type grammar $\Xi ::= \exists \overline\alpha. \Sigma$ ^{You should think of “abstracted types” as corresponding to signatures (a.k.a. module types) in traditional descriptions of ML. They can contain one or more abstract types (the $\overline\alpha$}

As an illustration of this, you can look at the desugaring rules on page 25, which say that the surface signature { type t; x : t } gets desugared to $\Xi = \exists \alpha : \Omega. \{ t : [= \alpha], x : \alpha \}$

In my opinion, writing $\exists$ here is an abuse of notation. A better mental model of an abstracted type is something like $(\overline{\alpha : \kappa}. \Sigma)$

A summary of my implementation recommendations

• Don’t create a separate data type for F_ω types $\tau$; instead, create a data type that represents large types $\Sigma$.

• Contexts $\Gamma$ contain large types.

• Don’t have a separate data type for small types; it will result in too much code duplication. Instead, smallness should be an invariant not tracked by the type system.

• Do create a separate data type for $\Xi$, along the lines of:

  type signat = (type_variable * kind) list * large_type

• Introduce a dedicated constructor for $[= \Xi]$

• Either have a dedicated constructor for $\forall \overline\alpha. \Sigma \to_\eta \Xi$the syntactic invariant for pure functions ($\forall \overline\alpha. \Sigma \to_{\texttt{I}} \Xi$

Wrapping up

That’s all I have time for today. In the next entry, I’ll cover the surface syntax of 1ML, the desugaring judgement $\Gamma \vdash T \leadsto \Xi$

Footnotes