<p>Type inference in a Damas-Hindley-Milner type system with subtyping is known to be undecidable in general.</p>
<p>What makes it so difficult? What options are there to get around undecidability which could make it work? For example, what are some &quot;minimal&quot; type annotations that would be necessary?</p>

<static-typing><type-inference><subtypes>
What are some options for integrating subtyping with Damas-Hindley-Milner inference?
CC BY-SA 4.0
2023-06-30T13:55:27.950Z
You can take a look at the work done by Nemerle developers - e.g.: https://moskal.me/pdf/msc.pdf
SK-logic
CC BY-SA 4.0
2023-06-30T16:07:00.933Z
There's also "algebraic subtyping," introduced by https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf and described more succinctly in https://dl.acm.org/doi/pdf/10.1145/3409006 and https://blog.polybdenum.com/2020/07/04/subtype-inference-by-example-part-1-introducing-cubiml.html
rpjohnst
<blockquote>
<p>Type inference in a Damas-Hindley-Milner type system with subtyping is known to be undecidable in general.</p>
<p>What makes it so difficult?</p>
</blockquote>
<p>You can have type inference for subtypes, but it’s undecidable to preserve <em>all</em> of the nice properties that make the algorithm W by Damas &amp; Milner so noteworthy:</p>
<ol>
<li>(Nice) Principal Types</li>
<li>No (Artificial) Annotations</li>
<li>Only Unification</li>
</ol>
<p>Subtyping interacts with all three. I can’t give a full exposition of all the issues, but I will give an overview of the specific challenges involved in this design space.</p>
<h1>1. (Nice) Principal Types</h1>
<p>The most important feature of the Damas–Hindley–Milner system, and the feature that I’ll spend the most time on here, is that it has <em>principal type inference</em>. In addition, the inferred types are very compact and easy to read.</p>
<p>Principal type inference means:</p>
<ol>
<li><p>The system has <em>principal types</em>.</p>
<p>If a term is typeable in a certain environment, then there is a generic type scheme that can be instantiated to give any valid type for that term in that environment.</p>
</li>
<li><p>There is a procedure (W) for finding the principal type.</p>
</li>
</ol>
<p>Subtype systems may not have principal types: a term can have multiple valid types, none of which is more general than the others; and which are all maxima, that is, not instances of a more general type.</p>
<h2>1.2. Decidable Subtyping</h2>
<p>The way Damas &amp; Milner achieve principality is essentially by restricting the subtyping relationship to a decidable one. There <em>is</em> a sort of subtype lattice, but it has only two levels:</p>
<ol>
<li><p>A universally quantified type variable is a <em>least specific</em> element</p>
</li>
<li><p>Any concrete type is a <em>most specific</em> one.</p>
</li>
</ol>
<p>(You can also stand on your head and call these “most general” and “least general” if you like—as long as you always remember which way is up!)</p>
<p>Because of these restricted levels, any bound on a type tells us a lot! Either we know exactly what it is, or we know that it must be polymorphic.</p>
<p>In the “less specific than” view of the lattice, any concrete types have a meet/min/lower-bound/intersection, namely a type variable; and no concrete types have a join/max/upper-bound/union. So, if you use a term at multiple types in the same context, then it must be <em>fully</em> polymorphic, or else it’s invalid; and you have to use a term consistently in different branches.</p>
<p>This rests on the fact that a universal “forall” quantifier is the same as an <em>infinite</em> intersection over all possible choices of type, that is:</p>
<p> identity : ∀<em>a</em>. <em>a</em> → <em>a</em></p>
<p> =</p>
<p> identity :<br />
   (unit → unit)<br />
  ∧ (bool → bool)<br />
  ∧ (int → int)<br />
  ∧ (string → string)<br />
  ∧ …</p>
