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?