I'm wondering if there's any update on this conjecture 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 in 1991; according to another email 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

  • $\begingroup$ 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! $\endgroup$
    – cody
    Commented Aug 4, 2022 at 15:39
  • 1
    $\begingroup$ 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... $\endgroup$
    – ionchy
    Commented Aug 5, 2022 at 17:03
  • 1
    $\begingroup$ 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). $\endgroup$
    – cody
    Commented Aug 5, 2022 at 18:47
  • 1
    $\begingroup$ Still, it's a natural question, and getting updates on the state of it would be nice. $\endgroup$
    – cody
    Commented Aug 5, 2022 at 18:48


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.