<p>This is really what lets them compress a big gnarly type into a small one: any <em>valid</em> set of constraints can be simplified.</p>
<p>This kinship between universals and intersections means that a lot of results are related between the two. For example, intersection and union subtyping need restrictions in the presence of effects, just like ML’s “value restriction” for universals. And rank-2 universal quantification—where (∀<em>x</em>. …) only appears nested on the left of at most 1 function arrow—has decidable type inference, as do rank-2 intersection types. (See <a href="https://dl.acm.org/doi/10.1145/237721.237728" rel="nofollow noreferrer">Jim 1996</a>) for more. And while we’re here…</p>
<blockquote>
<h3>★ Tangent! Types vs. Typings</h3>
<p>A principal <em>type</em> is not the same as a principal <em>typing</em>, although the terms are sometimes mixed up.</p>
<p>A principal <em>type</em> is the <em>most general type</em> you can give to a term in a given environment. A principal <em>typing</em> is a pair of the <em>least constrained environment</em> where that term is typeable, and the principal type in that environment.</p>
<p>Simply typed lambda calculus, without named recursive definitions, has principal typings, but Damas &amp; Milner’s system doesn’t. For an example, consider:</p>
<p> <strong>let</strong> loop () = loop () <strong>in</strong><br />
  (loop ()) (loop ())</p>
