<p>The conclusion of [Kfoury &amp; Tiuryn 1992] says (emphasis mine):</p>

<blockquote>
  <p>We prove that [...] for every <span class="math-container">$k\ge 3$</span> there is a typing of constants
  that assigns types in <span class="math-container">$S(1)$</span> such that the type reconstruction problem
  for <span class="math-container">$\Lambda_k$</span> <strong>extended by this typing</strong> is undecidable.
  Unfortunately, this result does not give any clue as to whether type
  reconstruction for <span class="math-container">$F_2$</span>, with or without constants, is decidable.
  <strong>Our decidability/undecidability proofs use in an essential way the apriori information about the rank of types.</strong></p>
</blockquote>

<p>So, if you <em>don't</em> force constants to have certain pre-defined types of known rank, or if you don't have constants at all, the problem <em>may</em> become easier (than undecidable). The proofs rely on having constants that are forced to have certain types. (Of course, as you pointed out, Wells showed that the problem <em>isn't</em> easier.)</p>

CC BY-SA 4.0
2020-04-15T07:04:06.490Z
2020-04-15T07:04:06.490Z
Radu GRIGore
<p>There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of
the Second-Order <span class="math-container">$\lambda$</span>-Calculus", that proves that type inference for Curry-style rank-<span class="math-container">$k$</span> polymorphic lambda calculus is undecidable if <span class="math-container">$k \ge 3$</span>. My thought was that since there must be terms that can be typed in rank-3 but not rank-2, and since System F is rank-<span class="math-container">$n$</span> (i.e. the union of all finite rank-<span class="math-container">$k$</span>), surely this implies that Curry-style System F type inference is undecidable as well. However, its undecidability isn't proven until 1996 by Wells in "Typability and Type Checking in the Second-Order <span class="math-container">$\lambda$</span>-Calculus Are Equivalent and Undecidable", which explicitly mentions Kfoury's paper (along with others) and states that decidability of both type inference and type checking have not yet been proven until then.</p>

<p>So given that rank-3 polymorphic lambda calculus is a fragment of System F, why doesn't the former's undecidability imply the undecidability of the latter?</p>

<type-theory><decidability><typed-lambda-calculus><type-inference><polymorphism>
Decidability of rank-k polymorphism vs. System F
ionchy
# Decidability of rank-k polymorphism vs. System F

(Asked by: username_0 on 2020-04-14)

There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of
the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda calculus is undecidable if $k \ge 3$. My thought was that since there must be terms that can be typed in rank-3 but not rank-2, and since System F is rank-$n$ (i.e. the union of all finite rank-$k$), surely this implies that Curry-style System F type inference is undecidable as well. However, its undecidability isn't proven until 1996 by Wells in "Typability and Type Checking in the Second-Order $\lambda$-Calculus Are Equivalent and Undecidable", which explicitly mentions Kfoury's paper (along with others) and states that decidability of both type inference and type checking have not yet been proven until then.

So given that rank-3 polymorphic lambda calculus is a fragment of System F, why doesn't the former's undecidability imply the undecidability of the latter?

**Tags:** type-theory, decidability, typed-lambda-calculus, type-inference, polymorphism


---

## 1 answers

### Answer by username_1 on 2020-04-15. Score: 5 | Accepted answer

The conclusion of [Kfoury & Tiuryn 1992] says (emphasis mine):

> We prove that [...] for every $k\ge 3$ there is a typing of constants
> that assigns types in $S(1)$ such that the type reconstruction problem
> for $\Lambda\_k$ **extended by this typing** is undecidable.
> Unfortunately, this result does not give any clue as to whether type
> reconstruction for $F\_2$, with or without constants, is decidable.
> **Our decidability/undecidability proofs use in an essential way the apriori information about the rank of types.**

So, if you *don't* force constants to have certain pre-defined types of known rank, or if you don't have constants at all, the problem *may* become easier (than undecidable). The proofs rely on having constants that are forced to have certain types. (Of course, as you pointed out, Wells showed that the problem *isn't* easier.)


---

