"Spurious" Type Equivalences in MLSub/Algebraic Subtyping

Question

I have been reading up on Stephen Dolan's "Algebraic Subtyping" in his PhD thesis and also the ICFP 2020 Paper "The simple essence of algebraic subtyping..." by Lionel Parreaux and I have found a puzzling "disagreement" between the two.

On the one hand, Dolan espouses the importance of "extensibility" of a notion of subtyping and defines subtyping as an initial distributive lattice supporting a specific group of type constructors of ML-style languages. So any type equivalence that holds in MLSub would then hold in any type system that is a complete lattice and satisfies some basic monotonicity properties for type constructors.

On the other hand, Parreaux criticizes MLSub for having too many type equivalences.

However, this comes at a cost: it requires making simplifying assumptions about the semantics of types. These assumptions hold in MLsub, but may not hold in languages with more advanced features.

Specifically, Parreaux says that in MLSub $(Int \to Int) \sqcap (Nat \to Nat)$ is equivalent to $(Int \sqcup Nat) \to (Int \sqcap Nat)$ and the record type $\{ tag: 0, payload: str \} \sqcup \{ tag: 1, payload: int \}$ is equivalent to the type $\{ tag: 0 \sqcup 1, payload: str \sqcup int \}$. He points to things like Typed Racket/TypeScript which would distinguish between these last two types (and probably also the first).

So how do I reconcile these two ? Is it that TypeScript/Typed Racket are not actually distributive lattices or that $\to$/record types aren't properly monotone/antitone? Or is my understanding of the initiality property wrong?

Answer 1

in their ICFP 2000 paper Intersection types and computational effects, Rowan Davies and Frank Pfenning showed that the distributivity rule for function types is unsound in the presence of effects.

This is because intersection introduction needs a value restriction in an effectful language and distributivity for function types lets you circumvent that. That is, you start with $\lambda x.\, e : (A \to B) \wedge (A \to C)$, and then if you have distributivity for function types, you get $\lambda x.\, e : A \to (B \wedge C)$.

So I would presume that Typed Racket does not support distributivity for function types.

Answer 2

A typechecker for an ML-like language has two tasks:

1. Inference: given a program, come up with a type for it, or prove that none exists.
2. Subsumption: given an inferred type and a user-written type signature, check that they match.

(1) can be done by collecting constraints arising from each subexpression, checking the set of constraints for consistency (i.e. that there is at least one solution), and reporting the set of constraints as the type of the program, possibly after simplification.

With subtyping, (2) is harder, as it requires not just checking for the existence of solutions to constraints, but checking that for every instance of the user-annotated type, there exists a compatible instance of the inferred one. (In other words, you're answering a $\forall\exists\dots$ question, not just a $\exists\dots$ question).

The point of initiality and distributivity of $\sqcap$ and $\sqcup$ over $\rightarrow$ and $\times$ in MLsub is to enable a solution of (2). (Prior systems already had solutions to (1): in particular, MLsub owes a lot to Pottier's 1998 thesis, which had inference but for which subsumption remains an open problem).

Parreaux's paper focuses on inference, mostly ignoring subsumption. He's correct in that you have a lot of freedom to change the subtyping order while keeping inference working, but if you drop initiality or distributivity then the MLsub subsumption algorithm stops working.

Answer 3

I'm late to the party, but I'd like to make a small clarification.

I did not really mean that MLsub has "too many" type equivalences. As explained in the same section of the Simple-sub paper (and pointed out by @dolan in his excellent answer above), while these equivalences come at a cost, they do give you simplification and subsumption checking algorithms in return. I was just highlighting that the equivalences are not strictly necessary for type inference itself, which I believe clarifies the ins and outs of the algebraic subtyping approach.

In most languages with unions and intersections, function types do not support such merging of their intersections. Here is a TypeScript example that demonstrates how it does not support merging intersected function types:

// An overloaded function f:
function f(x: string): string
function f(x: number): number
function f(x: unknown): unknown { return x }

let g: ((x: string) => string) & ((x: number) => number) = f

g("ok")
g(123)

let h: (x: string | number) => (string & number) = g  // error

Notice that the last line gives an error:

Type '{ (x: string): string; (x: number): number; }' is not assignable to type '(x: string | number) => never'.

It obviously has to be rejected: the identity function can be given type $(\mathit{Int} \to \mathit{Int}) \sqcap (\mathit{Str} \to \mathit{Str})$, but it is clearly not true that it can be given type $(\mathit{Int} \sqcup \mathit{Str}) \to (\mathit{Int} \sqcap \mathit{Str})$.

By contrast, MLsub can give both types $\mathit{Int} \to \mathit{Int}$ and $\mathit{Str} \to \mathit{Str}$ (and $\alpha \to \alpha$) to the identity function, but it cannot give it type $(\mathit{Int} \to \mathit{Int}) \sqcap (\mathit{Str} \to \mathit{Str})$. In that sense, MLsub is not a traditional intersection type system (in the sense of Barendregt, Coppo, and Dezani-Ciancaglini, a.k.a. BCD), which admit the intersection introduction rule:

$\begin{array}{cc} \dfrac{\Gamma \vdash_{\text{BCD}} M : \sigma \quad \Gamma \vdash_{\text{BCD}} M : \tau}{\Gamma \vdash_{\text{BCD}} M : \sigma \cap \tau}(\cap\text{I}) \end{array} $