<p>Since this is a nonterminating computation, it can be given any result type, as in:</p>
<ul>
<li><strong>S</strong> = ∀<em>a</em>. unit → <em>a</em> → <em>a</em></li>
<li><strong>T</strong> = ∀<em>b</em>. unit → <em>b</em></li>
</ul>
<p>And notice that S ≤ T. So these typings are both valid:</p>
<ul>
<li><p><strong>S ⊢ S</strong></p>
<p>loop : S ⊢ (loop ()) (loop ()) : S</p>
</li>
<li><p><strong>T ⊢ T</strong></p>
<p>loop : T ⊢ (loop ()) (loop ()) : T</p>
</li>
</ul>
<p>However, neither is more general than the other: (A ⊢ B) ≤ (C ⊢ D) if C ≤ A (contravariant) and B ≤ D (covariant), but (S ⊢ S) ≰ (T ⊢ T) and (T ⊢ T) ≰ (S ⊢ S) because we run into T ≰ S on each side.</p>
</blockquote>
<h2>1.3. Nominal Subtyping</h2>
<p>In a general subtyping lattice, we may have upper &amp; lower bounds that <em>don’t</em> give us equalities straight away. In a nominal type system, or when dealing with generic type variables, there isn’t necessarily any named type corresponding to the meet or join of any two types. As a result, we may need to keep intersections and unions around to solve later, if and when we get enough information to simplify them.</p>
<p>In the end, when we’ve accumulated all of the constraints we can deduce from the program, the solution isn’t necessarily unique.</p>
<p>We have a set of bounds, which we <em>can</em> check for consistency, at least. For example, if we only allow intersections and not unions, then we can report a type mismatch if there are multiple disjoint bounds. But with union types, even disjoint sets of constraints can be satisfied.</p>
<p>This comes down to a design question—you need to be very careful when extending the set of typeable valid programs, while still rejecting invalid programs, but how to do so is an art, not a single principle.</p>
<h2>1.4. Structural Subtyping</h2>
<p>You can do a little better here with structural/record types, because you may be able to simplify constraints earlier. You can construct an intersection A ∧ B directly, as the union of the properties of A and B.</p>
<p>This is part of how <a href="https://lptk.github.io/programming/2020/03/26/demystifying-mlsub.html" rel="nofollow noreferrer">algebraic subtyping</a> works. However, to achieve good inference, it gives up some opportunities for more expressiveness. For example, it relies on a <em>polarity</em> restriction: union types can’t appear in <em>negative</em> positions (inputs), and intersection types can’t appear in <em>positive</em> positions (outputs). So it can infer a function type such as A → (B ∨ C), but you can’t write a function of type (B ∨ C) → D and compose the two directly—instead, you would need to treat the cases B → D and C → D separately.</p>
<p>An understanding of polarisation in logic, and type inference as a kind of proof search, is helpful in coming up with ways to relax these restrictions. So, to your question:</p>
<blockquote>
<p>For example, what are some &quot;minimal&quot; type annotations that would be necessary?</p>
</blockquote>
<p>One way of allowing union types as inputs would be to allow “shift” annotations, whereby the programmer explicitly says where they want to switch polarity, to guide the inference process.</p>
<h1>2. No (Artificial) Annotations</h1>
<p>The second important property of algorithm W is that it needs <em>no artificial annotations</em>. Every definition’s type is inferrable without a type signature, and the only annotation that polymorphism needs is a very natural one, using a variable binding <strong>let</strong> <em>x</em> = <em>e</em><sub>1</sub> <strong>in</strong> <em>e</em><sub>2</sub> instead of a function application (λ<em>x</em>. <em>e</em><sub>2</sub>) <em>e</em><sub>1</sub>.</p>
<p>This again is a matter of design and praxis. The design of Haskell has been strongly informed by the goal of always being able to infer the types of programs in the basic language, when they’re unambiguous. But it’s also well established at this point that for any “fancy” extensions, type inference is a best effort, and at least some top-level annotations may be required, and this isn’t a burden—the sense is that the compiler should be allowed to ask for an annotation, if it has a good reason.</p>
<p>This also informs the design of Rust, which requires signatures on top-level definitions—indeed it doesn’t really have syntax for definitions <em>without</em> signatures.</p>
<h1>3. Only Unification</h1>
<p>Finally, W relies only on basic <em>unification</em> of equality constraints, which is decidable and efficient in practice. Upper and lower bounds are <em>inequality</em> constraints, which requires us to use <em>semi-unification</em>.</p>
<p>For arbitrary programs, this is undecidable (<a href="https://www.sciencedirect.com/science/article/pii/S0890540183710035" rel="nofollow noreferrer">Kfoury, Tiuryn, and Urzyczyn 1993</a>). Then again, humans don’t write arbitrary programs. So even an algorithm that isn’t guaranteed to terminate, or has poor asymptotic performance, can still sometimes be useful and efficient in practice.</p>
<p>Still, your final point:</p>
<blockquote>
<p>What options are there to get around undecidability which could make it work?</p>
</blockquote>
<p>There has been research into restrictions that make this problem decidable while remaining expressive (see <a href="https://link.springer.com/chapter/10.1007/3-540-54345-7_75" rel="nofollow noreferrer">Leiß and Henglein 2005</a>), such as:</p>
<ul>
<li>Limiting to one inequality at a time (uniformity)</li>
<li>Limiting bounds to simple pattern matches (left-linearity)</li>
<li>Placing various restrictions on recursion (acyclicity)</li>
<li>Bounding the number of variables to be solved, or where they may appear (quasi-monadicity)</li>
</ul>

