# Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack. For example:

newtype List t = List (forall r. r -> (t -> r -> r) -> r)

unList :: List t -> (forall r. r -> (t -> r -> r) -> r)
unList (List f) = f


Is (I think) equivalent to System-F omega:

List = \t. forall r. r -> (t -> r -> r) -> r


Except you have to call List and unList at the right moments.

Does this language with newtypes have more computation strength than System-F, equal to System-F omega?

• Aside: the relationship between $F$ and $F_{\omega}$ is not well-understood. Pawel Urzyczyn conjectured that $F_{\omega}$ is equivalent to typablility in $F_1$ (which is $F$ with first-order kinding). Oct 1 '19 at 20:57
• @MartinBerger for typing individual terms: obviously there are functions which are well typed both in system $F_\omega$ and system $F$, but that can only be actually used in system $F_\omega$.
– cody
Oct 3 '19 at 14:57
• @cody I'm referring to Problem 12 in the TLCA List of Open Problems. Oct 3 '19 at 15:53
• @MartinBerger I am familiar with the problem, but there is a subtle point here, which is that there are functions definable in $F_\omega$, which cannot be defined in $F$, if the function is to be taken $\mathbb{N}\rightarrow\mathbb{N}$.
– cody
Oct 4 '19 at 0:46
• @cody. By definable you mean semantically definable, not syntax? Aside, the conjecture is about $F_1$ vs $F_{\omega}$, that's what you meant? Oct 4 '19 at 9:01