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?

  • $\begingroup$ 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). $\endgroup$ Oct 1, 2019 at 20:57
  • $\begingroup$ @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$. $\endgroup$
    – cody
    Oct 3, 2019 at 14:57
  • $\begingroup$ @cody I'm referring to Problem 12 in the TLCA List of Open Problems. $\endgroup$ Oct 3, 2019 at 15:53
  • $\begingroup$ @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}$. $\endgroup$
    – cody
    Oct 4, 2019 at 0:46
  • $\begingroup$ @cody. By definable you mean semantically definable, not syntax? Aside, the conjecture is about $F_1$ vs $F_{\omega}$, that's what you meant? $\endgroup$ Oct 4, 2019 at 9:01


Your Answer

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