<p>I'm wondering if there's any update on <a href="http://tlca.di.unito.it/opltlca/opltlcasu19.html#x24-34000" rel="noreferrer">this conjecture</a> listed by Urzyczyn from years and years ago (I don't think that's its first appearance), which I'll restate below.</p>
<p>System F<sub>ω</sub> can be stratified into an infinite hierarchy of Systems F<sub>n</sub>, where F<sub>0</sub> corresponds to the usual polymorphic System F (quantifying over kinds ∗), F<sub>1</sub> to System F with type operators (quantifying over kinds e.g. ∗ → ∗), F<sub>2</sub> additionally quantifying over kinds e.g. (∗ → ∗) → ∗ (&quot;to the left of 2 arrows&quot;, so to speak), and so on.</p>
<p>Giannini et al. (1988) [1] show that there exists a (Curry-style, unannotated) lambda term that cannot be assigned a System F type, but which can be assigned a System F<sub>1</sub> type. (I believe it's <code>(λxy. y(xI)(xK))Ω</code>, where <code>Ω</code> is assigned some type that looks like <code>∀a: ∗ → ∗ . τ</code>.)</p>
<p>The question is then: <strong>For every n, is it possible to find a term that is not typeable in System F<sub>n</sub> but is typeable in System F<sub>n+1</sub> (or higher)?</strong> Urzyczyn asked this in <a href="https://www.seas.upenn.edu/%7Esweirich/types/archive/1991/msg00054.html" rel="noreferrer">an email</a> in 1991; according to <a href="https://www.cis.upenn.edu/%7Ebcpierce/types/archives/1993/msg00026.html" rel="noreferrer">another email</a> in 1993, Giannini et al. (1993) [2] were working on a partial result to collapse the hierarchy down to F<sub>1</sub> (which they call F<sub>3</sub>; unfortunate disagreement on the numbering conventions here...). Malecki (1997) shows that it does collapse (i.e. the answer to the above is <em>no</em>), but according to Urzyczyn on his webpage (first link above) the proof is incorrect.</p>
<p>Has any more progress been made toward this problem in either direction?</p>
<hr/>
<p>[1] <em>Characterization of typings in polymorphic type discipline</em>, LiCS 1988. <a href="https://ieeexplore.ieee.org/document/5101" rel="noreferrer">https://ieeexplore.ieee.org/document/5101</a>
<br/>
[2] <em>Type inference: some results, some problems</em>, Fundamenta Informaticae, 19:1-2. <a href="https://dl.acm.org/doi/abs/10.5555/175469.175472" rel="noreferrer">https://dl.acm.org/doi/abs/10.5555/175469.175472</a>
<br/>
[3] <em>Proofs in system F<sub>ω</sub> can be done in system F<sup>1</sup><sub>ω</sub></em>, CSL 1996. <a href="https://doi.org/10.1007/3-540-63172-0_46" rel="noreferrer">https://doi.org/10.1007/3-540-63172-0_46</a></p>

CC BY-SA 4.0
2022-08-04T15:39:24.977Z
Do you mind if I ask what prompted your interest in this question? The only person I've personally met that was enthusiastic about this was Pawel himself. It'd be cool to see renewed interest!
cody
CC BY-SA 4.0
2022-08-05T17:03:54.523Z
I think I literally just stumbled across the top link above last year while looking for unrelated stuff about rank-n polymorphism lol. It's been at the back of my mind since then bc it felt like the kind of thing that should've been (dis)proven by now, but I don't have much use for it and I'm guessing others don't either...
ionchy
CC BY-SA 4.0
2022-08-05T18:47:42.903Z
It certainly isn't useful in the way one might immediately think: the fact that a function is typeable in $F_1$ doesn't really guarantee that you'll have the type you "need", e.g. to apply to arguments. (What made me realize this is the fact that *every* normal form is typable in system $F$, but of course the type is usually useless).
cody
CC BY-SA 4.0
2022-08-05T18:48:08.837Z
Still, it's a natural question, and getting updates on the state of it would be nice.
cody
<type-theory><type-systems><typed-lambda-calculus>
Stratification of System Fω
ionchy
# Stratification of System Fω

(Asked by: username_0 on 2022-07-29)

I'm wondering if there's any update on [this conjecture](http://tlca.di.unito.it/opltlca/opltlcasu19.html#x24-34000) listed by Urzyczyn from years and years ago (I don't think that's its first appearance), which I'll restate below.

System Fω can be stratified into an infinite hierarchy of Systems Fn, where F0 corresponds to the usual polymorphic System F (quantifying over kinds ∗), F1 to System F with type operators (quantifying over kinds e.g. ∗ → ∗), F2 additionally quantifying over kinds e.g. (∗ → ∗) → ∗ ("to the left of 2 arrows", so to speak), and so on.

Giannini et al. (1988) [1] show that there exists a (Curry-style, unannotated) lambda term that cannot be assigned a System F type, but which can be assigned a System F1 type. (I believe it's `(λxy. y(xI)(xK))Ω`, where `Ω` is assigned some type that looks like `∀a: ∗ → ∗ . τ`.)

The question is then: **For every n, is it possible to find a term that is not typeable in System Fn but is typeable in System Fn+1 (or higher)?** Urzyczyn asked this in [an email](https://www.seas.upenn.edu/%7Esweirich/types/archive/1991/msg00054.html) in 1991; according to [another email](https://www.cis.upenn.edu/%7Ebcpierce/types/archives/1993/msg00026.html) in 1993, Giannini et al. (1993) [2] were working on a partial result to collapse the hierarchy down to F1 (which they call F3; unfortunate disagreement on the numbering conventions here...). Malecki (1997) shows that it does collapse (i.e. the answer to the above is *no*), but according to Urzyczyn on his webpage (first link above) the proof is incorrect.

Has any more progress been made toward this problem in either direction?

---

[1] *Characterization of typings in polymorphic type discipline*, LiCS 1988. <https://ieeexplore.ieee.org/document/5101>
  
[2] *Type inference: some results, some problems*, Fundamenta Informaticae, 19:1-2. <https://dl.acm.org/doi/abs/10.5555/175469.175472>
  
[3] *Proofs in system Fω can be done in system F1ω*, CSL 1996. <https://doi.org/10.1007/3-540-63172-0_46>

**Tags:** type-theory, type-systems, typed-lambda-calculus
> **Comments:**
> **username_1**: Do you mind if I ask what prompted your interest in this question? The only person I've personally met that was enthusiastic about this was Pawel himself. It'd be cool to see renewed interest!  
> **username_0**: I think I literally just stumbled across the top link above last year while looking for unrelated stuff about rank-n polymorphism lol. It's been at the back of my mind since then bc it felt like the kind of thing that should've been (dis)proven by now, but I don't have much use for it and I'm guessing others don't either...  
> **username_1**: It certainly isn't useful in the way one might immediately think: the fact that a function is typeable in $F_1$ doesn't really guarantee that you'll have the type you "need", e.g. to apply to arguments. (What made me realize this is the fact that *every* normal form is typable in system $F$, but of course the type is usually useless).  
> **username_1**: Still, it's a natural question, and getting updates on the state of it would be nice.  

---

## 0 answers