CC BY-SA 4.0
2023-07-10T22:19:03.340Z
2024-07-07T05:45:57.607Z
2024-07-07T05:45:57.607Z
Jon Purdy
CC BY-SA 4.0
2024-07-05T21:40:40.143Z
Re your tangent on typings: can you give me a pointer to where the syntax you used is explained? I'm confused by the "valid typings" that start with bold, contain `—` and have two occurrences of `⊢`. I'm familiar only with "context ⊢ expression : type".
Bergi
CC BY-SA 4.0
2024-07-07T02:07:11.670Z
@Bergi: That’s a bullet point where the stuff to the left of the dash is a label and the stuff to the right is the details. I’ll try to format it differently so it’s less weird-looking.
Jon Purdy
CC BY-SA 4.0
2024-07-07T02:50:33.233Z
Ok, I considered that, but then [what does `⊢` mean](https://en.wikipedia.org/wiki/Turnstile_(symbol)#Interpretations) between two types? Also now that I'm looking closer, `loop loop` seems to be missing some unit arguments?
Bergi
CC BY-SA 4.0
2024-07-07T04:37:22.517Z
Good answer, fun tangential fact, nominal subtyping in languages that have generic types and contravariant conversions (that is, `IComparable<Animal>` is convertible to `IComparable<Giraffe>` is *also* undecidable unless you put certain restrictions on the kinds of types you can make bases of other types.
Eric Lippert
CC BY-SA 4.0
2024-07-07T04:48:16.170Z
Fun fact about that tangential fact, it was this answer on stack exchange about how decidability of nominal subtyping was conjectured but not proven to be undecidable that inspired someone to come up with the proof. :) https://cstheory.stackexchange.com/questions/18846/a-simple-decision-problem-whose-decidability-is-not-known/18866#18866
Eric Lippert
CC BY-SA 4.0
2024-07-07T06:00:04.807Z
@Bergi: Thanks, updated. A turnstile between a context and a type like (A ⊢ B) is just omitting the “proof terms”, that is the variable names and expressions, so it means the same as (x : A ⊢ e : B). I’m not sure of a reference, sorry. As I understand it we’re the weird ones in computer science for preferring to *add* these terms in. In classical-land, if A and B are just names for propositions, then *x* is redundant and the structure of *e* is already implicit in the structure of the proof.
Jon Purdy
# What are some options for integrating subtyping with Damas-Hindley-Milner inference?
Posted by: username_0 on 2023-06-30
Type inference in a Damas-Hindley-Milner type system with subtyping is known to be undecidable in general.

What makes it so difficult? What options are there to get around undecidability which could make it work? For example, what are some "minimal" type annotations that would be necessary?
**Tags:** static-typing type-inference subtypes
> **Comments:**
> **username_1**: You can take a look at the work done by Nemerle developers - e.g.: https://moskal.me/pdf/msc.pdf  
> **username_2**: There's also "algebraic subtyping," introduced by https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf and described more succinctly in https://dl.acm.org/doi/pdf/10.1145/3409006 and https://blog.polybdenum.com/2020/07/04/subtype-inference-by-example-part-1-introducing-cubiml.html  
---
## 1 answers
### Answer by username_3 on 2023-07-10. Score: 9 | Accepted answer
> Type inference in a Damas-Hindley-Milner type system with subtyping is known to be undecidable in general.
>
> What makes it so difficult?

You can have type inference for subtypes, but it’s undecidable to preserve *all* of the nice properties that make the algorithm W by Damas & Milner so noteworthy:

1. (Nice) Principal Types
2. No (Artificial) Annotations
3. Only Unification

Subtyping interacts with all three. I can’t give a full exposition of all the issues, but I will give an overview of the specific challenges involved in this design space.

# 1. (Nice) Principal Types

The most important feature of the Damas–Hindley–Milner system, and the feature that I’ll spend the most time on here, is that it has *principal type inference*. In addition, the inferred types are very compact and easy to read.

Principal type inference means:

1. The system has *principal types*.

   If a term is typeable in a certain environment, then there is a generic type scheme that can be instantiated to give any valid type for that term in that environment.
2. There is a procedure (W) for finding the principal type.

Subtype systems may not have principal types: a term can have multiple valid types, none of which is more general than the others; and which are all maxima, that is, not instances of a more general type.

## 1.2. Decidable Subtyping

The way Damas & Milner achieve principality is essentially by restricting the subtyping relationship to a decidable one. There *is* a sort of subtype lattice, but it has only two levels:

1. A universally quantified type variable is a *least specific* element
2. Any concrete type is a *most specific* one.

(You can also stand on your head and call these “most general” and “least general” if you like—as long as you always remember which way is up!)

Because of these restricted levels, any bound on a type tells us a lot! Either we know exactly what it is, or we know that it must be polymorphic.

In the “less specific than” view of the lattice, any concrete types have a meet/min/lower-bound/intersection, namely a type variable; and no concrete types have a join/max/upper-bound/union. So, if you use a term at multiple types in the same context, then it must be *fully* polymorphic, or else it’s invalid; and you have to use a term consistently in different branches.

This rests on the fact that a universal “forall” quantifier is the same as an *infinite* intersection over all possible choices of type, that is:

 identity : ∀*a*. *a* → *a*

 =

 identity :  
   (unit → unit)  
  ∧ (bool → bool)  
  ∧ (int → int)  
  ∧ (string → string)  
  ∧ …

This is really what lets them compress a big gnarly type into a small one: any *valid* set of constraints can be simplified.

This kinship between universals and intersections means that a lot of results are related between the two. For example, intersection and union subtyping need restrictions in the presence of effects, just like ML’s “value restriction” for universals. And rank-2 universal quantification—where (∀*x*. …) only appears nested on the left of at most 1 function arrow—has decidable type inference, as do rank-2 intersection types. (See [Jim 1996](https://dl.acm.org/doi/10.1145/237721.237728)) for more. And while we’re here…

> ### ★ Tangent! Types vs. Typings
>
> A principal *type* is not the same as a principal *typing*, although the terms are sometimes mixed up.
>
> A principal *type* is the *most general type* you can give to a term in a given environment. A principal *typing* is a pair of the *least constrained environment* where that term is typeable, and the principal type in that environment.
>
> Simply typed lambda calculus, without named recursive definitions, has principal typings, but Damas & Milner’s system doesn’t. For an example, consider:
>
> **let** loop () = loop () **in**  
>   (loop ()) (loop ())
>
> Since this is a nonterminating computation, it can be given any result type, as in:
>
> * **S** = ∀*a*. unit → *a* → *a*
> * **T** = ∀*b*. unit → *b*
>
> And notice that S ≤ T. So these typings are both valid:
>
> * **S ⊢ S**
>
>   loop : S ⊢ (loop ()) (loop ()) : S
> * **T ⊢ T**
>
>   loop : T ⊢ (loop ()) (loop ()) : T
>
> However, neither is more general than the other: (A ⊢ B) ≤ (C ⊢ D) if C ≤ A (contravariant) and B ≤ D (covariant), but (S ⊢ S) ≰ (T ⊢ T) and (T ⊢ T) ≰ (S ⊢ S) because we run into T ≰ S on each side.

## 1.3. Nominal Subtyping

In a general subtyping lattice, we may have upper & lower bounds that *don’t* give us equalities straight away. In a nominal type system, or when dealing with generic type variables, there isn’t necessarily any named type corresponding to the meet or join of any two types. As a result, we may need to keep intersections and unions around to solve later, if and when we get enough information to simplify them.

In the end, when we’ve accumulated all of the constraints we can deduce from the program, the solution isn’t necessarily unique.

We have a set of bounds, which we *can* check for consistency, at least. For example, if we only allow intersections and not unions, then we can report a type mismatch if there are multiple disjoint bounds. But with union types, even disjoint sets of constraints can be satisfied.

This comes down to a design question—you need to be very careful when extending the set of typeable valid programs, while still rejecting invalid programs, but how to do so is an art, not a single principle.

## 1.4. Structural Subtyping

You can do a little better here with structural/record types, because you may be able to simplify constraints earlier. You can construct an intersection A ∧ B directly, as the union of the properties of A and B.

This is part of how [algebraic subtyping](https://lptk.github.io/programming/2020/03/26/demystifying-mlsub.html) works. However, to achieve good inference, it gives up some opportunities for more expressiveness. For example, it relies on a *polarity* restriction: union types can’t appear in *negative* positions (inputs), and intersection types can’t appear in *positive* positions (outputs). So it can infer a function type such as A → (B ∨ C), but you can’t write a function of type (B ∨ C) → D and compose the two directly—instead, you would need to treat the cases B → D and C → D separately.

An understanding of polarisation in logic, and type inference as a kind of proof search, is helpful in coming up with ways to relax these restrictions. So, to your question:

> For example, what are some "minimal" type annotations that would be necessary?

One way of allowing union types as inputs would be to allow “shift” annotations, whereby the programmer explicitly says where they want to switch polarity, to guide the inference process.

# 2. No (Artificial) Annotations

The second important property of algorithm W is that it needs *no artificial annotations*. Every definition’s type is inferrable without a type signature, and the only annotation that polymorphism needs is a very natural one, using a variable binding **let** *x* = *e*1 **in** *e*2 instead of a function application (λ*x*. *e*2) *e*1.

This again is a matter of design and praxis. The design of Haskell has been strongly informed by the goal of always being able to infer the types of programs in the basic language, when they’re unambiguous. But it’s also well established at this point that for any “fancy” extensions, type inference is a best effort, and at least some top-level annotations may be required, and this isn’t a burden—the sense is that the compiler should be allowed to ask for an annotation, if it has a good reason.

This also informs the design of Rust, which requires signatures on top-level definitions—indeed it doesn’t really have syntax for definitions *without* signatures.

# 3. Only Unification

Finally, W relies only on basic *unification* of equality constraints, which is decidable and efficient in practice. Upper and lower bounds are *inequality* constraints, which requires us to use *semi-unification*.

For arbitrary programs, this is undecidable ([Kfoury, Tiuryn, and Urzyczyn 1993](https://www.sciencedirect.com/science/article/pii/S0890540183710035)). Then again, humans don’t write arbitrary programs. So even an algorithm that isn’t guaranteed to terminate, or has poor asymptotic performance, can still sometimes be useful and efficient in practice.

Still, your final point:

> What options are there to get around undecidability which could make it work?

There has been research into restrictions that make this problem decidable while remaining expressive (see [Leiß and Henglein 2005](https://link.springer.com/chapter/10.1007/3-540-54345-7_75)), such as:

* Limiting to one inequality at a time (uniformity)
* Limiting bounds to simple pattern matches (left-linearity)
* Placing various restrictions on recursion (acyclicity)
* Bounding the number of variables to be solved, or where they may appear (quasi-monadicity)
> **Comments:**
> **username_4** (2024-07-05): Re your tangent on typings: can you give me a pointer to where the syntax you used is explained? I'm confused by the "valid typings" that start with bold, contain `—` and have two occurrences of `⊢`. I'm familiar only with "context ⊢ expression : type".  
> **username_3** (2024-07-07): @Bergi: That’s a bullet point where the stuff to the left of the dash is a label and the stuff to the right is the details. I’ll try to format it differently so it’s less weird-looking.  
> **username_4** (2024-07-07): Ok, I considered that, but then [what does `⊢` mean](https://en.wikipedia.org/wiki/Turnstile_(symbol)#Interpretations) between two types? Also now that I'm looking closer, `loop loop` seems to be missing some unit arguments?  
> **username_5** (2024-07-07): Good answer, fun tangential fact, nominal subtyping in languages that have generic types and contravariant conversions (that is, `IComparable<Animal>` is convertible to `IComparable<Giraffe>` is *also* undecidable unless you put certain restrictions on the kinds of types you can make bases of other types.  
> **username_5** (2024-07-07): Fun fact about that tangential fact, it was this answer on stack exchange about how decidability of nominal subtyping was conjectured but not proven to be undecidable that inspired someone to come up with the proof. :) https://cstheory.stackexchange.com/questions/18846/a-simple-decision-problem-whose-decidability-is-not-known/18866#18866  
> **username_3** (2024-07-07): @Bergi: Thanks, updated. A turnstile between a context and a type like (A ⊢ B) is just omitting the “proof terms”, that is the variable names and expressions, so it means the same as (x : A ⊢ e : B). I’m not sure of a reference, sorry. As I understand it we’re the weird ones in computer science for preferring to *add* these terms in. In classical-land, if A and B are just names for propositions, then *x* is redundant and the structure of *e* is already implicit in the structure of the proof.  
---
