<p>A typechecker for an ML-like language has two tasks:</p>
<ol>
<li><strong>Inference</strong>: given a program, come up with a type for it, or prove that none exists.</li>
<li><strong>Subsumption</strong>: given an inferred type and a user-written type signature, check that they match.</li>
</ol>
<p>(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.</p>
<p>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 <span class="math-container">$\forall\exists\dots$</span> question, not just a <span class="math-container">$\exists\dots$</span> question).</p>
<p>The point of initiality and distributivity of <span class="math-container">$\sqcap$</span> and <span class="math-container">$\sqcup$</span> over <span class="math-container">$\rightarrow$</span> and <span class="math-container">$\times$</span> in MLsub is to enable a solution of (2). (Prior systems already had solutions to (1): in particular, MLsub owes a lot to <a href="https://hal.inria.fr/inria-00073205/document" rel="noreferrer">Pottier's 1998 thesis</a>, which had inference but for which subsumption remains an open problem).</p>
<p>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.</p>

CC BY-SA 4.0
2022-03-04T10:10:16.377Z
2022-03-04T10:10:16.377Z
Stephen Dolan
<p>I'm late to the party, but I'd like to make a small clarification.</p>
<p>I did not really mean that MLsub has &quot;<em>too many</em>&quot; type equivalences. As explained in the same section of the Simple-sub paper (and pointed out by <a href="https://cstheory.stackexchange.com/users/65997/stephen-dolan">@dolan</a> 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.</p>
<p>In most languages with unions and intersections, function types do not support such merging of their intersections.
<a href="https://www.typescriptlang.org/play?#code/FAMwrgdgxgLglgewgAhACgB4C5kGcYBOcEA5gJQ75GmiSyIrrbIRgC2ARgKYEUvvcCtaPCSpMOSAGsICAO4Q+02QuQBvZAS4wwBFBmQBfYMAA225CRxoJeQsXLIAvAD471RwDJkN5q048ZM5u-oJBTqgmJGgARAhSMWTA0QCMAEwAzElmFgAW1sxUDsgAPvwBvME+RaTI3qGBzpbIyAD0rcg8BAhCwEA" rel="nofollow noreferrer">Here</a> is a TypeScript example that demonstrates how it does not support merging intersected function types:</p>
<pre><code>// 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) =&gt; string) &amp; ((x: number) =&gt; number) = f

g(&quot;ok&quot;)
g(123)

let h: (x: string | number) =&gt; (string &amp; number) = g  // error
</code></pre>
<p>Notice that the last line gives an error:</p>
<blockquote>
<p>Type '<code>{ (x: string): string; (x: number): number; }</code>' is not assignable to type '<code>(x: string | number) =&gt; never</code>'.</p>
</blockquote>
<p>It obviously has to be rejected: the identity function can be given type <span class="math-container">$(\mathit{Int} \to \mathit{Int}) \sqcap (\mathit{Str} \to \mathit{Str})$</span>, but it is clearly not true that it can be given type <span class="math-container">$(\mathit{Int} \sqcup \mathit{Str}) \to (\mathit{Int} \sqcap \mathit{Str})$</span>.</p>
<p>By contrast, MLsub can give both types <span class="math-container">$\mathit{Int} \to \mathit{Int}$</span> and <span class="math-container">$\mathit{Str} \to \mathit{Str}$</span> (and <span class="math-container">$\alpha \to \alpha$</span>) to the identity function, but it <em>cannot</em> give it type <span class="math-container">$(\mathit{Int} \to \mathit{Int}) \sqcap (\mathit{Str} \to \mathit{Str})$</span>. 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:</p>
<blockquote>
<p><span class="math-container">$\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}
$</span></p>
</blockquote>

CC BY-SA 4.0
2022-04-26T10:54:52.520Z
2022-04-26T10:54:52.520Z
Lionel Parreaux
<p>in their ICFP 2000 paper <a href="https://dl.acm.org/doi/abs/10.1145/351240.351259" rel="noreferrer"><em>Intersection types and computational effects</em></a>, Rowan Davies and Frank Pfenning showed that the distributivity rule for function types is unsound in the presence of effects.</p>
<p>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 <span class="math-container">$\lambda x.\, e : (A \to B) \wedge (A \to C)$</span>, and then if you have distributivity for function types, you get <span class="math-container">$\lambda x.\, e : A \to (B \wedge C)$</span>.</p>
<p>So I would presume that Typed Racket does not support distributivity for function types.</p>

CC BY-SA 4.0
2022-02-25T13:03:29.257Z
Distributive in this case means the distributive law of meets and joins: $a \sqcap (b \sqcup c) = (a \sqcup b) \sqcap (a \sqcup c)$ and the dual as well $a \sqcup (b \sqcap c) = (a \sqcap b) \sqcup (a \sqcap c)$. Does this implies the distributivity of function types you are describing?
Max New
CC BY-SA 4.0
2022-02-25T13:14:04.247Z
Ah, I’ve found my misunderstanding of the initiality property. The assumption is not just that all type constructors are *monotone* but that they are furthermore *lattice homomorphisms*, which includes your example.
Max New
CC BY-SA 4.0
2022-02-25T06:14:24.417Z
2022-02-25T06:14:24.417Z
Neel Krishnaswami
<p>I have been reading up on Stephen Dolan's &quot;Algebraic Subtyping&quot; in his PhD thesis and also the ICFP 2020 Paper &quot;The simple essence of algebraic subtyping...&quot; by Lionel Parreaux and I have found a puzzling &quot;disagreement&quot; between the two.</p>
<p>On the one hand, Dolan espouses the importance of &quot;extensibility&quot; 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.</p>
<p>On the other hand, Parreaux criticizes MLSub for having <em>too many</em> type equivalences.</p>
<blockquote>
<p>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.</p>
</blockquote>
<p>Specifically, Parreaux says that in MLSub <span class="math-container">$(Int \to Int) \sqcap (Nat \to Nat)$</span> is equivalent to <span class="math-container">$(Int \sqcup Nat) \to (Int \sqcap Nat)$</span> and the record type <span class="math-container">$\{ tag: 0, payload: str \} \sqcup \{ tag: 1, payload: int \}$</span> is equivalent to the type <span class="math-container">$\{ tag: 0 \sqcup 1, payload: str \sqcup int \}$</span>. He points to things like Typed Racket/TypeScript which would distinguish between these last two types (and probably also the first).</p>
<p>So how do I reconcile these two ? Is it that TypeScript/Typed Racket are not actually distributive lattices or that <span class="math-container">$\to$</span>/record types aren't properly monotone/antitone? Or is my understanding of the initiality property wrong?</p>

<type-systems><type-inference>
"Spurious" Type Equivalences in MLSub/Algebraic Subtyping
Max New
# "Spurious" Type Equivalences in MLSub/Algebraic Subtyping

(Asked by: username_0 on 2022-02-24)

I have been reading up on username_1's "Algebraic Subtyping" in his PhD thesis and also the ICFP 2020 Paper "The simple essence of algebraic subtyping..." by username_2 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?

**Tags:** type-systems, type-inference


---

## 3 answers

### Answer by username_3 on 2022-02-25. Score: 11 | Accepted answer

in their ICFP 2000 paper [*Intersection types and computational effects*](https://dl.acm.org/doi/abs/10.1145/351240.351259), 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.

> **Comments:**
> **username_0**: Distributive in this case means the distributive law of meets and joins: $a \sqcap (b \sqcup c) = (a \sqcup b) \sqcap (a \sqcup c)$ and the dual as well $a \sqcup (b \sqcap c) = (a \sqcap b) \sqcup (a \sqcap c)$. Does this implies the distributivity of function types you are describing?  
> **username_0**: Ah, I’ve found my misunderstanding of the initiality property. The assumption is not just that all type constructors are *monotone* but that they are furthermore *lattice homomorphisms*, which includes your example.  

---

### Answer by username_1 on 2022-03-04. Score: 10

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](https://hal.inria.fr/inria-00073205/document), 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 by username_2 on 2022-04-26. Score: 4

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}
$


---

